分離論理を用いたソフトウェア検証の発展

• 研究課題/領域番号: 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コードのメモリー安全性を検証する.