{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T16:23:25Z","timestamp":1783700605258,"version":"3.55.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["N66001-21-C-4028"],"award-info":[{"award-number":["N66001-21-C-4028"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,10,8]]},"abstract":"<jats:p>\n                    Even though heavily researched, a full formal model of the x86-64 instruction set is still not available. We present\n                    <jats:sc>libLISA<\/jats:sc>\n                    , a tool for automated discovery and analysis of the ISA of a CPU. This produces the most extensive formal x86-64 model to date, with over 118 000 different instruction groups. The process requires as little human specification as possible: specifically, we do not rely on a human-written (dis)assembler to dictate which instructions are executable on a given CPU, or what their in- and outputs are. The generated model is CPU-specific: behavior that is \u201cundefined\u201d is synthesized for the current machine. Producing models for five different x86-64 machines, we mutually compare them, discover undocumented instructions, and generate instruction sequences that are CPU-specific. Experimental evaluation shows that we enumerate virtually all instructions within scope, that the instructions\u2019 semantics are correct w.r.t. existing work, and that we improve existing work by exposing bugs in their handwritten models.\n                  <\/jats:p>","DOI":"10.1145\/3689723","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"333-361","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["libLISA: Instruction Discovery and Analysis on x86-64"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-9799-3517","authenticated-orcid":false,"given":"Jos","family":"Craaijo","sequence":"first","affiliation":[{"name":"Open Universiteit, Heerlen, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6625-1123","authenticated-orcid":false,"given":"Freek","family":"Verbeek","sequence":"additional","affiliation":[{"name":"Open Universiteit, Heerlen, Netherlands"},{"name":"Virginia Tech, Blacksburg, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8663-739X","authenticated-orcid":false,"given":"Binoy","family":"Ravindran","sequence":"additional","affiliation":[{"name":"Virginia Tech, Blacksburg, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_18"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3208071"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"issue":"14","key":"e_1_3_1_5_2","article-title":"The SMT-LIB Standard: Version 2.0","volume":"13","author":"Barrett Clark","year":"2010","unstructured":"Clark Barrett, Aaron Stump, Cesare Tinelli, et al. 2010. The SMT-LIB Standard: Version 2.0. In Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, UK), Vol. 13. 14.","journal-title":"Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, UK)"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/2695664.2695924"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_37"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.13380062"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314601"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","unstructured":"Rens Dofferhoff Michael G\u00f6ebel Kristian Rietveld and Erik van der Kouwe. 2020. iScanU: A Portable Scanner for Undocumented Instructions on RISC Processors. In 2020 50th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN 2020). 306\u2013317. https:\/\/doi.org\/10.1109\/DSN48063.2020.00047 10.1109\/DSN48063.2020.00047","DOI":"10.1109\/DSN48063.2020.00047"},{"key":"e_1_3_1_12_2","unstructured":"Christopher Domas. 2017. Breaking the x86 ISA. https:\/\/github.com\/xoreaxeaxeax\/sandsifter Accessed on 02\/05\/2024."},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254116"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987600"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950335"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908121"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","unstructured":"Nathan Jay and Barton P. Miller. 2018. Structured random differential testing of instruction decoders. In 2018 IEEE 25th International Conference on Software Analysis Evolution and Reengineering (SANER). 84\u201394. https:\/\/doi.org\/10.1109\/SANER.2018.8330199 10.1109\/SANER.2018.8330199","DOI":"10.1109\/SANER.2018.8330199"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","unstructured":"Doug Kwan Kostik Shtoyk Kostya Serebryany Maxim L Lifantsev and Peter Hochschild. 2021. SiliFuzz: fuzzing CPUs by proxy. Google Research (2021). https:\/\/doi.org\/10.48550\/arXiv.2110.11519 10.48550\/arXiv.2110.11519","DOI":"10.48550\/arXiv.2110.11519"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2019.2946444"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/2450136.2450139"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/1572272.1572303"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254111"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2016.7886675"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451150"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_1_29_2","first-page":"5341","volume-title":"33rd USENIX Security Symposium (USENIX Security 24)","author":"Solt Flavien","year":"2024","unstructured":"Flavien Solt, Katharina Ceesay-Seitz, and Kaveh Razavi. 2024. Cascade: CP U Fuzzing via Intricate Program Generation. In 33rd USENIX Security Symposium (USENIX Security 24). USENIX Association, Philadelphia, PA, 5341\u20135358."},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689723","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689723","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:03:37Z","timestamp":1770195817000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689723"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":29,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689723"],"URL":"https:\/\/doi.org\/10.1145\/3689723","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-04","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}