Apr 24 2009

Séminaire Marelle : Formal certification of ElGamal encryption: A gentle introduction to CertiCrypt

On Friday 24/04/2009, at 11h, in room Fermat Jaune.

Speaker: Sylvain Heraud.

Title: Formal certification of ElGamal encryption: A gentle introduction to CertiCrypt.

Abstract:
CertiCrypt is a framework that assists the construction of machine-checked cryptographic proofs that can be automatically verified by third parties. To date, CertiCrypt has been used to prove formally the exact security of widely studied cryptographic systems, such as the OAEP padding scheme and the Full Domain Hash digital signature scheme. The purpose of this article is to provide a gentle introduction to CertiCrypt. For concreteness, we focus on a simple but illustrative example, namely the semantic security of the Hashed ElGamal encryption scheme in both, the standard and the random oracle model.

PDF: http://www-sop.inria.fr/members/Sylvain.Heraud/paper/fast08.pdf

Apr 15 2009

Séminaire Marelle : Finite Group Representation Theory with Coq

On Wednesday 15/04/2009, at 10h30, in room Galois Coriolis.

Speaker: Sidi Ould Biha.

Title: Finite Group Representation Theory with Coq.

Abstract:
Representation theory is a branch of algebra that allows the study of groups through linear applications, i.e. matrices. Thus problems in abstract groups can be reduced to problems on matrices. Representation theory is the basis of character theory. In this paper we present a formalization of finite groups representation theory in the Coq system that includes a formalization of Maschke’s theorem on reducible finite group algebra.

Key-words: Representation theory, Maschke’s theorem, linear algebra, Coq, SSReflect.

URL: http://hal.inria.fr/inria-00377431/en/

Jan 30 2009

Séminaire Marelle : Formal certification of code-based cryptographic proofs

On Friday 30/01/2009, at 10h30, in room Fermat Jaune.

Speaker: Santiago Zanella Béguelin.

Title: Formal certification of code-based cryptographic proofs.

PDF: http://www-sop.inria.fr/members/Santiago.Zanella/Zanella.2009.POPL.pdf

Jan 09 2009

Séminaire Marelle : J.C. Filliatre: Queens on a Chessboard: an Exercise in Program Verification

On Friday 09/01/2009, at 10h30, in room Fermat Jaune.

Speaker: Laurent Théry.

Title: J.C. Filliatre: Queens on a Chessboard: an Exercise in Program Verification.

URL: http://why.lri.fr/queens/

Dec 19 2008

Séminaire Marelle : Connecting Grobner bases programs with Coq to do proofs in algebra, geometry and arithmetics

On Friday 19/12/2008, at 10h30, in room Galois Coriolis.

Speaker: Loïc Pottier.

Title: Connecting Grobner bases programs with Coq to do proofs in algebra, geometry and arithmetics.

PDF: http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-418/paper5.pdf

Dec 12 2008

Séminaire Marelle : Validation of Security Mechanisms for Embedded Systems

On Friday 12/12/2008, at 10h30, in room Fermat Jaune.

PhD Thesis of Dorina Ghindici (LIFL Lille), talk given by Yves Bertot.

Title: Validation of Security Mechanisms for Embedded Systems.

Abstract:
This thesis addresses the problem of information flow security in the context of mobile code. Our work aims at providing a solution to confidentiality issues in multiapplicative systems: ensuring security for an applications running on small and autonomous systems by verifying information flow properties at deployment time. Existing work on information flow does not scale to small open systems due to resources limitations and due to lack of modularity, which is essential in a dynamically evolving environment. In order to provide a complete solution, we address both practical and theoretical aspects. We first propose a model and a tool dedicated to small open systems running Java bytecode, with support for inheritance and override. Our approach is modular, hence the verification is incremental and is performed on the target device, the only place where the security can be guaranteed. To our knowledge, it is the first information flow verifier for embedded systems. Moreover, our model improves information flow usability in such systems by limiting the overhead for adding information flow security to a Java Virtual Machine. To prove its usability, we ran different experiments and we tested the tool in several contexts: on a case study from the literature, on an application for mobile phone, and in an integrated security validation and verification framework that spans the entire software lifecycle. Secondly, we tackle the information flow issue from a theoretical point of view. We propose a formal model, based on abstract memory graphs; an abstract memory graph is a points-to graph extended with nodes abstracting input values of primitive type and flows arising from implicit flow. Again, the model is modular, which allows incremental analysis and dynamic download of new programs. Our construction is proved correct with respect to non-interference. Contrary to most type-based approached, our abstract memory graph is build independently on any security level knowledge. Information flow is checked by labeling graphs a posteriori.