2013 Fiscal Year Research-status 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)
|
|---|
| Keywords | 形式検証 / 定理証明支援系 / C言語 / アセンブリ言語 / セキュリティプロトコル / TLS / Coq |
|---|
| Research Abstract |
C言語のプログラムの形式検証基盤を完成した。ケーススタディーとして、セキュリティプロトコルTLSの実用的実装の一部の形式検証を完成した。具体的には、定理証明支援系Coqを用いて、ネットワークパケットのパージングを行う161行の関数(コメントとデバッグ情報を除く：85行)について形式仕様を記述（形式モデル：132行（元のプログラムのバグの修正のための12行を含む）)し、形式検証した。その検証実験の完成のため、形式検証基盤に自動検証機能を追加した。最終的に、全体で約3293行（形式モデルの1行当たり約24行）の形式証明を記述した。上記のC言語の形式検証基盤とケーススタディーを公開した。成果普及のために、C言語の形式検証基盤の最新版を国内ワークショップで発表し、デモを行った。情報収集に加え、以上の成果をまとめ、論文を国際雑誌に投稿した。また、昨年度のアセンブリ言語の形式検証と上記のC言語の形式検証研究をまとめ、国際ワークショップで発表し、国内ワークショップでポスター発表した。フランスのIRCICA研究所の2XS研究チーム(組込みソフトウェアのための安全性の研究)での成果発表がきっかけで、上記のC言語の形式検証基盤がプラットフォーム依存部分を正しく表現していて、組込みソフトウェアの形式検証に相応しいと確認できた。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究の目的は組込み用のプログラムのための定理証明支援系の形式検証基盤の構築である。現在まで、共通の形式定理のライブラリに基づいて、アセンブリ言語とC言語、それぞれの形式検証基盤を構築し、それぞれの基盤の有効性を、現実的なケーススタディーを用いて確かめた。アセンブリ言語とC言語を混在するプログラムの形式検証のためには、それぞれの基盤の正確さ・十分な詳細さが大事である。特に、アセンブリ言語とC言語がデータ構造を共通で使用できるよう、C言語の基本型（ポインタ、整数、構造体）の厳密な形式モデルの構築に努めた。しかし一方で、得たC言語の形式モデルの詳細さの副作用によって、今年度のケーススタディーの完成が困難になるほど、定理証明支援系の形式証明検査の効率が予想外に低下することも分かった。
|
| Strategy for Future Research Activity |
今後、アセンブリ言語とC言語の形式検証基盤の統合を行う。最初に、C言語でのインラインアセンブラ記述への対応を可能とする形式モデルを提案する。次に、昨年度形式化した関数呼出しのモデルを呼出規約の概念で詳細化・拡張する。そのため、従来開発したC言語の意味操作論と分離論理の形式モデルにローカル変数の概念を導入し、複数のアセンブリ言語を扱えるように関数呼出しの形式モデルを一般化する。統合した形式検証基盤の有効性を確かめるため、従来ケーススタディーとして行った多倍長整数やバイナリパケット等の形式検証を再利用する。ただ、新たなケーススタディーの完成のために、今年度明らかになった形式証明検査の効率低下の問題に対して、具体的な対策が必要になるかもしれない。また、フランスのIRCICA研究所の2XS研究チーム（チーム長: Prof. Gilles Grimaud；研究テーマ：組込みソフトウェアのための安全性の研究）で開発中の組込みソフトウェアに本研究の形式検証基盤を応用することを検討する。
|
| Expenditure Plans for the Next FY Research Funding |
国際誌の論文の執筆を最初の年度に行ったため、成果発表のための分の旅費の支出を最終年度にした。
主に成果発表と情報収集を行うため、旅費として研究費を使う。C言語とアセンブリ言語を両方扱える基盤を整理してから、その実験の結果に基づく論文を投稿する。
|
