This article presents my feedback on introducing Frama-C for cybersecurity in several engineering and master’s level university courses. It consists of a single lecture and a single lab session. Frama-C is an open source platform providing C code analyzers based on formal methods. The course focuses on its three main techniques provided through dedicated analyzers, namely deductive verification with Wp, abstract interpretation with Eva, and runtime annotation verification with E-ACSL. The aim of the course is to introduce students to these formal techniques, emphasizing their practical aspects in cybersecurity.

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