La vérification formelle de programmes est une méthode fortement désirée dans l'élaboration et la vérification de systèmes informatiques, et tout particulièrement dans le cas de systèmes d'exploitation. En effet, garantir certaines propriétés une fois pour toutes dans des briques de bases sur lesquelles reposent un ensemble considérable d'applications va de soi.

Un langage récent, Rust, a bousculé la programmation système par sa capacité à fournir des abstractions de haut niveau et de la sécurité mémoire sans surcoûts à l'exécution tout en maintenant un niveau de performance comparable à C/C++. Par conséquent, de nombreux outils de vérification de programmes Rust ont vu le jour ces quelques dernières années.

Dans ma présentation, je donnerai un aperçu de Rust et de la vérification déductive, la méthode de vérification formelle choisie, en illustrant cela par la vérification à l'aide de Creusot, un outil de traduction vers la plateforme de vérification déductive Why3, d'un driver Bluetooth dans le système d'exploitation embarqué tockOS.

----------------------------------------------------------------------

Formal verification is a highly sought-after method in the development and verification of computer systems, peculiarly in the case of operating systems. Indeed, it goes without saying that certain properties must be guaranteed once and for all in the foundational building blocks upon which a vast array of applications relies.

A recent language, Rust, has revolutionized system programming with its ability to provide high-level abstractions and memory safety without additional runtime overhead, while maintaining a performance level comparable to C/C++. Consequently, numerous Rust program verification tools have emerged in recent years.

In my presentation, I will provide an overview of Rust and deductive verification, the chosen formal verification method, illustrating this through the verification of a Bluetooth driver in an embedded operating system using Creusot, a tool that translates code to the why3 deductive verification platform.