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
