| 研究概要 |
組込みシステムの普及に伴い,低レベルプログラムの安全性の保証に対する重要性が高まっている.
国際規格において,最も厳密な評価保証レベルは形式検証である.しかし,大規模なプログラムの形式検証は技術的にまだ大変な作業であるため,一般的に使われていない.本研究の目的は,この現状の改善として使い易いプログラムの形式検証の環境を実現することである.昨年度はその環境の整備と応用を行い,今年度の成果はその環境の改善とC言語の現実的なサポートの拡張である.
1.形式検証の環境の改善:プログラムの形式モデルから実行可能なコードの生成の方式を提案と実験をし,他の言語のサポートのための改善を行った.具体的に,アセンブリのモデルから実行可能なコードの生成ができ,その実験によって,本研究のアプローチの確認ができただけでなく,盛んなデバッガ(GDB)のバグも発見できた.また,形式検証の環境の改善として,モジュールを導入し,他の言語のサポートができるようになった.以上の成果を発表するため,JOUANNAUD Jean-Pierre教授に清華大学(北京,中国)で招待され,セミナー("Formal verification of cryptographic software in Coq", 2010年5月28日)を行った.昨年度の成果と上記の改善に基づく論文が国際雑誌に採択された.また,検証環境の改善として,符号付き多倍長整数演算を導入し,昨年度の予備実験(2進拡張互除法のアセンブリプログラム)に繋がる.
2.C言語の現実的なサポートの拡張:上記の形式検証の環境の改善を踏まえて,C言語のモデルの開発ができた.このモデルは現実的であるため、C言語とアセンブリを組み合わせる低レベルプログラムの検証が可能になる.例えば,現実的な特徴として(再帰的データを含む)構造体のレイアウトと動的メモリ割当を含むメモリーモデルである.学術的な貢献として現実的なC言語のモデルのための分離論理を挙げられる.その論理は象徴するアルゴリズム(in-place reverse list)で動作の確認を行った.
|
