2023 Fiscal Year Annual Research Report
Formal Methods in General-Purpose Action-Oriented Programming
| Project/Area Number |
22KJ0614
|
|---|
| Allocation Type | Multi-year Fund |
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
丁 曄澎 東京大学, 工学系研究科, 特別研究員(DC1)
|
|---|
| Project Period (FY) |
2023-03-08 – 2024-03-31
|
| Keywords | ソフトウェア工学 / 情報セキュリティ / 分散コンピューティング / 形式手法 / プログラミング言語 / ブロックチェーン |
|---|
| Outline of Annual Research Achievements |
本研究では、複雑システムの正当性を数理的に保証するための理論基盤と実践方法論の構築を目的としている。今年度においては、形式的実装を実現に向けた遷移指向プログラミング(Transition-Oriented Programming)パラダイムの基本理論の構築し、特有の遷移指向プログラミング言語を実装した。そして、遷移指向プログラミングパラダイムと言語に基づき、様々な分野への応用研究を行った。これにより、信頼性の高い分散システムや堅牢なプログラミングツール、および説明可能なAIモデルを構築することが可能となった。
具体的には、グラフ遷移システム(Graph Transition System)理論を案出し、遷移システム理論と書き換えシステム理論を統一している。これで、システムの正当性を形式化し、時相型プロパティと関数型プロパティを同じ理論フレームワークに形式仕様記述、検証、実装することが可能となった。また、Seniという遷移指向プログラミング言語を実装し、グラフ遷移システム理論を実用化した。これにより、提案している遷移システム理論を分散コンピューティング、情報セキュリティ、ソフトウェア工学、暗号理論などの分野に応用した。例えば、検証したプロパティに基づき、正当性を保証する分権システム(Decentralized Systems)の形式的実装手法を提案した。また、自己主権型アイデンティティの枠組みの正当性を確保するための検証と実装するフレームワークを構築した。さらに、非中央集権型アプリ、特に分散型金融プロトコルの脆弱性を特定できる手法を実現した。研究成果は国際会議と論文誌で発表した。
|
