| 研究概要 |
組込みシステムの普及に伴い,低レベルプログラムの安全性の保証に対する重要性が高まっている.国際規格において,最も厳密な評価保証レベルは形式的検証である.しかし,大規模なプログラムの形式的検証は技術的にまだ大変な作業であるため,一般的に使われていない.本研究の目的は,この現状の改善として使い易いプログラムの形式的検証の環境を実現することである.今年度の成果はその環境の整備とそれによる新しい応用である.
1. 形式的検証の環境の整備:本研究の形式的検証の環境は基礎ライブラリに基づいており,データ構造や低レベルプログラム(C言語のサブセットとスマートカード用のアセンブリ)の性質(分離論理で表現)を提供する.今回,以前本研究代表者が携わった成果を元にして,機能の改善と整理を行った.拡張の一例として,形式的検証済みの小規模コンパイラを追加した.そのコンパイラは制御構造とジャンプ命令の言語の間の翻訳において,意味を保つだけでなく,分離論理による性質も保つ.
2. 新しい応用:現実的な疑似乱数生成器の形式的検証に成功した.アセンブリ言語を扱い易くするために,上記のコンパイラを利用した.その成果は安全性の面から重要である.従来,暗号研究者らによる安全性証明の対象はアルゴリズムであり,実際に動作するプログラムではなかった一方,我々はアセンブリを直接扱いながら,暗号学的・形式的安全性証明が同時にできた.
3. より規模の大きい応用に向けて:組込みシステム用の低レベルプログラムは効率を考慮してコンパイラで生成せず,直接手で実装することが多い.そこで,我々は,低レベル記述による複雑さを省くために,疑似コードから半手動でアセンブリプログラムを構成する形式的アプローチを提案し,予備実験(2進互拡張除法の実装)を行った.
|
