Point of contact
Virgile Prevosto, CEA List
Summary
Historically, formal methods have mostly focused on proving safety properties of critical embedded systems, which were relatively isolated. With the advent of IoT, it becomes more and more important to be able to specify security (i.e. confidentiality, integrity, availability, …) and privacy properties, and to verify that programs are conforming to these specifications. While the underlying analysis techniques are mostly the same, the kind of properties to be investigated can be quite different and warrant further research.
A few references
- Carmine Abate et al. Trace-Relating Compiler Correctness and Secure Compilation. In 29th European Symposium on Programming (ESOP). 2020
- Lesly-Ann Daniel, Sébastien Bardin, Tamara Rezk. Binsec/Rel: Efficient Relational Symbolic Execution for Constant-Time at Binary-Level. In 41st IEEE Symposium on Security and Privacy. 2020
- J. Almeida et al. Machine-checked proofs for cryptographic standards: Indifferentiability of Sponge and secure high-assurance implementations of SHA-3. In ACM SIGSAC Conference on Computer and Communications Security (CCS), 2019
- Virgile Robles et al. MetAcsl: Specification and Verification of High-Level Properties. In 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems,(TACAS). 2019