Verified information flow control applied to cyber-physical systems
Contrôle vérifié de flux d'information appliqué aux systèmes cyber-physiques
Résumé
Computing has become omnipresent in daily life through tools that are technologically enriched and increasingly connected to the Internet. When these objects stop working due to a combination of circumstances, it can have dramatic consequences on the safety of people who depend on them. Their functioning can also be altered by a malicious will to harm and which, during an attack, will create a situation conducive to a targeted malfunction. In this work, we explore the use of formal methods in an embedded and cyber-physical environment. First, we use F* to model the safety of programs on an Arduino. In a second step, we implement LIO (Library Input Output) in F* in a system or embedded context. We put forward an approach that allows to choose between a static verification and a dynamic verification in order to reduce the proof load or the cost at runtime. We also propose a mechanization of the non-interference proof using metaprogramming. This proof focuses on the interaction between the program and the library rather than on the library only.
L’informatique est devenue omniprésente dans la vie de tous les jours au travers d’outils de plus en plus riches technologiquement et de plus en plus connectés à internet. Lorsque ces objets arrêtent de fonctionner suite à un concours de circonstances, cela peut avoir des conséquences dramatiques sur la sûreté des personnes qui en dépendent. Leur fonctionnement peut être aussi altéré par une volonté malveillante de nuire et qui lors d’une attaque créera la situation propice à un dysfonctionnement ciblé. Dans ce travail, nous explorons l’utilisation des méthodes formelles dans un environnement embarqué et cyber-physique. Dans un premier temps, nous utilisons F* pour modéliser la sûreté des programmes sur une Arduino. Puis nous implémentons LIO (Library Input Output) en F* dans un contexte système ou embarqué. Nous mettons ici en avant une approche qui permet de choisir entre une vérification statique et une vérification dynamique afin de réduire la charge de preuve ou le coût à l’exécution. Nous proposons également une mécanisation de la preuve de non-interférence en utilisant la métaprogrammation. Cette preuve porte sur l’interaction entre le programme et la librairie plutôt que sur la librairie seulement.
Origine : Version validée par le jury (STAR)