Verified programming and secure integration of operating system libraries in Coq
Programmation vérifiée et intégration sécurisée de bibliothèques de systèmes d’exploitation dans Coq
Résumé
As a revolutionary kernel extension technology, Berkeley Packet Filters (BPF) has been applied for various operating systems from different domains, from servers (Linux's extended BPF) to micro-controllers (RIOT-OS rBPF). The isolation of BPF virtual machines (VM) is critical to ensure system integrity against potentially malicious programs, especially for micro-controllers that rarely feature hardware memory protection. This thesis presents a trusted rBPF virtual machine that is formally proven fault-isolate in the Coq proof assistant. We present an end-to-end verification workflow for extracting verified executable C implementation from abstract rBPF models written in Coq. We also introduce Just-in-Time techniques into rBPF for performance optimization. All our proofs have been mechanized in Coq.
En tant que technologie révolutionnaire d'extension du noyau, Berkeley Packet Filters (BPF) a été appliqué à divers systèmes d'exploitation dans différents domaines, des serveurs (BPF étendu de Linux) aux micro-contrôleurs (rBPF de RIOT-OS). L'isolation des machines virtuelles BPF est essentielle pour garantir l'intégrité du système contre les programmes potentiellement malveillants, en particulier pour les microcontrôleurs qui disposent rarement d'une protection matérielle de la mémoire. Cette thèse présente une machine virtuelle rBPF de confiance dont l'isolation des fautes est formellement prouvée dans l'assistant de preuve Coq. Nous présentons un processus de vérification de bout en bout pour extraire une implémentation C exécutable vérifiée à partir de modèles rBPF abstraits écrits en Coq. Nous introduisons également des techniques Just-in-Time dans rBPF pour l'optimisation des performances. Nos preuves sont toutes vérifiées mécaniquement dans Coq.
Origine : Version validée par le jury (STAR)