| Research Abstract |
組込みシステムの普及に伴い,低レベルプログラムの安全性の保証に対する重要性が高まっている.国際規格において,最も厳密な評価保証レベルは形式検証である.しかし,大規模なプログラムの形式検証は技術的にまだ大変な作業であるため,一般的に使われていない.本研究の目的は,この現状の改善としてプログラムの形式検証の環境を実現することである.今年度の成果は二つ目のケーススタディの完成と基礎ライブラリの拡張とアセンブリとC言語を組み合わせたプログラムのサポートに向けての拡張である.
平成21年度に低レベルプログラムの形式検証のスケーラビリティ問題に対して抽象的な疑似コードからのアセンブリプログラムの構成を提案した:新しい多倍長正数の関数を形式検証し,詳細化の予備実験を行った.今年度,分離論理を利用して,符号付きの整数を形式化し,多倍長整数の関数の形式検証ができた.その関数を利用して,2進拡張互除法の疑似コードからアセンブリプログラムを構成し,疑似コードの詳細化によって,その正しさの形式証明を取得し,現実的で形式検証済みの符号付きの多倍長整数のライブラリの構築が可能になった.
平成22年度にC言語の形式モデルを提案した.今年度,分離論理の定理を形式化し,アラインメントとパディングを公理化した.この拡張によって,アセンブリとC言語を組み合わせたプログラムの形式検証が可能になる.
平成21・22年度に暗号論的疑似乱数生成器の形式検証ができた.その際,プログラムに対して分離論理に基づく仕様を利用し,その仕様自体は第三者の数学の形式基盤(確率論,整数論)から得た.今回,その数学の形式基盤を拡張した.大数の法則を含む確率論の形式化に加えて,情報理論の基礎を形式化し,情報理論の有名なシャノン定理の形式化が成功した.その新しい基盤は情報理論に基づく次世代暗号のプログラムの形式検証に役に立つ.
|
