2012 Fiscal Year Research-status Report
組込みソフトウェアの安全な構築のためのＣ言語のモデルとその形式検証
| Project/Area Number |
24500051
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| 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 – 2015-03-31
|
| Keywords | 形式検証 / 定理証明支援系 / C言語 / アセンブリ言語 / 多倍長整数演算 / 詳細化 / Coq |
|---|
| Research Abstract |
アセンブリ言語のプログラムのための形式検証基盤を改良した。その上で、詳細化という技術を用いて、この基盤上での形式検証のケーススタディーを行い、実用性を確認した。ここで用いた詳細化技術は、疑似コードとアセンブリ言語プログラムの関係を形式的に表現し、それらの対応関係を用いて形式検証を容易にする技術である。具体的な結果としては、MIPSアセンブリによる符号付き多倍長整数演算関数の実装25個（313行）に分離論理を適用して検証し、これらを用いた2進拡張互除法のアセンブリ言語プログラムの詳細化による検証に成功した。これらの検証した関数の行う処理は暗号スキームの実装などにしばしば使われるもので、今後の実験結果のライブラリとしての再利用も期待できる。これらのプログラムと検証結果をライブラリ化し公開した。以上の成果をまとめた論文を国際雑誌に投稿し採録され、現在出版予定である。つぎに、開発中のC言語の形式検証基盤の拡張に関しては、これまでの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言語とアセンブリ言語を同時に扱うための仕組みに、今回のアセンブリ言語の検証で用いた詳細化の枠組みとその研究で得られたノウハウを応用する。
|
| Strategy for Future Research Activity |
まず、本年度構築した関数呼出しの形式化を用いるプロトタイプを拡張する。具体的に、ローカル変数の概念などを導入し、関係する標準的な性質（健全性など）を形式化し、従来開発したC言語の形式検証基盤との統合を行う。この準備によって、プログラムのインタフェースに関する形式検証基盤上での取り扱いが整理される。次に、C言語とアセンブリ言語を両方扱えるように、従来開発したアセンブリ言語とC言語の形式検証基盤を拡張する。この研究にはテクニカルな詳細が多いため、最初にインラインアセンブリを用いるC言語プログラムの形式検証を実験として行う。その小規模実験を完成させたのち、プラットフォーム依存部分を抽象化するように努める。その翌年度には、ケーススタディーとして暗号スキーム実装の一部の検証ができるように努める。
|
| Expenditure Plans for the Next FY Research Funding |
主に成果発表と情報収集を行うため、旅費として研究費を使う。定理証明支援系の国際会議のワークショップで中間の成果を発表する。C言語とアセンブリ言語を両方扱える基盤を整備してから、その実験の結果に基づく論文の執筆を開始する。
|
