2022 Fiscal Year Annual Research Report
Formal Methods in General-Purpose Action-Oriented Programming
| Project/Area Number |
21J21087
|
|---|
| Allocation Type | Single-year Grants |
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
丁 曄澎 東京大学, 工学系研究科, 特別研究員(DC1)
|
|---|
| Project Period (FY) |
2021-04-28 – 2024-03-31
|
| Keywords | ソフトウェア工学 / 情報セキュリティ / 形式手法 / 分散システム / プログラミング言語 / ブロックチェーン |
|---|
| Outline of Annual Research Achievements |
本研究では、複雑システムの正当性を数理的に保証するための理論基盤と実践方法論の構築を目的としている。そのためには、形式手法によって堅牢なシステムを実現に向けた汎用アクション指向プログラミングパラダイムを提案している。使いやすい形式仕様記述手法を新しいモデリング言語に実装し、形式的検証とプログラムの自動生成を行うアルゴリズムを案出する。これにより、信頼性の高い分散システムや堅牢なプログラミングツール、および説明可能なAIモデルを構築することが可能となる。
今年度においては、構築している形式的検証手法に基づき、セキュリティ分野への応用研究を行った。具体的には、定式化した遷移システムのバリアントを使用し、抽象化されたセキュリティインフラのメカニズムの属性を自動的に検証できる手法を試みた。これにより、提案している理論の実用化を行い、有効性を評価し、実際のパファーマンスを測定した。特に、自己主権型アイデンティティの枠組みやブロックチェーン上の分散型アプリなどの中で、アクション指向プログラミングを用いてメカニズムの設計と検証を行い、安全性について形式的に解析した。研究成果は国際会議と論文誌で発表した。
また、アクション指向プログラミングの理論基盤を活用し、プログラム分析分野と分散コンピューティングにおける実用化を考案している。提案している形式仕様記述手法を使用し、プログラミングやアーキテクチャーなどの構造と行動の定式化をする上で、形式的検証技術を利用し、自動的に反例（脆弱性）を特定する方法を促進している。特に、スマートコントラクトの脆弱性の発見やコンセンサスメカニズムの正当性の証明などの最適化を探求している。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の研究計画の通りに実施し、汎用アクション指向プログラミングの理論基盤の構築が概ね完了し、実用化に焦点を当てた研究を行なった。提案した手法を多様な分野で実証し、その有効性を示した。研究成果として、国際会議での採択が2件，国内会議での発表が2件，国際誌での採択が1件となった。
|
| Strategy for Future Research Activity |
今後の計画として、実証の結果に基づき、汎用アクション指向プログラミングの理論を改善し、実用化を推進する予定である。具体的には、遷移システム理論と時相論理を発展させ、プログラム分析やセキュリティなどの分野で実証し、理論フレームワークの最適化を行う。また、提案手法を実装し、実際の複雑システムの開発と検証過程に応用し、実験で評価する。研究成果については、国際会議または論文誌で発表することを目指している。
|
