{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T16:37:02Z","timestamp":1743093422922,"version":"3.40.3"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031131875"},{"type":"electronic","value":"9783031131882"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T00:00:00Z","timestamp":1659744000000},"content-version":"vor","delay-in-days":217,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>RIOT is a micro-kernel dedicated to IoT applications that adopts eBPF (extended Berkeley Packet Filters) to implement so-called femto-containers. As micro-controllers rarely feature hardware memory protection, the isolation of eBPF virtual machines (VM) is critical to ensure system integrity against potentially malicious programs. This paper shows how to directly derive, within the Coq proof assistant, the verified C implementation of an eBPF virtual machine from a Gallina specification. Leveraging the formal semantics of the CompCert C compiler, we obtain an end-to-end theorem stating that the C code of our VM inherits the safety and security properties of the Gallina specification. Our refinement methodology ensures that the isolation property of the specification holds in the verified C implementation. Preliminary experiments demonstrate satisfying performance.<\/jats:p>","DOI":"10.1007\/978-3-031-13188-2_15","type":"book-chapter","created":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T08:16:57Z","timestamp":1659687417000},"page":"293-316","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["End-to-End Mechanized Proof of\u00a0an\u00a0eBPF Virtual Machine for\u00a0Micro-controllers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8467-5827","authenticated-orcid":false,"given":"Shenghao","family":"Yuan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6815-0652","authenticated-orcid":false,"given":"Fr\u00e9d\u00e9ric","family":"Besson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0556-4265","authenticated-orcid":false,"given":"Jean-Pierre","family":"Talpin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Samuel","family":"Hym","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Koen","family":"Zandberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6239-9983","authenticated-orcid":false,"given":"Emmanuel","family":"Baccelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,8,6]]},"reference":[{"unstructured":"Anand, A., et al.: Certicoq : a verified compiler for Coq. In: CoqPL (2017)","key":"15_CR1"},{"doi-asserted-by":"crossref","unstructured":"Appel, A.W., et al.: Program logics for certified compilers. In: CUP (2014)","key":"15_CR2","DOI":"10.1017\/CBO9781107256552"},{"doi-asserted-by":"crossref","unstructured":"Baccelli, E., et al.: RIOT: an open source operating system for low-end embedded devices in the IoT. IoT J. 5(6), 4428\u20134440 (2018)","key":"15_CR3","DOI":"10.1109\/JIOT.2018.2815038"},{"doi-asserted-by":"publisher","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development. In: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-662-07964-5","key":"15_CR4","DOI":"10.1007\/978-3-662-07964-5"},{"unstructured":"Bond, B., et al.: Vale: verifying high-performance cryptographic assembly code. In: USENIX Security, pp. 917\u2013934 (2017)","key":"15_CR5"},{"unstructured":"Costan, V., Lebedev, I., Devadas, S.: Sanctum: minimal hardware extensions for strong software isolation. In: USENIX Security, pp. 857\u2013874. USENIX (2016)","key":"15_CR6"},{"doi-asserted-by":"crossref","unstructured":"Desharnais, M., Brunthaler, S.: Towards efficient and verified virtual machines for dynamic languages. In: CPP, pp. 61\u201375. ACM (2021)","key":"15_CR7","DOI":"10.1145\/3410273"},{"doi-asserted-by":"publisher","unstructured":"Dunchev, C., Guidi, F., Sacerdoti Coen, C., Tassi, E.: ELPI: fast, embeddable, $$\\lambda $$ prolog interpreter. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 460\u2013468. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_32","key":"15_CR8","DOI":"10.1007\/978-3-662-48899-7_32"},{"doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 Where Programs Meet Provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8","key":"15_CR9","DOI":"10.1007\/978-3-642-37036-6_8"},{"unstructured":"Fleming, M.: A thorough introduction to eBPF. Linux Weekly News (2017)","key":"15_CR10"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"564","DOI":"10.1007\/978-3-030-53291-8_29","volume-title":"Computer Aided Verification","author":"J Van Geffen","year":"2020","unstructured":"Van Geffen, J., Nelson, L., Dillig, I., Wang, X., Torlak, E.: Synthesizing JIT compilers for In-Kernel DSLs. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 564\u2013586. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_29"},{"unstructured":"Gu, R., et al.: Certikos: an extensible architecture for building certified concurrent os kernels. In: OSDI, pp. 653\u2013669. USENIX (2016)","key":"15_CR12"},{"doi-asserted-by":"crossref","unstructured":"Haas, A., et al.: Bringing the web up to speed with webassembly. In: PLDI, pp. 185\u2013200. ACM (2017)","key":"15_CR13","DOI":"10.1145\/3140587.3062363"},{"issue":"5","key":"15_CR14","first-page":"720","volume":"3","author":"O Hahm","year":"2016","unstructured":"Hahm, O., Baccelli, E., Petersen, H., Tsiftes, N.: Operating systems for low-end devices in the Internet of Things: a survey. IoT J. 3(5), 720\u2013734 (2016)","journal-title":"IoT J."},{"doi-asserted-by":"crossref","unstructured":"Jomaa, N., Torrini, P., Nowak, D., Grimaud, G., Hym, S.: Proof-oriented design of a separation kernel with minimal trusted computing base. In: AVOCS, vol. 76. Electronic Communications of the EASST (2018)","key":"15_CR15","DOI":"10.1016\/j.scico.2017.06.012"},{"doi-asserted-by":"crossref","unstructured":"Jourdan, J.H., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: POPL, pp. 247\u2013259. ACM (2015)","key":"15_CR16","DOI":"10.1145\/2775051.2676966"},{"doi-asserted-by":"crossref","unstructured":"Klein, G., et al.: seL4: formal verification of an OS kernel. In: SOSP, p. 207. ACM Press (2009)","key":"15_CR17","DOI":"10.1145\/1629575.1629596"},{"issue":"7","key":"15_CR18","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"unstructured":"Leroy, X., Appel, A.W., Blazy, S., Stewart, G.: The CompCert Memory Model, Version 2. Research Report RR-7987, INRIA (2012)","key":"15_CR19"},{"issue":"1","key":"15_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-008-9099-0","volume":"41","author":"X Leroy","year":"2008","unstructured":"Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program transformations. JAR 41(1), 1\u201331 (2008)","journal-title":"JAR"},{"doi-asserted-by":"publisher","unstructured":"Letouzey, P.: A new extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 200\u2013219. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-39185-1_12","key":"15_CR21","DOI":"10.1007\/3-540-39185-1_12"},{"unstructured":"Li, S.W., Li, X., Gu, R., Nieh, J., Hui, J.Z.: Formally verified memory protection for a commodity multiprocessor hypervisor. In: USENIX Security, pp. 3953\u20133970. USENIX (2021)","key":"15_CR22"},{"unstructured":"Lochbihler, A.: A machine-checked, type-safe model of Java concurrency: language, virtual machine, memory model, and verified compiler. Ph.D. thesis, Karlsruhe Institute of Technology (2012)","key":"15_CR23"},{"doi-asserted-by":"crossref","unstructured":"Madhavapeddy, A., et al.: Unikernels: library operating systems for the cloud. In: ASPLOS, pp. 461\u2013472. ACM (2013)","key":"15_CR24","DOI":"10.1145\/2499368.2451167"},{"unstructured":"McCanne, S., Jacobson, V.: The BSD packet filter: a new architecture for user-level packet capture. In: Usenix Winter Conference, vol. 46, pp. 259\u2013270. USENIX (1993)","key":"15_CR25"},{"doi-asserted-by":"crossref","unstructured":"Mogul, J., Rashid, R., Accetta, M.: The packer filter: an efficient mechanism for user-level network code. In: SOSP, pp. 39\u201351. ACM (1987)","key":"15_CR26","DOI":"10.1145\/37499.37505"},{"doi-asserted-by":"crossref","unstructured":"Mullen, E., Pernsteiner, S., Wilcox, J.R., Tatlock, Z., Grossman, D.: \u0152uf: minimizing the Coq extraction TCB. In: CPP, pp. 172\u2013185. ACM (2018)","key":"15_CR27","DOI":"10.1145\/3167089"},{"doi-asserted-by":"crossref","unstructured":"Myreen, M.O.: Verified just-in-time compiler on x86. In: POPL, pp. 107\u2013118. ACM (2010)","key":"15_CR28","DOI":"10.1145\/1707801.1706313"},{"unstructured":"Nelson, L., Geffen, J.V., Torlak, E., Wang, X.: Specification and verification in the field: applying formal methods to BPF just-in-time compilers in the Linux kernel. In: OSDI, pp. 41\u201361. USENIX (2020)","key":"15_CR29"},{"unstructured":"Noorman, J., et al.: Sancus: low-cost trustworthy extensible networked devices with a zero-software trusted computing base. In: USENIX Security, pp. 479\u2013498. USENIX (2013)","key":"15_CR30"},{"unstructured":"Pit-Claudel, C., Philipoom, J., Jamner, D., Erbsen, A., Chlipala, A.: Relational compilation for performance-critical applications. In: PLDI. ACM (2022)","key":"15_CR31"},{"key":"15_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Pnueli","year":"1998","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 151\u2013166. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0054170"},{"key":"15_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-030-39322-9_3","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Porncharoenwase","year":"2020","unstructured":"Porncharoenwase, S., Bornholt, J., Torlak, E.: Fixing code that explodes under symbolic evaluation. In: Beyer, D., Zufferey, D. (eds.) VMCAI 2020. LNCS, vol. 11990, pp. 44\u201367. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-39322-9_3"},{"doi-asserted-by":"publisher","unstructured":"Protzenko, J., et al.: Verified low-level programming embedded in F*. In: PACMPL 1(ICFP), pp. 17:1\u201317:29 (2017). https:\/\/doi.org\/10.1145\/3110261","key":"15_CR34","DOI":"10.1145\/3110261"},{"doi-asserted-by":"publisher","unstructured":"Rizkallah, C., et al.: A framework for the automatic formal verification of refinement from Cogent to C. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 323\u2013340. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-43144-4_20","key":"15_CR35","DOI":"10.1007\/978-3-319-43144-4_20"},{"doi-asserted-by":"crossref","unstructured":"Tanaka, A.: Coq to C translation with partial evaluation. In: PEPM@POPL, pp. 14\u201331. ACM (2021)","key":"15_CR36","DOI":"10.1145\/3441296.3441394"},{"unstructured":"Tassi, E.: Coq-Elpi, Coq plugin embedding Elpi (2021). https:\/\/github.com\/LPCIC\/coq-elpi","key":"15_CR37"},{"doi-asserted-by":"crossref","unstructured":"Zandberg, K., Baccelli, E.: Minimal virtual machines on IoT microcontrollers: the case of Berkeley Packet Filters with rBPF. In: PEMWN, pp. 1\u20136. IEEE (2020)","key":"15_CR38","DOI":"10.23919\/PEMWN50727.2020.9293081"},{"doi-asserted-by":"crossref","unstructured":"Zandberg, K., Baccelli, E.: Femto-Containers: DevOps on Microcontrollers with Lightweight Virtualization & Isolation for IoT Software Modules (2021), preprint","key":"15_CR39","DOI":"10.1145\/3528535.3565242"},{"doi-asserted-by":"publisher","unstructured":"Zhang, X., Li, Y., Sun, M.: Towards a formally verified EVM in\u00a0production environment. In: Bliudze, S., Bocchi, L. (eds.) COORDINATION 2020. LNCS, vol. 12134, pp. 341\u2013349. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-50029-0_21","key":"15_CR40","DOI":"10.1007\/978-3-030-50029-0_21"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13188-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,13]],"date-time":"2023-02-13T19:25:06Z","timestamp":1676316306000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13188-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131875","9783031131882"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13188-2_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"6 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The source code and proofs of our virtual machine, its generated code and benchmark data are available on.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Artifacts"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"209","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.9","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9.7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}