Formal Methods in General-Purpose Action-Oriented Programming

点击翻译按钮获取中文摘要

本研究では、複雑システムの正当性を数理的に保証するための理論基盤と実践方法論の構築を目的としている。そのためには、形式手法によって堅牢なシステムを実現に向けた汎用アクション指向プログラミングパラダイムを提案している。使いやすい形式仕様記述手法を新しいモデリング言語に実装し、形式的検証とプログラムの自動生成を行うアルゴリズムを案出する。これにより、信頼性の高い分散システムや堅牢なプログラミングツール、および説明可能なAIモデルを構築することが可能となる。今年度においては、構築している形式的検証手法に基づき、セキュリティ分野への応用研究を行った。具体的には、定式化した遷移システムのバリアントを使用し、抽象化されたセキュリティインフラのメカニズムの属性を自動的に検証できる手法を試みた。これにより、提案している理論の実用化を行い、有効性を評価し、実際のパファーマンスを測定した。特に、自己主権型アイデンティティの枠組みやブロックチェーン上の分散型アプリなどの中で、アクション指向プログラミングを用いてメカニズムの設計と検証を行い、安全性について形式的に解析した。研究成果は国際会議と論文誌で発表した。また、アクション指向プログラミングの理論基盤を活用し、プログラム分析分野と分散コンピューティングにおける実用化を考案している。提案している形式仕様記述手法を使用し、プログラミングやアーキテクチャーなどの構造と行動の定式化をする上で、形式的検証技術を利用し、自動的に反例（脆弱性）を特定する方法を促進している。特に、スマートコントラクトの脆弱性の発見やコンセンサスメカニズムの正当性の証明などの最適化を探求している。