Université de Rennes 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 Berkeley Packet FiltersCoqVérification formelleGénération de codeMachine virtuelle Berkeley Packet FiltersCoqFormal VerificationCode GenerationVirtual Machine Logiciels -- Vérification Systèmes d'exploitation (ordinateurs) 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. 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. Electronic Thesis or DissertationText en application/pdf1 : 4258 Kohttps://ged.univ-rennes1.fr/nuxeo/site/esupversions/3a499e48-42ec-46fa-8e46-cf8efa6bffc5 Yuan Shenghao 1994-09-28 CN 27504937X nuaaysh@126.com 2023URENS060 http://www.theses.fr/2023URENS060 2023-12-08 Informatique Université de Rennesthesis.degree.grantor_1 26693823X Doctorat non ouiTalpinJean-Pierreintervenant_1094211515BessonFrédéricintervenant_2070000182BlazySandrineintervenant_3153042567BaccelliEmmanuelintervenant_4111395380GrimaudGillesintervenant_5122743083ZhaoYongwangintervenant_6275053520 MATISSEecoleDoctorale_1 267602553 INRIA-RENNES partenaireRecherche_1 133175863 ddc:004 TalpinJean-PierreBessonFrédéricBlazySandrineBaccelliEmmanuelGrimaudGillesZhaoYongwangUniversité de RennesMATISSE INRIA-RENNES ASCII PDF 4360186