{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T15:57:21Z","timestamp":1742918241996,"version":"3.40.3"},"publisher-location":"Singapore","reference-count":29,"publisher":"Springer Nature Singapore","isbn-type":[{"type":"print","value":"9789819606016"},{"type":"electronic","value":"9789819606023"}],"license":[{"start":{"date-parts":[[2024,11,25]],"date-time":"2024-11-25T00:00:00Z","timestamp":1732492800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,25]],"date-time":"2024-11-25T00:00:00Z","timestamp":1732492800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-981-96-0602-3_11","type":"book-chapter","created":{"date-parts":[[2024,11,24]],"date-time":"2024-11-24T03:46:55Z","timestamp":1732420015000},"page":"197-216","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formalizing x86-64 ISA in\u00a0Isabelle\/HOL:\u00a0A Binary Semantics for\u00a0eBPF JIT Correctness"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-0035-7251","authenticated-orcid":false,"given":"Jiayi","family":"Lu","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8467-5827","authenticated-orcid":false,"given":"Shenghao","family":"Yuan","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2755-3089","authenticated-orcid":false,"given":"David","family":"Sanan","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2284-1383","authenticated-orcid":false,"given":"Yongwang","family":"Zhao","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,25]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Armstrong, A., et\u00a0al.: ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS. Proc. ACM Program. Lang. 3(POPL), 1\u201331 (2019)","key":"11_CR1","DOI":"10.1145\/3290384"},{"doi-asserted-by":"crossref","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)","key":"11_CR2","DOI":"10.1145\/3571202"},{"key":"11_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions","author":"Y Bertot","year":"2010","unstructured":"Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions, 1st edn. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-662-07964-5","edition":"1"},{"doi-asserted-by":"crossref","unstructured":"Dasgupta, S., Park, D., Kasampalis, T., Adve, V.S., Ro\u015fu, G.: A complete formal semantics of x86-64 user-level instruction set architecture. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 1133\u20131148 (2019)","key":"11_CR4","DOI":"10.1145\/3314221.3314601"},{"unstructured":"Fleming, M.: A thorough introduction to eBPF (2017)","key":"11_CR5"},{"doi-asserted-by":"crossref","unstructured":"Fromherz, A., Giannarakis, N., Hawblitzel, C., Parno, B., Rastogi, A., Swamy, N.: A verified, efficient embedding of a verifiable assembly language. In: Principles of Programming Languages (POPL 2019). ACM (2019). https:\/\/www.microsoft.com\/en-us\/research\/publication\/a-verified-efficient-embedding-of-a-verifiable-assembly-language\/","key":"11_CR6","DOI":"10.1145\/3290376"},{"unstructured":"Goel, S.: Formal verification of application and system programs based on a validated x86 ISA model. Ph.D. thesis, University of Texas at Austin (2016)","key":"11_CR7"},{"doi-asserted-by":"crossref","unstructured":"Goel, S., Slobodov\u00e1, A., Sumners, R., Swords, S.: Verifying x86 instruction implementations. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 47\u201360 (2020)","key":"11_CR8","DOI":"10.1145\/3372885.3373811"},{"unstructured":"Hou, Z., Sanan, D., Tiu, A., Liu, Y.: A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor. Archive of Formal Proofs (2016). https:\/\/isa-afp.org\/entries\/SPARCv8.html. Formal proof development","key":"11_CR9"},{"key":"11_CR10","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1007\/s10817-020-09579-4","volume":"65","author":"Z H\u00f3u","year":"2021","unstructured":"H\u00f3u, Z., Sanan, D., Tiu, A., Liu, Y., Hoa, K.C., Dong, J.S.: An Isabelle\/HOL formalisation of the SPARC instruction set architecture and the TSO memory model. J. Autom. Reason. 65, 569\u2013598 (2021)","journal-title":"J. Autom. Reason."},{"doi-asserted-by":"publisher","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, pp. 179\u2013191. Association for Computing Machinery, New York (2014). https:\/\/doi.org\/10.1145\/2535838.2535841","key":"11_CR11","DOI":"10.1145\/2535838.2535841"},{"doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009). http:\/\/xavierleroy.org\/publi\/compcert-CACM.pdf","key":"11_CR12","DOI":"10.1145\/1538788.1538814"},{"unstructured":"Leroy, X., Appel, A.W., Blazy, S., Stewart, G.: The CompCert memory model, version 2. Research report RR-7987, INRIA (2012). https:\/\/inria.hal.science\/hal-00703441","key":"11_CR13"},{"unstructured":"Lu, J., Yuan, S., Sanan, D., Zhao, Y.: Solana x64 Semantics (2024). https:\/\/github.com\/shenghaoyuan\/Solana-x64-Semantics","key":"11_CR14"},{"doi-asserted-by":"crossref","unstructured":"Morrisett, G., Tan, G., Tassarotti, J., Tristan, J.B., Gan, E.: RockSalt: better, faster, stronger SFI for the x86. In: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 395\u2013404 (2012)","key":"11_CR15","DOI":"10.1145\/2254064.2254111"},{"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 2020), pp. 41\u201361. USENIX Association (2020). https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/nelson","key":"11_CR16"},{"key":"11_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"11_CR18","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-1-4419-5998-0_3","volume-title":"Scalable Techniques for Formal Verification","author":"S Ray","year":"2010","unstructured":"Ray, S.: Introduction to ACL2. In: Ray, S. (ed.) Scalable Techniques for Formal Verification, pp. 25\u201349. Springer, Boston (2010). https:\/\/doi.org\/10.1007\/978-1-4419-5998-0_3"},{"unstructured":"RISCV-Coq Team: RISC-V Specification in Coq (2024). https:\/\/github.com\/mit-plv\/riscv-coq","key":"11_CR19"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28\u201332. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_6"},{"unstructured":"Solana-Labs: Solana rBPF (2024). https:\/\/github.com\/solana-labs\/rbpf","key":"11_CR21"},{"issue":"6","key":"11_CR22","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1145\/276609.276617","volume":"41","author":"P Tyma","year":"1998","unstructured":"Tyma, P.: Why are we using Java again? Commun. ACM 41(6), 38\u201342 (1998). https:\/\/doi.org\/10.1145\/276609.276617","journal-title":"Commun. ACM"},{"unstructured":"Verbeek, F., Bharadwaj, A., Bockenek, J., Roessle, I., Weerwag, T., Ravindran, B.: X86 instruction semantics and basic block symbolic execution. Archive of Formal Proofs (2021). https:\/\/isa-afp.org\/entries\/X86_Semantics.html. Formal proof development","key":"11_CR23"},{"key":"11_CR24","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2019.102371","volume":"187","author":"J Wang","year":"2020","unstructured":"Wang, J., Fu, M., Qiao, L., Feng, X.: Formalizing SPARCv8 instruction set architecture in Coq. Sci. Comput. Program. 187, 102371 (2020). https:\/\/doi.org\/10.1016\/J.SCICO.2019.102371","journal-title":"Sci. Comput. Program."},{"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 2014), pp. 33\u201347. USENIX Association, Broomfield (2014). https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/wang_xi","key":"11_CR25"},{"doi-asserted-by":"crossref","unstructured":"Wang, Y., Xu, X., Wilke, P., Shao, Z.: CompCertELF: verified separate compilation of C programs into elf object files. Proc. ACM Program. Lang. 4(OOPSLA), 1\u201328 (2020)","key":"11_CR26","DOI":"10.1145\/3428265"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"728","DOI":"10.1007\/978-3-030-81688-9_34","volume-title":"Computer Aided Verification","author":"X Xu","year":"2021","unstructured":"Xu, X., Wu, J., Wang, Y., Yin, Z., Li, P.: Automatic generation and validation of instruction encoders and decoders. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 728\u2013751. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_34"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-031-65627-9_16","volume-title":"Computer Aided Verification","author":"S Yuan","year":"2024","unstructured":"Yuan, S., Besson, F., Talpin, J.P.: End-to-end mechanized proof of a JIT-accelerated eBPF virtual machine for IoT. In: Gurfinkel, A., Ganesh, V. (eds.) CAV 2024. LNCS, vol. 14681, pp. 325\u2013347. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_16"},{"doi-asserted-by":"publisher","unstructured":"Yuan, S., Talpin, J.P.: Verified functional programming of an IoT operating system\u2019s bootloader. In: Proceedings of the 19th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2021, pp. 89\u201397. Association for Computing Machinery, New York (2021). https:\/\/doi.org\/10.1145\/3487212.3487347","key":"11_CR29","DOI":"10.1145\/3487212.3487347"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-96-0602-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,24]],"date-time":"2024-11-24T04:19:21Z","timestamp":1732421961000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-96-0602-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,25]]},"ISBN":["9789819606016","9789819606023"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-981-96-0602-3_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,25]]},"assertion":[{"value":"25 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETTA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Dependable Software Engineering: Theories, Tools, and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hong Kong","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","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":"26 November 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 November 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setta2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/setta2024.cs.cityu.edu.hk\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}