2015 Fiscal Year Annual Research Report
組込みソフトウェアの安全な構築のためのＣ言語のモデルとその形式検証
| Project/Area Number |
24500051
|
|---|
| Research Institution | National Institute of Advanced Industrial Science and Technology |
|---|
Principal Investigator |
Affeldt Reynald 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (40415641)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
大岩 寛 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 研究グループ長 (20415649)
|
|---|
| Project Period (FY) |
2012-04-01 – 2016-03-31
|
| Keywords | 形式検証 / 定理証明支援系 / C言語 / 多倍長整数演算 / Coq |
|---|
| Outline of Annual Research Achievements |
C言語の形式検証基盤に関数呼出しに対応する拡張を行った。その拡張に基づいて国際会議でチュートリアルを行った。平成２６年度に明らかになった定理証明支援系Coqの効率低下の問題は解決した。そのため、Coqの開発者会議に参加し、本研究のパフォーマンス問題を議論した。また、効率の問題に対して、自動検証のためのプラグインの開発を検討した。その開発のための必要な知識はCoqの開発者会議で得た。その実験に基づいた報告を国内会議で発表した。本研究のC言語の形式検証基盤とそのケーススタディ（セキュリティプロトコルTLSの実用的実装の検証）を招待講演として国内会議で発表した。フランスのIRCICA研究所に招待され（ホスト：Prof. Gilles Grimaud）、本研究のアセンブリ言語とC言語形式検証基盤を発表した。また、本研究の多倍長整数演算関数の形式検証技術の改善を始めた。平成２４年度に行った多倍長整数演算関数の形式検証技術を議論するために、スタンフォード大学で行われたHACS 2016会議に招待された。その際、最も効率的な多倍長整数演算関数実装GMPの形式検証プロジェクトをスペインのIMDEA Software研究所のDr. Strubと提案した。現在、Dr. Dupressoirの協力を得て、形式検証実験を行っている。現時点、多倍長整数の加算・減算・乗算・比較・シフトなどの関数実装の正当性の形式検証ができ、今後検証済みC言語コードの出力を行う予定である。
|
