4 papers
Systematic Timing Leakage Analysis of NIST PQDSS Candidates: Tooling and Lessons Learned
Olivier Adjonyo, Sebastien Bardin, Emanuele Bellini +5
The PQDSS standardization process requires cryptographic primitives to be free from vulnerabilities, including timing and cache side-channels. Resistance to timing leakage is there…
A Systematic Evaluation of Automated Tools for Side-Channel Vulnerabilities Detection in Cryptographic Libraries
Antoine Geimer, Mathéo Vergnolle, Frédéric Recoules +3
To protect cryptographic implementations from side-channel vulnerabilities, developers must adopt constant-time programming practices. As these can be error-prone, many side-channe…
Interface Compliance of Inline Assembly: Automatically Check, Patch and Refine
Frédéric Recoules, Sébastien Bardin, Richard Bonichon +3
Inline assembly is still a common practice in low-level C programming, typically for efficiency reasons or for accessing specific hardware resources. Such embedded assembly codes i…
Get rid of inline assembly through verification-oriented lifting
Frédéric Recoules, Sébastien Bardin, Richard Bonichon +2
Formal methods for software development have made great strides in the last two decades, to the point that their application in safety-critical embedded software is an undeniable s…