Frama-C for the Internet of Things

Frama-C is a framework for the static and dynamic analysis of ANSI-C programs. We explore the use of this framework for the formal verification of IoT software, in particular the Contiki lightweight operating system.

Our work include research work on the verification of Contiki and other IoT software, research work on extension of Frama-C to ease IoT verification, as well as tutorials on these topics.

Research Papers

Papers in Journals

Papers in Conference Proceedings

1. Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. Logic against ghosts: Comparison of two proof approaches for a list module. In ACM Symposium on Applied Computing (SAC), pages 2186-2195. ACM, 2019. Best Paper Award. doi
2. Allan Blanchard, Frédéric Loulergue, and Nikolai Kosmatov. Towards Full Proof Automation in Frama-C using Auto-Active Verification. In Nasa Formal Methods, LNCS, pages 88-105. Springer, 2019. doi
3. Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C. In Nasa Formal Methods, number 10811 in LNCS, pages 37-53. Springer, 2018. doi
4. Frédéric Loulergue, Allan Blanchard, and Nikolai Kosmatov. Ghosts for lists: from axiomatic to executable specifications. In Tests and Proofs (TAP), volume 10889 of LNCS, pages 177-184. Springer, 2018. doi

Code

Coming soon!

Tutorials

1. Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. Formal Verification for an Internet of Secured Things. In ACM SAC, Limassol, Cyprus, 2019, url
2. Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. Formal Verification of IoT Software with Frama-C. In 3rd World Congress on Formal Methods, Porto, Portugal, October 2019, url
3. Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. A lesson on verification of IoT software with Frama-C. In International Conference on High Performance Computing and Simulation (HPCS), pages 21–30, Orléans, France, 2018. IEEE. doi
4. Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. Towards reliable things: Formal verification of IoT software with Frama-C. 29th IEEE International Symposium on Software Reliability Engineering (ISSRE), 2018, url
5. Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. Secure your things: Secure development of IoT software with Frama-C. In IEEE Cybersecurity Development Conference (SecDev), pages 126-127. IEEE, 2018. doi
6. Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. Towards secure things, or how to verify IoT software with Frama-C. Zooming Innovation in Consumer Electronics International Conference (ZINC), 2018.