Improving Digital Systems Security Evaluation


Sound Static Analysis of Regular Expressions for Vulnerabilities to Denial of Service Attacks.

F. Parolini and A. Miné

Binsec/Rel : Symbolic Binary Analyzer for Security with Applications to Constant-Time and Secret-Erasure.

Lesly-Ann Daniel, Sébastien Bardin, Tamara Rezk.

Introducing Robust Reachability.

Guillaume Girol, Benjamin Farinier, Sébastien Bardin

BAXMC: a CEGAR approach to Max#SAT

Thomas Vigouroux , Cristian Ene, David Monniaux , Laurent Mounier, Marie-Laure Potet

PROSPECT: Provably Secure Speculation for the Constant-Time Policy

Lesly-Ann Daniel, Marton Bognar, Job Noorman, Sébastien Bardin, Tamara Rezk, Frank Piessens

Adversarial Reachability for Program-level Security Analysis

Soline Ducousso, Sébastien Bardin, Marie-Laure Potet.

A generic framework to develop and verify security mechanisms at the microarchitectural level: application to control-flow integrity

Matthieu Baty, Pierre Wilke, Guillaume Hiet, Alix Trieu, Arnaud Fontaine