Development of model checking technology for dependable distributed systems

• Project/Area Number: 23K28060
• Project/Area Number (Other): 23H03370 (2023)
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Multi-year Fund (2024); Single-year Grants (2023)
• Section: 一般
• Review Section: Basic Section 60050:Software-related
• Research Institution: Osaka University
• Principal Investigator: 土屋 達弘 大阪大学, 大学院情報科学研究科, 教授 (30283740)
• Co-Investigator(Kenkyū-buntansha): 林原 尚浩 京都産業大学, 情報理工学部, 教授 (20397227) ; 緒方 和博 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (30272991) ; 中川 博之 岡山大学, 環境生命自然科学学域, 教授 (40508834)
• Project Period (FY): 2023-04-01 – 2027-03-31
• Project Status: Granted (Fiscal Year 2024)
• Budget Amount: ¥18,330,000 (Direct Cost: ¥14,100,000、Indirect Cost: ¥4,230,000); Fiscal Year 2026: ¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000); Fiscal Year 2025: ¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000); Fiscal Year 2024: ¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000); Fiscal Year 2023: ¥5,850,000 (Direct Cost: ¥4,500,000、Indirect Cost: ¥1,350,000)
• Keywords: ディペンダブルシステム / 分散システム / モデルチェッキング / 機密実行

Outline of Research at the Start

ネットワーク上で複数のサーバを協調させサービスを実現する分散システムは，現代の情報化社会において欠かせない．このような分散システムを，誤りや悪意ある攻撃に耐えられるように，信頼性高く，つまり，ディペンダブルに実現するためには，その設計の正しさを網羅的に検証することが重要である．本研究では，分散システムの設計を検証するために，モデルチェッキングと呼ばれる手法を発展させる．具体的には，現状，サーバの台数が小さい場合にしか適用できないこの手法を，より規模の大きいシステムにも適用できるようにする．さらに，最近のCPUがもつ機密実行機能を利用した分散システムの検証も可能にする．