LIP6. Instructions pour venir ici.
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.
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.