{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:24:32Z","timestamp":1787592272919,"version":"build-2736575974"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>We present the first formal semantics for the Solana eBPF bytecode language used in smart contracts on the Solana blockchain platform. Our formalization accurately captures all binary-level instructions of the Solana eBPF instruction set architecture. This semantics is structured in a small-step style, facilitating the formalization of the Solana eBPF interpreter within Isabelle\/HOL. We provide a semantics validation framework that extracts an executable semantics from our formalization to test against the original implementation of the Solana eBPF interpreter. This approach introduces a novel lightweight and non-invasive method to relax the limitations of the existing Isabelle\/HOL extraction mechanism. Furthermore, we illustrate potential applications of our semantics in the formalization of the main components of the Solana eBPF virtual machine<\/jats:p>","DOI":"10.1145\/3720414","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["A Complete Formal Semantics of eBPF Instruction Set Architecture for Solana"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8467-5827","authenticated-orcid":false,"given":"Shenghao","family":"Yuan","sequence":"first","affiliation":[{"name":"Zhejiang University, Hangzhou, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7896-1694","authenticated-orcid":false,"given":"Zhuoruo","family":"Zhang","sequence":"additional","affiliation":[{"name":"Zhejiang University, Hangzhou, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-0035-7251","authenticated-orcid":false,"given":"Jiayi","family":"Lu","sequence":"additional","affiliation":[{"name":"Zhejiang University, Hangzhou, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2755-3089","authenticated-orcid":false,"given":"David","family":"Sanan","sequence":"additional","affiliation":[{"name":"Singapore Institute of Technology, Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0178-0171","authenticated-orcid":false,"given":"Rui","family":"Chang","sequence":"additional","affiliation":[{"name":"Zhejiang University, Hangzhou, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2284-1383","authenticated-orcid":false,"given":"Yongwang","family":"Zhao","sequence":"additional","affiliation":[{"name":"Zhejiang University, Hangzhou, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-48065-3_18"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167084"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"e_1_3_2_5_1","unstructured":"BoredPerson. 2024. Fix JIT second level defence. https:\/\/github.com\/solana-labs\/rbpf\/pull\/557"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_32"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3548606.3560552"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314601"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.08.005"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65627-9_22"},{"key":"e_1_3_2_12_1","volume-title":"A Thorough Introduction to eBPF","author":"Fleming Matt","year":"2017","unstructured":"MattFleming. 2017. A Thorough Introduction to eBPF."},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314560"},{"key":"e_1_3_2_14_1","unstructured":"SudhanshuGoswami. 2005. An introduction to KProbes. https:\/\/www.kernel.org\/doc\/html\/latest\/kprobes.html"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00022"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70278-0_33"},{"key":"e_1_3_2_17_1","unstructured":"Meta Incubator. 2018. A high performance layer 4 load balancer. https:\/\/github.com\/facebookincubator\/katran"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40002.2020.00066"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32409-4_8"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94821-8_23"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-96-0602-3_11"},{"key":"e_1_3_2_23_1","first-page":"403","volume-title":"Software Engineering and Formal Methods","author":"Malgoni Diego","year":"2021","unstructured":"DiegoMalgoni, Achim D.Brucker. 2021. Denotational Semantics of Solidity in Isabelle\/HOL. In Software Engineering and Formal Methods, RaduCalinescu, Corina S.P\u0103s\u0103reanu (Eds.). Springer International Publishing, Cham, 403\u2013422."},{"key":"e_1_3_2_24_1","first-page":"259","volume-title":"USENIX Winter Conference","author":"McCanne Steven","year":"1993","unstructured":"StevenMcCanne, VanJacobson. 1993. The BSD Packet Filter: A New Architecture for User-Level Packet Capture. In USENIX Winter Conference, 46. USENIX Association, San Diego, California, USA, 259\u2013270."},{"key":"e_1_3_2_25_1","unstructured":"Microsoft. 2019. eBPF implementation that runs on top of Windows. https:\/\/github.com\/microsoft\/ebpf-for-windows"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3341361"},{"key":"e_1_3_2_27_1","first-page":"41","volume-title":"14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20)","author":"Nelson Luke","year":"2020","unstructured":"LukeNelson, JacobVan Geffen, EminaTorlak, XiWang. 2020. 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). USENIX Association, USA, 41\u201361. https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/nelson"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_8"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3264591"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656844.3690237"},{"key":"e_1_3_2_32_1","unstructured":"BhatSanjit ShachamHovav. 2023. Formal Verification of the Linux Kernel eBPF Verifier Range Analysis. https:\/\/sanjit-bhat.github.io\/assets\/pdf\/ebpf-range-analysis22.pdf"},{"key":"e_1_3_2_33_1","unstructured":"Kudelski Security. 2019. 2019. Solana Labs Architectural Security Review and Report. https:\/\/kudelskisecurity.com\/wp-content\/uploads\/Solana-Labs-Architectural-Security-Review-and-Report.pdf"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3623178"},{"key":"e_1_3_2_36_1","doi-asserted-by":"crossref","unstructured":"Solana Labs. 2018. Solana Labs eBPF. https:\/\/github.com\/solana-labs\/ebpf","DOI":"10.1155\/2018\/3128758"},{"key":"e_1_3_2_37_1","unstructured":"Solana Labs. 2024. Fix clank. https:\/\/github.com\/solana-labs\/rbpf\/pull\/583"},{"key":"e_1_3_2_38_1","doi-asserted-by":"crossref","unstructured":"DaveThaler. 2024. BPF Instruction Set Architecture (ISA) draft-ietf-bpf-isa-04. https:\/\/datatracker.ietf.org\/doc\/draft-ietf-bpf-isa-04","DOI":"10.17487\/RFC9669"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_29"},{"key":"e_1_3_2_41_1","unstructured":"FreekVerbeek AbhijithBharadwaj JoshuaBockenek IanRoessle TimmyWeerwag BinoyBaran. 2021. x86 instruction semantics and basic block symbolic execution. https:\/\/isa-afp.org\/entries\/x86_Semantics.html"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_12"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241"},{"key":"e_1_3_2_44_1","first-page":"33","volume-title":"11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14)","author":"Wang Xi","year":"2014","unstructured":"XiWang, DavidLazar, NicholasZeldovich, AdamChlipala, ZacharyTatlock. 2014. Int\u03ack: A Trustworthy In-Kernel Interpreter Infrastructure. In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14). USENIX Association, USA, 33\u201345. https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/wang"},{"key":"e_1_3_2_45_1","unstructured":"YupengWang ShuvenduLahiri ShuoChen RongPan SidiDillig CodyBorn ImmadNaseer. 2019. Formal Specification and Verification of Smart Contracts for Azure Blockchain. https:\/\/www.microsoft.com\/en-us\/research\/publication\/formal-specification-and-verification-of-smart-contracts-for-azure-blockchain\/"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3452296.3472929"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65627-9_16"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_15"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-99-8664-4_22"},{"key":"e_1_3_2_50_1","unstructured":"ShenghaoYuan ZhuoruoZhang JiayiLu DavidSanan. 2022. A complete formal semantics of eBPF instruction set architecture for Solana VM. https:\/\/github.com\/shenghaoyuan\/CertiBPF\/tree\/oopsla25-ae"},{"key":"e_1_3_2_51_1","doi-asserted-by":"crossref","unstructured":"ShenghaoYuan ZhuoruoZhang JiayiLu DavidSanan. 2025. A complete formal semantics of eBPF instruction set architecture for Solana VM. https:\/\/doi.org\/10.5281\/zenodo.14909585","DOI":"10.1145\/3720414"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3582535.3565242"},{"key":"e_1_3_2_53_1","first-page":"137","volume-title":"Computer Aided Verification","author":"Emma Jingyi","year":"2020","unstructured":"JingyiEmma, ZhongKevin, ChengShaozhe, AdeebWolfgang, GrieskampSam, SeanBlackshear, JunliPark, YoniZohar, ClarkBarrett, David L.Dill. 2020. The Move Prover. In Computer Aided Verification, Shuvendu K.Lahiri, ChaoWang (Eds.). Springer International Publishing, Cham, 137\u2013150."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720414","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720414","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:28:48Z","timestamp":1787588928000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720414"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":52,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720414"],"URL":"https:\/\/doi.org\/10.1145\/3720414","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}