| 研究概要 |
組込みシステムの普及に伴い,低レベルプログラムの安全性の保証に対する重要性が高まっている.国際規格において,最も厳密な評価保証レベルは形式検証である.しかし,現状では,形式検証で大規模なプログラムを扱い辛い.一方,低レベルプログラムの特徴である詳細なメモリ操作のために研究レベルでは分離論理という形式手法が提案されている.本研究では,分離論理に基づく形式検証の環境を構築し,現実的なケーススタディ(ICカード用のアセンブリ言語の疑似乱数生成器,暗号スキームの実装に欠かせない2進拡張互除法を含む符号付き多倍長整数処理の関数)でその検証環境の実用性を実証した.
|
