Quantitative extension of formal models and its application to software analysis

2022 Fiscal Year Final Research Report

• Project/Area Number: 19H04083
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Single-year Grants
• Section: 一般
• Review Section: Basic Section 60050:Software-related
• Research Institution: Nagoya University
• Principal Investigator: Seki Hiroyuki 名古屋大学, 情報学研究科, 教授 (80196948)
• Co-Investigator(Kenkyū-buntansha): 小川 瑞史 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (40362024) ; 結縁 祥治 名古屋大学, 情報学研究科, 教授 (70230612) ; 橋本 健二 名古屋大学, 情報学研究科, 助教 (90548447)
• Project Period (FY): 2019-04-01 – 2023-03-31
• Keywords: ソフトウェア検証 / モデル検査 / プログラム自動合成 / レジスタオートマトン / 形式言語理論 / 量的情報流 / 線形時相論理 / セキュリティ

Outline of Final Research Achievements

We studied on the following three research topics. First, we proposed two notions on dynamic quantitative information flow (QIF), analyzed the complexity for computing these QIFs and implemented a tool for computing these QIFs based on model counting tools. Second, we investigated the complexity of basic problems on register context-free grammar (RCFG). We then proposed generalized RCFG and provided a sufficient condition for an RCFG to have decidability property on basic problems. As an application of register models to software verification, we studied LTL (linear-time temporal logic) model checking for register pushdown systems. We also proposed a subclass of mu-calculus with the freeze quantifiers which are equivalent to register automata. Furthermore, we investigated the reactive synthesis from visibly register pushdown automata. Third, we introduced the optimal run problem for weighted register automata and analyzed its complexity.

Free Research Field

ソフトウェア基礎理論

Academic Significance and Societal Importance of the Research Achievements

ソフトウェアの信頼性を保証する方法論を確立することは現代社会の喫緊の課題である．本研究の成果は，長年にわたり蓄積されたソフトウェア検証の理論的成果をさらに現実の問題に応用可能とするため，情報漏洩量，データ値および重みといった量的概念を組み込んだ数理モデルに対して，ソフトウェアの信頼性を保証する手法を与えたことに学術的および社会的意義がある．例えば，有限状態モデルにデータ値を扱う能力を加えると容易に基本問題が判定不能となってしまうが，本手法におけるレジスタモデルではデータ値の操作に合理的制約を加えることにより，重要な基本問題の判定可能性を失うことなく拡張が可能となっている．