{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T07:28:45Z","timestamp":1769758125941,"version":"3.49.0"},"reference-count":72,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2023,3,3]],"date-time":"2023-03-03T00:00:00Z","timestamp":1677801600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"U.S. Air Force and DARPA","award":["FA8750-16-C-0045"],"award-info":[{"award-number":["FA8750-16-C-0045"]}]},{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2023,3,31]]},"abstract":"<jats:p>The end of Moore\u2019s Law has ushered in a diversity of hardware not seen in decades. Operating system (OS) (and system software) portability is accordingly becoming increasingly critical. Simultaneously, there has been tremendous progress in program synthesis. We set out to explore the feasibility of using modern program synthesis to generate the machine-dependent parts of an operating system. Our ultimate goal is to generate new ports automatically from descriptions of new machines.<\/jats:p>\n          <jats:p>One of the issues involved is writing specifications, both for machine-dependent operating system functionality and for instruction set architectures. We designed two domain-specific languages: Alewife for machine-independent specifications of machine-dependent operating system functionality and Cassiopea for describing instruction set architecture semantics. Automated porting also requires an implementation. We developed a toolchain that, given an Alewife specification and a Cassiopea machine description, specializes the machine-independent specification to the target instruction set architecture and synthesizes an implementation in assembly language with a customized symbolic execution engine. Using this approach, we demonstrate the successful synthesis of a total of 140 OS components from two pre-existing OSes for four real hardware platforms. We also developed several optimization methods for OS-related assembly synthesis to improve scalability.<\/jats:p>\n          <jats:p>The effectiveness of our languages and ability to synthesize code for all 140 specifications is evidence of the feasibility of program synthesis for machine-dependent OS code. However, many research challenges remain; we also discuss the benefits and limitations of our synthesis-based approach to automated OS porting.<\/jats:p>","DOI":"10.1145\/3563943","type":"journal-article","created":{"date-parts":[[2022,9,20]],"date-time":"2022-09-20T11:19:51Z","timestamp":1663672791000},"page":"1-70","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Towards Porting Operating Systems with Program Synthesis"],"prefix":"10.1145","volume":"45","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4434-5057","authenticated-orcid":false,"given":"Jingmei","family":"Hu","sequence":"first","affiliation":[{"name":"Harvard University, Boston, MA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1228-9887","authenticated-orcid":false,"given":"Eric","family":"Lu","sequence":"additional","affiliation":[{"name":"Harvard University, Boston, MA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9328-1686","authenticated-orcid":false,"given":"David A.","family":"Holland","sequence":"additional","affiliation":[{"name":"Harvard University, Boston, MA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5999-2882","authenticated-orcid":false,"given":"Ming","family":"Kawaguchi","sequence":"additional","affiliation":[{"name":"Harvard University, Boston, MA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6734-5383","authenticated-orcid":false,"given":"Stephen","family":"Chong","sequence":"additional","affiliation":[{"name":"Harvard University, Boston, MA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2165-4658","authenticated-orcid":false,"given":"Margo","family":"Seltzer","sequence":"additional","affiliation":[{"name":"The University of British Columbia, Vancouver, BC, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,3,3]]},"reference":[{"key":"e_1_3_4_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_3_4_3_1","volume-title":"Proceedings of the 46th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Armstrong Alasdair","year":"2019","unstructured":"Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell. 2019. ISA semantics for ARMv8-a, RISC-V, and CHERI-MIPS. In Proceedings of the 46th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages."},{"key":"e_1_3_4_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168906"},{"key":"e_1_3_4_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629579"},{"key":"e_1_3_4_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134000"},{"key":"e_1_3_4_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/202453.202472"},{"key":"e_1_3_4_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706339"},{"key":"e_1_3_4_9_1","first-page":"917","volume-title":"Proceedings of the 26th USENIX Security Symposium.","author":"Bond Barry","year":"2017","unstructured":"Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson. 2017. Vale: Verifying high-performance cryptographic assembly code. In Proceedings of the 26th USENIX Security Symposium.USENIX Association, Vancouver, BC, 917\u2013934. Retrieved from https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/bond."},{"key":"e_1_3_4_10_1","volume-title":"Proceedings of the 2017 Programming Languages Design and Implementation Conference.","author":"Bornholt James","year":"2017","unstructured":"James Bornholt and Emina Torlak. 2017. Synthesizing memory models from framework sketches and litmus tests. In Proceedings of the 2017 Programming Languages Design and Implementation Conference."},{"key":"e_1_3_4_11_1","volume-title":"Proceedings of the 33rd Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications.","author":"Bornholt James","year":"2018","unstructured":"James Bornholt and Emina Torlak. 2018. Finding code that explodes under symbolic evaluation. In Proceedings of the 33rd Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications."},{"key":"e_1_3_4_12_1","unstructured":"Thomas Bourgeat Ian Clester Andres Erbsen Samuel Gruetter Andrew Wright and Adam Chlipala. 2021. A multipurpose formal RISC-V specification. arXiv:2104.00762. Retrieved from https:\/\/arxiv.org\/abs\/2104.00762."},{"key":"e_1_3_4_13_1","first-page":"472","volume-title":"Proceedings of the International Conference on Automated Deduction","author":"Brotherston James","year":"2017","unstructured":"James Brotherston, Nikos Gorogiannis, and Max Kanovich. 2017. Biabduction (and related problems) in array separation logic. In Proceedings of the International Conference on Automated Deduction. Springer, 472\u2013490."},{"key":"e_1_3_4_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"e_1_3_4_15_1","first-page":"1093","volume-title":"Proceedings of the 29th USENIX Security Symposium.","author":"Chen Weiteng","year":"2020","unstructured":"Weiteng Chen, Xiaochen Zou, Guoren Li, and Zhiyun Qian. 2020. KOOBE: Towards facilitating exploit generation of kernel out-of-bounds write vulnerabilities. In Proceedings of the 29th USENIX Security Symposium.USENIX Association, 1093\u20131110. Retrieved from https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/chen-weiteng."},{"key":"e_1_3_4_16_1","volume-title":"Proceedings of the CIDR","author":"Chu Shumo","year":"2017","unstructured":"Shumo Chu, Chenglong Wang, Konstantin Weitz, and Alvin Cheung. 2017. Cosette: An automated prover for SQL. In Proceedings of the CIDR."},{"key":"e_1_3_4_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/138407"},{"key":"e_1_3_4_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_4_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/349214.349233"},{"key":"e_1_3_4_20_1","doi-asserted-by":"crossref","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Proceedings of the Computer-Aided Verification Conference.","volume":"8559","author":"Dutertre Bruno","year":"2014","unstructured":"Bruno Dutertre. 2014. Yices 2.2. In Proceedings of the Computer-Aided Verification Conference.Armin Biere and Roderick Bloem (Eds.), Lecture Notes in Computer Science, Vol. 8559. Springer, 737\u2013744."},{"key":"e_1_3_4_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/238721.238775"},{"key":"e_1_3_4_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/224056.224076"},{"key":"e_1_3_4_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737977"},{"key":"e_1_3_4_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/3489212.3489311"},{"key":"e_1_3_4_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926423"},{"key":"e_1_3_4_26_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000010"},{"key":"e_1_3_4_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3282307"},{"key":"e_1_3_4_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2019.2897677"},{"key":"e_1_3_4_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/AAI28452520"},{"key":"e_1_3_4_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/563340.563383"},{"key":"e_1_3_4_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3365137.3365401"},{"key":"e_1_3_4_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3472749.3474740"},{"key":"e_1_3_4_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_4_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"e_1_3_4_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_4_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_4_37_1","first-page":"20","volume-title":"Proceedings of the 6th Conference on Operating Systems Design and Implementation - Volume 6.","author":"Li Zhenmin","year":"2004","unstructured":"Zhenmin Li, Shan Lu, Suvda Myagmar, and Yuanyuan Zhou. 2004. CP-miner: A tool for finding copy-paste and related bugs in operating system code. In Proceedings of the 6th Conference on Operating Systems Design and Implementation - Volume 6.USENIX Association, Berkeley, CA,20\u201320. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id=1251254.1251274."},{"key":"e_1_3_4_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.07.041"},{"key":"e_1_3_4_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/224056.224075"},{"key":"e_1_3_4_40_1","volume-title":"Linux Kernel Develoment, Third Edition","author":"Love Robert","year":"2010","unstructured":"Robert Love. 2010. Linux Kernel Develoment, Third Edition. Addison-Wesley Professional."},{"key":"e_1_3_4_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/36206.36194"},{"key":"e_1_3_4_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/231070"},{"key":"e_1_3_4_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319345"},{"key":"e_1_3_4_44_1","first-page":"153","volume-title":"Proceedings of the Operating Systems Design and Implementation.","author":"Mosberger David","year":"1996","unstructured":"David Mosberger and Larry L. Peterson. 1996. Making paths explicit in the scout operating system. In Proceedings of the Operating Systems Design and Implementation. USENIX Assoc., Seattle, WA, 153\u2013167."},{"key":"e_1_3_4_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2019.2915318"},{"key":"e_1_3_4_46_1","article-title":"Linux assemblers: A comparison of GAS and NASM","author":"Narayan Ram","year":"2007","unstructured":"Ram Narayan. 2007. Linux assemblers: A comparison of GAS and NASM. Tutorial:http:\/\/www.ibm.com\/developerworks\/library\/l-gas-nasm.html.","journal-title":"Tutorial:"},{"key":"e_1_3_4_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_3_4_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2892208.2892233"},{"key":"e_1_3_4_49_1","volume-title":"Proceedings of the 46th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.","author":"Polikarpova Nadia","year":"2019","unstructured":"Nadia Polikarpova and Ilya Sergey. 2019. Structuring the synthesis of heap-manipulating programs. In Proceedings of the 46th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages."},{"key":"e_1_3_4_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814310"},{"key":"e_1_3_4_51_1","first-page":"11","article-title":"The synthesis kernel","volume":"1","author":"Pu Calton","year":"1988","unstructured":"Calton Pu, Henry Massalin, and John Ioannidis. 1988. The synthesis kernel. Computing Systems 1, 1 (1988), 11\u201332.","journal-title":"Computing Systems"},{"key":"e_1_3_4_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/36206. 36181"},{"key":"e_1_3_4_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/3077629.3077658"},{"key":"e_1_3_4_54_1","unstructured":"RISC-V. 2019. ISA Formal Spec Public Review. (2019). Retrieved October 1 2022 from https:\/\/github.com\/riscvarchive\/ISA_Formal_Spec_Public_Review."},{"key":"e_1_3_4_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629583"},{"key":"e_1_3_4_56_1","doi-asserted-by":"publisher","DOI":"10.5555\/2685048.2685101"},{"key":"e_1_3_4_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451150"},{"key":"e_1_3_4_58_1","first-page":"523","volume-title":"Proceedings of the 29th USENIX Security Symposium.","author":"Shinde Shweta","year":"2020","unstructured":"Shweta Shinde, Shengyi Wang, Pinghai Yuan, Aquinas Hobor, Abhik Roychoudhury, and Prateek Saxena. 2020. BesFS: A POSIX filesystem for enclaves with a mechanized safety proof. In Proceedings of the 29th USENIX Security Symposium.USENIX Association, 523\u2013540. Retrieved from https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/shinde."},{"key":"e_1_3_4_59_1","doi-asserted-by":"crossref","unstructured":"Yan Shoshitaishvili Ruoyu Wang Christopher Salls Nick Stephens Mario Polino Audrey Dutcher John Grosen Siji Feng Christophe Hauser Christopher Kruegel and Giovanni Vigna. 2016. SoK: (state of) the art of war: Offensive techniques in binary analysis. In Proceedings of the 2016 IEEE Symposium on Security and Privacy .","DOI":"10.1109\/SP.2016.17"},{"key":"e_1_3_4_60_1","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1007\/978-3-319-21690-4_23","volume-title":"Proceedings of the Computer Aided Verification","author":"Singh Rishabh","year":"2015","unstructured":"Rishabh Singh and Sumit Gulwani. 2015. Predicting a correct program in programming by example. In Proceedings of the Computer Aided Verification, Daniel Kroening and Corina S. P\u0103s\u0103reanu (Eds.), Springer International Publishing, Cham, 398\u2013414."},{"key":"e_1_3_4_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2025113.2025153"},{"key":"e_1_3_4_62_1","volume-title":"Program Synthesis by Sketching","author":"Solar-Lezama Armando","year":"2008","unstructured":"Armando Solar-Lezama. 2008. Program Synthesis by Sketching. Ph.D. Dissertation. Berkeley, CA. Advisor(s) Bodik, Rastislav. AAI3353225."},{"key":"e_1_3_4_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375599"},{"key":"e_1_3_4_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065045"},{"key":"e_1_3_4_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_4_66_1","first-page":"2541","volume-title":"Proceedings of the 29th USENIX Security Symposium.","author":"Song Dokyung","year":"2020","unstructured":"Dokyung Song, Felicitas Hetzelt, Jonghwan Kim, Brent ByungHoon Kang, Jean-Pierre Seifert, and Michael Franz. 2020. Agamotto: Accelerating kernel driver fuzzing with lightweight virtual machine checkpoints. In Proceedings of the 29th USENIX Security Symposium.USENIX Association, 2541\u20132557. Retrieved from https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/song."},{"key":"e_1_3_4_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/800009.808043"},{"key":"e_1_3_4_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737960"},{"key":"e_1_3_4_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984006"},{"key":"e_1_3_4_70_1","first-page":"1","volume-title":"Proceedings of the 32nd Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications.","author":"Srinivasan Venkatesh","year":"2017","unstructured":"Venkatesh Srinivasan, Ara Vartanian, and Thomas Reps. 2017. Model-assisted machine-code synthesis. In Proceedings of the 32nd Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications.1\u201326."},{"key":"e_1_3_4_71_1","first-page":"530","volume-title":"Proceedings of the ACM SIGPLAN Notices","author":"Torlak Emina","year":"2014","unstructured":"Emina Torlak and Rastislav Bodik. 2014. A lightweight symbolic virtual machine for solver-aided host languages. In Proceedings of the ACM SIGPLAN Notices. ACM, 530\u2013541."},{"key":"e_1_3_4_72_1","doi-asserted-by":"crossref","first-page":"564","DOI":"10.1007\/978-3-030-53291-8_29","volume-title":"Proceedings of the Computer Aided Verification Conference","author":"Geffen Jacob Van","year":"2020","unstructured":"Jacob Van Geffen, Luke Nelson, I\u015f\u0131l Dillig, Xi Wang, and Emina Torlak. 2020. Synthesizing JIT compilers for in-kernel DSLs. In Proceedings of the Computer Aided Verification Conference. Springer International Publishing, Cham, 564\u2013586."},{"key":"e_1_3_4_73_1","first-page":"1","volume-title":"Proceedings of the 33rd Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications","author":"Wang Chenglong","year":"2018","unstructured":"Chenglong Wang, Alvin Cheung, and Rastislav Bod\u00edk. 2018. Speeding up symbolic reasoning for relational queries. In Proceedings of the 33rd Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications. 1\u201325."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563943","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563943","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:15Z","timestamp":1750183695000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563943"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,3,3]]},"references-count":72,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,3,31]]}},"alternative-id":["10.1145\/3563943"],"URL":"https:\/\/doi.org\/10.1145\/3563943","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,3,3]]},"assertion":[{"value":"2021-01-19","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-08-30","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-03-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}