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 *help |
¥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がもつ機密実行機能を利用した分散システムの検証も可能にする．
|
| Outline of Annual Research Achievements |
本課題の初年度であった2023年度は、関連研究の詳細な調査と、それに基づく研究の実現方法の具体化を検討した．これに加えて，計画達成のための基本となる技術の研究開発を行った。
まず，ディペンダブル分散システムの核となるアルゴリズムの正しさの保証について，アルゴリズムの形式記述，および，モデルチェッキングによる形式検証を実施した．具体的には，本課題の主要な対象として取り上げているコンセンサスアルゴリズムについて，形式仕様記述言語を用いてモデル化を行った．2023年度は，プロセスのクラッシュやメッセージの喪失（オミッション故障）への耐性を保証するRaftアルゴリズムに加えて，ラウンドモデルという抽象化された分散計算モデル上で設計されたいくつかのアルゴリズムを取り上げ，仕様記述とモデルチェッキングによる形式検証を実施した．仕様記述言語・フレームワークには，RaftについてはMaudeを用いた．また，ラウンドモデル上のアルゴリズムについては，TLA+を利用した．後者のラウンドモデルベースのアルゴリズムについては，メッセージの内容が任意に書き換わる故障への耐性をもつものも検証の対象とし，そのような故障のモデル化も同時に実施した．
更に，分散システムにおけるセキュリティの実現方法と，その検証について，既存のセキュリティプロトコルの形式検証だけでなく，TEE（機密実行環境，trusted execution environment）を利用した新たなプロトコルの検討を行った．
これらの研究の結果の一部について，国内および国際会議にて発表を実施した．
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
本研究は全体を4年間として計画している．1年目の2023年度は，先行研究や最新研究の詳細な調査と，それに基づく研究の実現方法の具体化を主な課題と考えていた．2023年度はこの課題を実施すると共に，参画する各研究者が各自で計画達成のための基本となる技術の研究開発を行った．具体的には、ディペンダブル分散システムで中心的な役割を果たすコンセンサスアルゴリズムの仕様化とモデルチェッキング，セキュリティプロトコルの検討や形式検証などである．これらの研究について，すでに国内外の会議で発表を実施しており，初年度の進捗については，計画より進んでいると判断した．
|
| Strategy for Future Research Activity |
計画の通り，ディペンダブルな分散システム実現の核となるコンセンサスアルゴリズムを中心に，その正しさを保証するための検証等の研究を進める．すでに，いくつかの具体的なアルゴリズムについて，形式仕様記述とモデルチェッキングを試みている．今後は，これらの研究を発展させ，ビザンチン障害を含むように対象となる故障モデルを拡大するとともに，モデルチェッキングの性能（検証の速度，扱うことのできるシステムの大きさ）を向上させるための技術の開発を行う．
加えて，検証の対象として，TEEを利用したアルゴリズムを扱えるように，仕様化およびモデルチェッキングや他の検証技術を進化させる．
さらに，コンセンサスと組み合わせて用いられることの多い，リーダー選挙アルゴリズムについても，対象を広げて研究を行う．ここで，具体的なリーダー選挙として，シークレットリーダー選挙を対象とすることを検討している．これは，選ばれたリーダーにしか選挙の結果がわからないという性質を実現する問題であり，ブロックチェーンに代表されるコンセンサスアルゴリズムの応用において，リーダーへの攻撃を回避するのに有用である．
このシークレットリーダー選挙を含め，ディペンダブル分散システムの中核となるアルゴリズムを設計し，形式的な仕様化と検証を進めながら，実装レベルでの設計を進める．
|
Report
(1 results)
Research Products
(6 results)
