{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:19:20Z","timestamp":1763468360055,"version":"3.45.0"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2018,1,10]],"date-time":"2018-01-10T00:00:00Z","timestamp":1515542400000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Office of the Assistant Secretary of Defense for Research and Engineering"},{"name":"U.S. Department of Education under GAANN","award":["P200A100053"],"award-info":[{"award-number":["P200A100053"]}]},{"name":"NSF CAREER","award":["00017806"],"award-info":[{"award-number":["00017806"]}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CNS-1319748"],"award-info":[{"award-number":["CNS-1319748"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2017,5,31]]},"abstract":"<jats:p>There is no such thing as high assurance without high assurance hardware. High assurance hardware is essential because any and all high assurance systems ultimately depend on hardware that conforms to, and does not undermine, critical system properties and invariants. And yet, high assurance hardware development is stymied by the conceptual gap between formal methods and hardware description languages used by engineers. This article advocates a semantics-directed approach to bridge this conceptual gap. We present a case study in the design of secure processors, which are formally derived via principled techniques grounded in functional programming and equational reasoning. The case study comprises the development of secure single- and dual-core variants of a single processor, both based on a common semantic specification of the ISA. We demonstrate via formal equational reasoning that the dual-core processor respects a \u201cno-write-down\u201d information flow policy. The semantics-directed approach enables a modular and extensible style of system design and verification. The secure processors require only a very small amount of additional code to specify and implement, and their security verification arguments are concise and readable. Our approach rests critically on ReWire, a functional programming language providing a suitable foundation for formal verification of hardware designs. This case study demonstrates both ReWire\u2019s expressiveness as a programming language and its power as a framework for formal, high-level reasoning about hardware systems.<\/jats:p>","DOI":"10.1145\/2967497","type":"journal-article","created":{"date-parts":[[2017,1,10]],"date-time":"2017-01-10T10:41:17Z","timestamp":1484044877000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["A Principled Approach to Secure Multi-core Processor Design with ReWire"],"prefix":"10.1145","volume":"16","author":[{"given":"Adam","family":"Procter","sequence":"first","affiliation":[{"name":"University of Missouri, Columbia, MO"}]},{"given":"William L.","family":"Harrison","sequence":"additional","affiliation":[{"name":"University of Missouri, Columbia, MO"}]},{"given":"Ian","family":"Graves","sequence":"additional","affiliation":[{"name":"University of Missouri, Columbia, MO"}]},{"given":"Michela","family":"Becchi","sequence":"additional","affiliation":[{"name":"University of Missouri, Columbia, MO"}]},{"given":"Gerard","family":"Allwein","sequence":"additional","affiliation":[{"name":"U.S. Naval Research Laboratory, Washington, DC"}]}],"member":"320","published-online":{"date-parts":[[2017,1,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45340-3_2"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2228360.2228584"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289440"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_16"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/MDT.2006.134"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_18"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/FPL.2014.6927454"},{"key":"e_1_2_1_8_1","unstructured":"Andy Gill. 2011. Declarative FPGA circuit synthesis using Kansas Lava. In ERSA\u201911."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2611429.2617811"},{"key":"e_1_2_1_10_1","unstructured":"Carlos Eduardo Gim\u00e9nez. 1996. Un Calcul De Constructions Infinies Et Son Application A La Verification De Systemes Communicants. Ph.D. Dissertation. L\u2019\u00c9cole Normale Sup\u00e9rieure de Lyon."},{"volume-title":"Proceedings of the 1982 Symposium on Security and Privacy (SSP\u201982)","author":"Joseph","key":"e_1_2_1_11_1","unstructured":"Joseph A. Goguen and Jos\u00e9 Meseguer. 1990. Security policies and security models. In Proceedings of the 1982 Symposium on Security and Privacy (SSP\u201982). IEEE Computer Society Press, 11--20."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/2034214.2034238"},{"key":"e_1_2_1_13_1","unstructured":"Ian Graves. 2015. Device-Level Composition in ReWire. Ph.D. Dissertation. University of Missouri."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03034-5_2"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11924661_6"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1662658.1662663"},{"key":"e_1_2_1_17_1","volume-title":"Harrison and Adam Procter","author":"William","year":"2015","unstructured":"William L. Harrison and Adam Procter. 2015. Cheap (but functional) threads. Submitted to the Journal of Functional Programming."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34281-3_15"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2011.68"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993512"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/926535"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199528"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/361011.361073"},{"key":"e_1_2_1_25_1","unstructured":"Adam Procter. 2014. Semantics-Driven Design and Implementation of High-Assurance Hardware. Ph.D. Dissertation. University of Missouri."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","unstructured":"Adam Procter William L. Harrison Ian Graves Michela Becchi and Gerard Allwein. 2015b. Online supplement accompanying \u201cA Principled Approach to Secure Multi-Core Processor Design in ReWire\u201d. Retrieved from http:\/\/adamprocter.com\/tecs15. 10.1145\/2967497","DOI":"10.1145\/2967497"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2670529.2754970"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2003.819898"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480929"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00053-0"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/353629.353648"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","unstructured":"Matthew Wilding David Greve Raymond Richards and David Hardin. 2010. Formal verification of partition management for the AAMP7G microprocessor. In Design and Verification of Microprocessor Systems for High-Assurance Applications David S. Hardin (Ed.). 175--191. 10.1007\/978-1-4419-1539-9_6","DOI":"10.1007\/978-1-4419-1539-9_6"},{"volume-title":"PicoBlaze 8-bit Embedded Microcontroller User Guide. Xilinx","key":"e_1_2_1_34_1","unstructured":"Xilinx. 2011. PicoBlaze 8-bit Embedded Microcontroller User Guide. Xilinx, Inc."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/2830840.2830850"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2967497","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2967497","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2967497","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:45:59Z","timestamp":1763459159000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2967497"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1,10]]},"references-count":35,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,5,31]]}},"alternative-id":["10.1145\/2967497"],"URL":"https:\/\/doi.org\/10.1145\/2967497","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2017,1,10]]},"assertion":[{"value":"2015-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-06-01","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-01-10","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}