ソフトウェア安全性のための論理検証技術
概要・研究の背景
セキュリティに関わるソフトウェアやシステムに対しては、提供されるセキュ リティ保証を的確に評価することが必要不可欠です。形式検証は、セキュリ ティ保証の評価手法の中で最も厳密な、従って最も信頼度の高い技術です。 形式検証とは、一口で言えば、数学的主張に対する証明を、コンピュータ上 で検証可能な形で与えることです。システムに求められるセキュリティ仕様は、 そのシステムについての数学的言明と見做すことができます。我々は、セキュ リティ仕様をいかにして数学的に記述するか、そして、それをいかにして形式的に証明するかについての研究を行っています。 具体的には、仕様記述のための形式的言語や、それらを応用してのソフトウェアや暗号プロトコルの形式検証についての研究に取り組んでいます。我々は、形式検証のために、主に定理証明支援系 Coqを使っています。
| 定理証明支援系Coqのよる形式検証の流れ： |
|---|
 |
研究内容
ソフトウェアのソースコードの形式検証
組込みシステムの普及に伴い、低レベルプログラムのソースコード安全性の保証に対する重要性が高まっている。国際規格において、最も厳密な評価保証レベルは形式検証である。 しかし、現状では、形式検証で大規模なプログラムを扱い辛い。一方、低レベルプログラムの特徴である詳細なメモリ操作のために研究レベルでは分離論理という形式手法が提案されている。本研究では、分離論理に基づく形式検証の環境を構築し、現実的なケーススタディ（ICカード用のアセンブリ言語の疑似乱数生成器、暗号スキームの実装に欠かせない２進拡張互除法を含む符号付き多倍長整数処理の関数、通信プロトコルの実装）でその検証環境の実用性を実証する。追加情報
情報理論・符号理論の形式化
通信の特性は情報の理論で記述されるが、その最も基本的な結果がシャノンの 定理である。シャノンの定理の証明は単純ではなく、証明の詳細は入門書でも あまり述べられない。これは好ましくない状況である。なぜなら、コンピュー タセキュリティの重要な結果は情報理論を安全性根拠（無条件安全性など）と しているからである。本発表では、証明支援系 Coq上での情報理論の形式定義 や補題のライブラリを構成に関して報告する。今回構成するライブラリの有用 性を示す結果として、圧縮と誤り訂正に関するシャノンの定理の形式的証明を 世界で最初に提供する。追加情報
担当研究者
- AFFELDT Reynald
- 坂口 和彦
主な研究成果
- アフェルト レナルド. チュートリアル:定理証明支援系Coq入門. 日本ソフトウェア科学会 第31回大会. 2014.09.07. 日本ソフトウェア科学会. online
- Reynald Affeldt and Kazuhiko Sakaguchi. An Intrinsic Encoding of a Subset of C and its Application to TLS Network Packet Processing. Journal of Formalized Reasoning, 7(1):63-104, 2014. online
- Reynald Affeldt, Manabu Hagiwara, Jonas Senizergues. Formalization of Shannon's Theorems. Journal of Automated Reasoning, 53(1):63-103, 2014. Springer. online
- Reynald Affeldt. On Construction of a Library of Formally Verified Low-level Arithmetic Functions. Innovations in Systems and Software Engineering, 9(2):59-77, 2013. NASA/Springer. online
- Reynald Affeldt, David Nowak, and Kiyoshi Yamada. Certifying Assembly with Formal Security Proofs: the Case of BBS. Science of Computer Programming, 77(10-11):1058-1074, 2012. Elsevier. online