| 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コードのメモリー安全性を検証する.
|
