Cet article présente un retour d’expérience lié à un enseignement de Frama-C pour la cybersécurité dispensé dans plusieurs formations d’ingénieurs et universitaires de niveau master. Il est constitué d’un cours et d’un TP de trois heures chacun. Frama-C est une plateforme open source fournissant des analyseurs de code C. Le cours est articulé autour de ses trois techniques et analyseurs principaux, à savoir la vérification déductive avec Wp, l’interprétation abstraite avec Eva, et la vérification d’annotations à l’exécution avec E-ACSL. Le but du cours est de faire découvrir ces techniques formelles aux étudiants en insistant sur leurs aspects pratiques en cybersécurité.

This paper is a tutorial introduction to Frama-C, a framework for the analysis and verification of sequential C programs, and in particular its EVA, WP, and E-ACSL plugins. The examples are drawn from Contiki, a lightweight operating system for the Internet of Things.

Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static and dynamic analysis for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel, and their compliance to a common specification language, ACSL.

This paper presents a three-hour tutorial on Frama-C in which we provide a comprehensive overview of its most important plug-ins: the abstract-interpretation based plug-in Value, the deductive verification tool WP, the runtime verification tool E-ACSL and the test generation tool PathCrawler. We also emphasize different possible collaborations between these plug-ins and a few others. The presentation is illustrated on concrete examples of C programs

• Frama-C Overview: Slides, Simple plugin
• Value Analysis: Slides and Examples
• WP: Slides and Examples

Examples