{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T08:08:56Z","timestamp":1790928536479,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":22,"publisher":"ACM","license":[{"start":{"date-parts":[[2026,9,28]],"date-time":"2026-09-28T00:00:00Z","timestamp":1790553600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"ZJNSF Major Program","award":["LD24F020013"],"award-info":[{"award-number":["LD24F020013"]}]},{"name":"Zhejiang Pioneer (Jianbing) Project","award":["2024C01032"],"award-info":[{"award-number":["2024C01032"]}]},{"name":"NSFC","award":["62502431"],"award-info":[{"award-number":["62502431"]}]},{"name":"NSFC","award":["62532012"],"award-info":[{"award-number":["62532012"]}]},{"name":"NSFC","award":["62572427"],"award-info":[{"award-number":["62572427"]}]},{"name":"Zhejiang Key Laboratory Project","award":["2024E10001"],"award-info":[{"award-number":["2024E10001"]}]},{"name":"Fundamental Research Funds for the Central Universities of China","award":["226-2024-00140"],"award-info":[{"award-number":["226-2024-00140"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,9,29]]},"DOI":"10.1145\/3837779.3838167","type":"proceedings-article","created":{"date-parts":[[2026,9,14]],"date-time":"2026-09-14T19:54:26Z","timestamp":1789415666000},"page":"26-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Specification of Linux eBPF Instruction Set Architecture in Sail"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-5699-1121","authenticated-orcid":false,"given":"Yazhou","family":"Tang","sequence":"first","affiliation":[{"name":"Zhejiang University, Hangzhou, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8467-5827","authenticated-orcid":false,"given":"Shenghao","family":"Yuan","sequence":"additional","affiliation":[{"name":"Zhejiang University, Hangzhou, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0556-4265","authenticated-orcid":false,"given":"Jean-Pierre","family":"Talpin","sequence":"additional","affiliation":[{"name":"Inria, Rennes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9663-7441","authenticated-orcid":false,"given":"Mingshuai","family":"Chen","sequence":"additional","affiliation":[{"name":"Zhejiang University, Hangzhou, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,9,28]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3173162.3177156"},{"key":"e_1_3_2_1_2_1","unstructured":"Alasdair Armstrong. 2025. Sail Asciidoctor Plugin. https:\/\/github.com\/Alasdair\/asciidoctor-sail Accessed: 2026-06-19."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_14"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_3_2_1_6_1","unstructured":"Daniel Borkmann. 2021. bpf: Fix up register-based shifts in interpreter to silence KUBSAN. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=28131e9d933339a92f78e7ab6429f4aaaa07061c Accessed: 2026-06-19."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_3_2_1_8_1","unstructured":"Andreas Rossberg (editor). 2026. WebAssembly Specification (Release 3.0). https:\/\/webassembly.github.io\/spec\/core\/ Accessed: 2026-06-19."},{"key":"e_1_3_2_1_9_1","unstructured":"Matt Fleming. 2017. A Thorough Introduction to eBPF. https:\/\/lwn.net\/Articles\/740157\/ Accessed: 2026-06-19."},{"key":"e_1_3_2_1_10_1","unstructured":"Alan Jowett and contributors. 2026. BPF Conformance. https:\/\/github.com\/Alan-Jowett\/bpf_conformance Accessed: 2026-08-13."},{"key":"e_1_3_2_1_11_1","unstructured":"The kernel development community. 2025. BPF Instruction Set Architecture (ISA). https:\/\/docs.kernel.org\/bpf\/standardization\/instruction-set.html Accessed: 2026-06-19."},{"key":"e_1_3_2_1_12_1","unstructured":"Suresh Krishnan and David Vernet. 2024. Core BPF ecosystem standardized in RFC 9669. https:\/\/www.ietf.org\/blog\/bpf-rfc9669\/ Accessed: 2026-06-19."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_14_1","volume-title":"14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20)","author":"Nelson Luke","year":"2020","unstructured":"Luke Nelson, Jacob Van Geffen, Emina Torlak, and Xi Wang. 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."},{"key":"e_1_3_2_1_15_1","unstructured":"Gordon D. Plotkin. 1981. A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19. Computer Science Department Aarhus University Aarhus Denmark."},{"key":"e_1_3_2_1_16_1","unstructured":"Swarn Priya Fr\u00e9d\u00e9ric Besson Connor Sughrue Tim Steenvoorden Jamie Fulford Freek Verbeek and Binoy Ravindran. 2025. BeePL: Correct-by-compilation kernel extensions. arXiv:2507.09883 [cs.PL]"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","unstructured":"Dave Thaler. 2024. BPF Instruction Set Architecture (ISA). RFC 9669. doi:10.17487\/RFC9669","DOI":"10.17487\/RFC9669"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_29"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_15"},{"key":"e_1_3_2_1_21_1","volume-title":"Proc. ACM Program. Lang. 10","author":"Yuan Shenghao","year":"2026","unstructured":"Shenghao Yuan, Yazhou Tang, Tianci Cao, Fr\u00e9d\u00e9ric Besson, Jean-Pierre Talpin, and Mingshuai Chen. 2026. Formalizing the Linux eBPF Core ISA: A Mechanized Operational Semantics and Its Real-World Applications. Proc. ACM Program. Lang. 10, OOPSLA2 (2026). https:\/\/shenghaoyuan.github.io\/publications\/OOPSLA2026.pdf To appear."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3720414"}],"event":{"name":"SOSP '26: ACM SIGOPS 32nd Symposium on Operating Systems Principles","location":"Prague Czech Republic","acronym":"eBPF'26","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX"]},"container-title":["Proceedings of the 4th Workshop on eBPF and Kernel Extensions"],"original-title":[],"deposited":{"date-parts":[[2026,9,14]],"date-time":"2026-09-14T19:54:37Z","timestamp":1789415677000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3837779.3838167"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,9,28]]},"references-count":22,"alternative-id":["10.1145\/3837779.3838167","10.1145\/3837779"],"URL":"https:\/\/doi.org\/10.1145\/3837779.3838167","relation":{},"subject":[],"published":{"date-parts":[[2026,9,28]]},"assertion":[{"value":"2026-09-28","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}