PACS

The PACS group (for “Proofs and Code Analyses for Security” in French) develops code analysis techniques and tools for software security. We address both source-level and low-level codes, and we study effective combinations of static and dynamic analysis techniques (abstract interpretation, compilation, concolic execution, fuzzing and even a bit of formal proofs). We currently focus on the following research areas.

Code robustness against fault injections Security of embedded systems like smart-cards, secured dongles and IoTs relies on the robustness of devices against physical fault attacks (such as laser or electromagnetic attacks). Current certification schemes (e.g., Common Criteria) require protection mechanisms against multi-fault injection attacks. Typically, these protections often consist in “Counter-Measures”: monitors which perform redundant computations in order to detect/prevent some attacks.

For a given system, such kind of attacks leads to an exponential number of unintended behaviors. In order to help both developers and auditors to master this complexity, we aim to propose faithful fault models and automated code analysis taking into account the impact of physical attacks. More on this topic.

Vulnerability detection and analysis We develop static analysis for binary level code dedicated to vulnerability detection like “Use-After-Free” or “Buffer overflows”. Such software bugs may indeed exploited in software attacks. More on this topic.

Non-interference and side-channel attacks “Side-channel attacks” consists in observing several executions (typically, running times) of an information system in order to infer some information about secret data. Constant-time programming is a standard countermeasure against such attacks. We have studied how to relax this policy by proving that the program does not leak more information than the intended public output. More on this topic.

Security of Industrial Control Systems Industrial Control Systems (e.g. SCADA and PLC) are mostly based on proprietary infrastructures and legacy software. Because of this specificity, despite the fact that their security is critical, these systems have been less studied in the literature. Within the FUI Aramis project, we proposed an end-to-end approach to take into account applicative filtering rules for industrial protocols, dealing both with safety and security concerns. More on this topic.

Security Countermeasures into Formally Verified Compilers CompCert is a moderately optimizing C compiler, with a formal proof of functional correctness in the Coq proof assistant. We aim also to study how to adapt this formal proof, in order to ensure that countermeasures added manually by programmers are indeed useful (in particular, their are not removed by the optimization pass). We also study how security countermeasures can automatically be added by the compiler (while preserving the formal proof of correctness). More on this topic.