| Project/Area Number |
21H03421
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
龍田 真 国立情報学研究所, 情報学プリンシプル研究系, 教授 (80216994)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
中澤 巧爾 名古屋大学, 情報学研究科, 准教授 (80362581)
木村 大輔 東邦大学, 理学部, 講師 (90455197)
|
|---|
| Project Period (FY) |
2021-04-01 – 2024-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥16,900,000 (Direct Cost: ¥13,000,000、Indirect Cost: ¥3,900,000)
Fiscal Year 2023: ¥5,460,000 (Direct Cost: ¥4,200,000、Indirect Cost: ¥1,260,000)
Fiscal Year 2022: ¥5,460,000 (Direct Cost: ¥4,200,000、Indirect Cost: ¥1,260,000)
Fiscal Year 2021: ¥5,980,000 (Direct Cost: ¥4,600,000、Indirect Cost: ¥1,380,000)
|
|---|
| Keywords | ソフトウェア検証 / ソフトウェア解析 / 分離論理 / メモリ安全性 |
|---|
| Outline of Research at the Start |
ソフトウェア検証理論として近年よい理論(オハーン理論)が提案され理論的にも実用的にも成功しているが, 精度がまだ不十分である. 本研究の大目的は, オハーン理論を発展させることにより高精度なソフトウェア検証を可能にする新理論を構築することである. 本研究の目的は, オハーン理論に一般的述語, 配列, 算術を追加した論理体系に対して, 関数の再帰呼出しを追加し, 再帰データを追加し, また, 関数ポインタ呼出しを追加し, またそれらのアルゴリズムの効率を実装実験により証拠付けることである. この実装システムを用いてOpenSSLおよびgitのCコードのメモリー安全性を検証する.
|
| Outline of Annual Research Achievements |
本研究の大目標は, オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して, 再帰呼出し, 再帰データ, 関数ポインタを追加し, 大規模なシステムソフトウェアを解析/検証する}ことができる理論を確立し, その理論に基づいて解析/検証システムをパソコン上に実装することであった. 研究成果は, オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して, 精密なメモリモデルの理論および再帰データ, 間接参照を追加した論理体系をまず構築し, これをほぼ実装した. また, この理論全体に関連して, 循環証明体系の計算の複雑性を明らかにした.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して,精密なメモリモデルの理論および再帰データ, 間接参照を追加した論理体系をまず構築し, これをほぼ実装した. また, この理論全体に関連して, 循環証明体系の計算の複雑性を明らかにした. 以上により進捗はおおむね良好であるといえる.
|
| Strategy for Future Research Activity |
オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して, 再帰呼出し, 再帰データ, 関数ポインタを追加し, 大規模なシステムソフトウェアを解析/検証する}ことができる理論を確立し, その理論に基づいて解析/検証システムをパソコン上に実装する研究をさらに進める. ループ解析の精度が必要であることがわかってきたので, 抽象解釈の技法を取り入れてループ解析を高精度化する.
|
