![[HTTP Mutual Access Authentication]](/files/special/MutualAuth/index-en/mutual.png)
![[Fail-Safe C]](/files/project/FailSafeC-ja/FSC-logo.png){kind=logo}
![[暗号モジュールの物理解析攻撃]](/special/SASEBO/SASEBO_banner.png)
![[LR-AKE]](/files/project/LRAKE-en/renew8.gif)
![[QR-JAM]](/files/project/index-ja/qr-jam-150.jpg)
![[Knoppix-JA]](/files/project/index-ja/knoppix-j.PNG)
ソフトウェア安全性のための論理検証技術
概要
セキュリティに関わるソフトウェアやシステムに対しては、提供されるセキュ リティ保証を的確に評価することが必要不可欠です。形式的検証は、セキュリ ティ保証の評価手法の中で最も厳密な、従って最も信頼度の高い技術です。 形式的検証とは、一口で言えば、数学的主張に対する証明を、コンピュータ上 で検証可能な形で与えることです。システムに求められるセキュリティ仕様は、 そのシステムについての数学的言明と見做すことができます。我々は、セキュ リティ仕様をいかにして数学的に記述するか、そして、それをいかにして形式 的に証明するかについての研究を行っています。 具体的には、仕様記述のための形式的言語や、それらを応用してのソフトウェ アや暗号プロトコルの形式的検証についての研究に取り組んでいます。
担当研究者
- Reynald Affeldt
- 山田 聖
- David Nowak
- 田中 三貴
主な研究成果
- Reynald Affeldt, David Nowak, and Kiyoshi Yamada. Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS. AVoCS 2009. Article. 日本語での概要.
- Reynald Affeldt and Hubert Comon-Lundh. Verification of Security Protocols with a Bounded Number of Sessions based on Resolution for Rigid Variables. Formal to Practical Security, LNCS 5458, May 2009. (c)Springer. Springer online. Preprint.
- Nicolas Marti and Reynald Affeldt. A Certified Verifier for a Fragment of Separation Logic. Computer Software, 25(3):135-147, July 2008. Preprint.
- Reynald Affeldt, Miki Tanaka, and Nicolas Marti. Formal Proof of Provable Security by Game-playing in a Proof Assistant. Provsec 2007, LNCS 4784. (c)Springer. Springer online. Preprint. 日本語での概要.
- David Nowak. A Framework for Game-Based Security Proofs. ICICS 2007, LNCS 4861. Cryptology ePrint Archive: Report 2007/199.
- Stephane Demri and David Nowak. Reasoning about transfinite sequences. International Journal of Foundations of Computer Science, 18(1):87-112, February 2007. Preprint
- Stephane Demri, Ranko Lazic, and David Nowak. On the freeze quantifier in Constraint LTL: decidability and complexity. Information and Computation, 205(1):2-24, January 2007. Preprint
- Reynald Affeldt and Nicolas Marti. An approach to formal verification of arithmetic functions in assembly. ASIAN 2006, LNCS 4435. (c)Springer. Springer online. Preprint.
- Slawomir Lasota, David Nowak, and Yu Zhang. On completeness of logical relations for monadic types. ASIAN 2006, LNCS 4435.
- Nicolas Marti, Reynald Affeldt, and Akinori Yonezawa. Formal verification of the heap manager of an operating system using separation logic. ICFEM 2006. LNCS 4260. (c) Springer. Springer online. Preprint
- Reynald Affeldt and David Nowak. Application of formal verification to software security. ISSS 2006. Slides and examples
- Reynald Affeldt and Nicolas Marti. Seplog: a Coq implementation of separation logic and its application to verification of low-level programs.