Formal Methods in General-Purpose Action-Oriented Programming

通用目的面向动作编程中的形式化方法

基本信息

批准号：
22KJ0614
负责人：
丁曄澎
金额：
$ 1.41万
依托单位：
The University of Tokyo
依托单位国家：
日本
项目类别：
Grant-in-Aid for JSPS Fellows
财政年份：
2023
资助国家：
日本
起止时间：
2023-03-08 至 2024-03-31
项目状态：
已结题

项目摘要

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

这项研究旨在建立一种理论基础和实用方法，以数学上确保复杂系统的合法性。为此，我们提出了一个通用的 - 可使用的动作，以面向的编程范式实现正式方法实现强大的系统。易于 - 使用形式规范说明方法以新的建模语言实现，我们提出了自动生成程序并自动生成程序的算法。结果，可以构建可靠的分布式系统，强大的编程工具以及可以解释的AI模型。在这个财政年度，我们根据建立的正式验证方法对安全领域进行了应用研究。具体而言，我们尝试使用公式过渡系统的范围自动验证抽象安全基础结构的属性。结果，提出的理论是实用的，评估了有效性并测量了实际的香水。特别是，在区块链上的自有权力身份和分布式应用程序的框架内，使用面向动作的编程设计和验证该机制，并对安全性进行了正式分析。该研究的结果发表在国际会议和文章中。此外，以动作为导向的编程的理论基础被认为是在程序分析和分散计算中实用的。如何使用正式验证技术使用正式的验证技术自动识别示例（漏洞），并使用拟议的形式规格描述方法来促进编程和架构的行为。特别是，它探讨了智能合同漏洞的发现以及共识机制合法性的优化。