PACSS (Archive)

VERIMAG/PACSS team is led by David Monniaux and Marie-Laure Potet

The PACSS team (Proofs and Code analysis for Safety and Security) develops methods and tools for helping analysis and verification of programs by mathematical means. Properties that are targeted are correctness, absence of runtime error or security properties.

The PACSS team was formed in 2015 following the reorganization of VERIMAG. Previously, scientists from both the DCS and the SYNCHRONE teams worked on shared topics ; it made sense that they should be in the same team.

Research topics are the following ones :

Abstract interpretation and decision procedures

Proofs of correctness using Coq

Verification by automata and acceleration-based approaches

Code analysis for vulnerability detection We develop code analysis tools in order to evaluate source or low-level code. We aim two types of diagnostic : robustness or vulnerabilty detection. We consider both source and low-level code. Our approach is based on a combination of static analyses and concolic execution. More on this topic

Security properties evaluation In the domain of security, verification is generally declined as robustness criteria and must be led against attacker models. We propose tools and technics dedicated to the evaluation of secure devices (smartcard or secured dongle) against fault attacks (such as laser or electromagnetic attacks). We are also interested for modeling and verifying other security requirements (confidentiality, integrity, isolation...) in particular in the context of Common Criteria certification. More on this topic