{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,29]],"date-time":"2026-10-29T06:18:23Z","timestamp":1793254703411,"version":"4.5.0"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656262","type":"print"},{"value":"9783031656279","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Modern operating systems have adopted Berkeley Packet Filters (BPF) as a mechanism to extend kernel functionalities dynamically, <jats:italic>e.g.,<\/jats:italic> Linux\u2019s eBPF or RIOT\u2019s rBPF. The just-in-time (JIT) compilation of eBPF introduced in Linux eBPF for performance has however led to numerous critical issues. Instead, RIOT\u2019s rBPF uses a slower but memory-isolating interpreter (a virtual machine) which implements a defensive semantics of BPF; and therefore trades performance for security. To increase performance without sacrificing security, this paper presents a fully verified JIT implementation for RIOT\u2019s rBPF, consisting of: i\/ an end-to-end refinement workflow to both proving the JIT correct from an abstract specification and by deriving a verified concrete C implementation; ii\/ a symbolic CompCert interpreter for executing  binary code; iii\/ a verified JIT compiler for rBPF; iv\/ a verified hybrid rBPF virtual machine. Our core contribution is, to the best of our knowledge, the first and fully verified rBPF JIT compiler with correctness guarantees from high-level specification to low-level implementation. Benchmarks on microcontrollers hosting the RIOT operating system demonstrate significant performance improvements over the existing implementations of rBPF, even in worst-case application scenarios.<\/jats:p>","DOI":"10.1007\/978-3-031-65627-9_16","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T19:01:31Z","timestamp":1721934091000},"page":"325-347","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["End-to-End Mechanized Proof of\u00a0a\u00a0JIT-Accelerated eBPF Virtual Machine for\u00a0IoT"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8467-5827","authenticated-orcid":false,"given":"Shenghao","family":"Yuan","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6815-0652","authenticated-orcid":false,"given":"Fr\u00e9d\u00e9ric","family":"Besson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0556-4265","authenticated-orcid":false,"given":"Jean-Pierre","family":"Talpin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"16_CR1","unstructured":"Anand, A., et al.: CertiCoq : a verified compiler for Coq. In: CoqPL (2017)"},{"issue":"6","key":"16_CR2","first-page":"4428","volume":"5","author":"E Baccelli","year":"2018","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)","journal-title":"IoT-J"},{"key":"16_CR3","doi-asserted-by":"publisher","unstructured":"Barri\u00e8re, A., Blazy, S., Fl\u00fcckiger, O., Pichardie, D., Vitek, J.: Formally verified speculation and deoptimization in a JIT compiler. Proc. ACM Program. Lang. 5(POPL), 26 (2021). https:\/\/doi.org\/10.1145\/3434327","DOI":"10.1145\/3434327"},{"key":"16_CR4","doi-asserted-by":"publisher","unstructured":"Barri\u00e8re, A., Blazy, S., Pichardie, D.: Formally verified native code generation in an effectful JIT: Turning the CompCert backend into a formally verified JIT compiler. Proc. ACM Program. Lang. 7(POPL), 249\u2013277 (2023). https:\/\/doi.org\/10.1145\/3571202","DOI":"10.1145\/3571202"},{"key":"16_CR5","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions. Springer (2013)"},{"key":"16_CR6","doi-asserted-by":"publisher","unstructured":"Bratman, H.: A alternate form of the \u201cuncol diagram\u201d. Commun. ACM 4(3), 142 (1961). https:\/\/doi.org\/10.1145\/366199.366249","DOI":"10.1145\/366199.366249"},{"key":"16_CR7","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)","DOI":"10.1145\/3410273"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/978-3-662-48899-7_32","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C Dunchev","year":"2015","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":"16_CR9","unstructured":"Fleming, M.: A Thorough Introduction to eBPF. Linux Weekly News (2017)"},{"key":"16_CR10","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"},{"key":"16_CR11","unstructured":"Gu, R., et al.: CertiKOS: an extensible architecture for building certified concurrent OS kernels. In: OSDI, pp. 653\u2013669. USENIX (2016)"},{"key":"16_CR12","unstructured":"Hutchings, B.: Executing arbitrary code within the kernel (2021). https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2021-29154"},{"key":"16_CR13","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.\u00a076. Electronic Communications of the EASST (2018)","DOI":"10.1016\/j.scico.2017.06.012"},{"key":"16_CR14","unstructured":"Keshri, R.: confidentiality problem (2021). https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2021-20320"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Klein, G., et al.: seL4: formal verification of an OS kernel. In: SOSP, pp. 207. ACM Press (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"16_CR16","unstructured":"Krysiuk, P.: Linux kernel vulnerability in NetApp products (2021). https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2021-38300"},{"issue":"7","key":"16_CR17","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"},{"key":"16_CR18","unstructured":"Leroy, X., Appel, A.W., Blazy, S., Stewart, G.: The CompCert Memory Model, Version 2. Research Report RR-7987, INRIA (2012)"},{"issue":"1","key":"16_CR19","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"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-39185-1_12","volume-title":"Types for Proofs and Programs","author":"P Letouzey","year":"2003","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":"16_CR21","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":"16_CR22","unstructured":"McCanne, S., Jacobson, V.: The BSD Packet Filter: A New Architecture for User-level Packet Capture. In: Usenix Winter Conference. vol.\u00a046, pp. 259\u2013270. USENIX (1993)"},{"key":"16_CR23","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)","DOI":"10.1145\/37499.37505"},{"key":"16_CR24","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)","DOI":"10.1145\/3167089"},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"Myreen, M.O.: Verified just-in-time compiler on x86. In: POPL, pp. 107\u2013118. ACM (2010)","DOI":"10.1145\/1707801.1706313"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Myreen, M.O., Owens, S.: Proof-producing synthesis of ml from higher-order logic. In: Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, pp. 115\u2013126. ICFP \u201912, Association for Computing Machinery, New York, NY, USA (2012). https:\/\/doi.org\/10.1145\/2364527.2364545","DOI":"10.1145\/2364527.2364545"},{"key":"16_CR27","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":"16_CR28","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: 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20), pp. 41\u201361. USENIX Association, USA (2020)"},{"key":"16_CR29","unstructured":"Pit-Claudel, C., Philipoom, J., Jamner, D., Erbsen, A., Chlipala, A.: Relational compilation for performance-critical applications. In: PLDI. ACM (2022)"},{"key":"16_CR30","doi-asserted-by":"publisher","unstructured":"Protzenko, J., et al.: Verified low-level programming embedded in F*. PACMPL 1(ICFP), 17:1\u201317:29 (2017). https:\/\/doi.org\/10.1145\/3110261","DOI":"10.1145\/3110261"},{"key":"16_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-319-43144-4_20","volume-title":"Interactive Theorem Proving","author":"C Rizkallah","year":"2016","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":"16_CR32","doi-asserted-by":"crossref","unstructured":"Sozeau, M., Boulier, S., Forster, Y., Tabareau, N., Winterhalter, T.: Coq coq correct! verification of type checking and erasure for coq, in Coq. Proc. ACM Program. Lang. 4(POPL), 8:1\u20138:28 (2020). https:\/\/doi.org\/10.1145\/3371076","DOI":"10.1145\/3371076"},{"key":"16_CR33","doi-asserted-by":"crossref","unstructured":"Tanaka, A.: Coq to C translation with partial evaluation. In: PEPM@POPL, pp. 14\u201331. ACM (2021)","DOI":"10.1145\/3441296.3441394"},{"key":"16_CR34","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"},{"key":"16_CR35","unstructured":"Wang, X., Lazar, D., Zeldovich, N., Chlipala, A., Tatlock, Z.: Jitk: a trustworthy In-Kernel interpreter infrastructure. In: 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14), pp. 33\u201347. USENIX Association, Broomfield, CO (2014)"},{"key":"16_CR36","unstructured":"YUAN, S.: CertrBPF-JIT: A verified JIT for RIOT-OS rBPF (2024). https:\/\/gitlab.inria.fr\/x-SYuan\/certrbpf-jit\/-\/tree\/CAV24-AE"},{"key":"16_CR37","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-031-13188-2_15","volume-title":"Computer Aided Verification","author":"S Yuan","year":"2022","unstructured":"Yuan, S., Besson, F., Talpin, J.P., Hym, S., Zandberg, K., Baccelli, E.: End-to-end mechanized proof of an eBPF virtual machine for micro-controllers. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification, pp. 293\u2013316. Springer International Publishing, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_15"},{"key":"16_CR38","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)","DOI":"10.23919\/PEMWN50727.2020.9293081"},{"key":"16_CR39","doi-asserted-by":"crossref","unstructured":"Zandberg, K., Baccelli, E., Yuan, S., Besson, F., Talpin, J.P.: Femto-containers: lightweight virtualization and fault isolation for small software functions on low-power IoT microcontrollers. In: Proceedings of the 23rd ACM\/IFIP International Middleware Conference, pp. 161\u2013173. Middleware \u201922, Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3528535.3565242","DOI":"10.1145\/3528535.3565242"},{"key":"16_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-030-50029-0_21","volume-title":"Coordination Models and Languages","author":"X Zhang","year":"2020","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"}],"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-65627-9_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T19:04:04Z","timestamp":1721934244000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65627-9_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656262","9783031656279"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65627-9_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}