Séminaires
Séminaire du 26 janvier 2018
Lieu
LIP6. Instructions pour venir ici.
Programme
14h00-15h00: Yann Thierry-Mieg (LIP6), Multi-solution model-checking with Guarded Action Language.
Abstract : In recent years we developped a pivot language called GAL for expressing semantics of concurrent systems. This language plays the role of pivot in a multi-solution architecture for model-checking and verification. We have implemented translations from several popular formalisms and a few Domain Specific Languages to GAL. Historically we used our set decision diagram SDD based engine to perform model-checking of GAL specifications. We now have also built solutions based on SMT solvers and adapters for the LTSmin (multi-solution) model-checker. In this talk we will give an overview of this architecture and some of its applications, and zoom on the more recently added SMT based solutions.
15h00-15h30 : Inès Ben El Ouahma(LIP6), Symbolic approach for side-channel resistance analysis of masked assembly codes
Abstract :
Masking is a popular countermeasure against side-channel attacks, which
randomizes secret data with random and uniform variables called masks.
At software level, masking is usually added in the source code and its
effectiveness needs to be verified. This talk presents a symbolic method
to verify side-channel robustness of masked programs. The analysis is
performed at the assembly level since compilation and optimisations may
alter the added protections. Our proposed method aims to verify that
intermediate computations are statistically independent from secret
variables using defined distribution inference rules. For example we
verify the first round of a masked AES and show that some secure
algorithms or source codes are not leakage-free in their assembly
implementations.