| 研究課題/領域番号 |
21H03421
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 国立情報学研究所 |
|---|
研究代表者 |
龍田 真 国立情報学研究所, 情報学プリンシプル研究系, 教授 (80216994)
|
|---|
| 研究分担者 |
中澤 巧爾 名古屋大学, 情報学研究科, 准教授 (80362581)
木村 大輔 東邦大学, 理学部, 講師 (90455197)
|
|---|
| 研究期間 (年度) |
2021-04-01 – 2024-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
16,900千円 (直接経費: 13,000千円、間接経費: 3,900千円)
2023年度: 5,460千円 (直接経費: 4,200千円、間接経費: 1,260千円)
2022年度: 5,460千円 (直接経費: 4,200千円、間接経費: 1,260千円)
2021年度: 5,980千円 (直接経費: 4,600千円、間接経費: 1,380千円)
|
|---|
| キーワード | ソフトウェア検証 / ソフトウェア解析 / 分離論理 / メモリ安全性 |
|---|
| 研究開始時の研究の概要 |
ソフトウェア検証理論として近年よい理論(オハーン理論)が提案され理論的にも実用的にも成功しているが, 精度がまだ不十分である. 本研究の大目的は, オハーン理論を発展させることにより高精度なソフトウェア検証を可能にする新理論を構築することである. 本研究の目的は, オハーン理論に一般的述語, 配列, 算術を追加した論理体系に対して, 関数の再帰呼出しを追加し, 再帰データを追加し, また, 関数ポインタ呼出しを追加し, またそれらのアルゴリズムの効率を実装実験により証拠付けることである. この実装システムを用いてOpenSSLおよびgitのCコードのメモリー安全性を検証する.
|
| 研究実績の概要 |
本研究の大目標は, オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して, 再帰呼出し, 再帰データ, 関数ポインタを追加し, 大規模なシステムソフトウェアを解析/検証する}ことができる理論を確立し, その理論に基づいて解析/検証システムをパソコン上に実装することであった. 研究成果は, オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して, 精密なメモリモデルの理論および再帰データ, 間接参照を追加した論理体系をまず構築し, これをほぼ実装した. また, この理論全体に関連して, 循環証明体系の計算の複雑性を明らかにした.
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して,精密なメモリモデルの理論および再帰データ, 間接参照を追加した論理体系をまず構築し, これをほぼ実装した. また, この理論全体に関連して, 循環証明体系の計算の複雑性を明らかにした. 以上により進捗はおおむね良好であるといえる.
|
| 今後の研究の推進方策 |
オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して, 再帰呼出し, 再帰データ, 関数ポインタを追加し, 大規模なシステムソフトウェアを解析/検証する}ことができる理論を確立し, その理論に基づいて解析/検証システムをパソコン上に実装する研究をさらに進める. ループ解析の精度が必要であることがわかってきたので, 抽象解釈の技法を取り入れてループ解析を高精度化する.
|
