{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,5]],"date-time":"2026-03-05T16:19:15Z","timestamp":1772727555774,"version":"3.50.1"},"reference-count":114,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2023,1,19]],"date-time":"2023-01-19T00:00:00Z","timestamp":1674086400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Science Foundation","award":["1419869, 1524680"],"award-info":[{"award-number":["1419869, 1524680"]}]},{"DOI":"10.13039\/100000028","name":"Semiconductor Research Corporation","doi-asserted-by":"crossref","award":["2015-TS-2633"],"award-info":[{"award-number":["2015-TS-2633"]}],"id":[{"id":"10.13039\/100000028","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Google PhD Fellowship"},{"DOI":"10.13039\/501100004410","name":"TUBITAK","doi-asserted-by":"crossref","award":["2219"],"award-info":[{"award-number":["2219"]}],"id":[{"id":"10.13039\/501100004410","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. Emerg. Technol. Comput. Syst."],"published-print":{"date-parts":[[2023,1,31]]},"abstract":"<jats:p>This article surveys the landscape of security verification approaches and techniques for computer systems at various levels: from a software-application level all the way to the physical hardware level. Different existing projects are compared, based on the tools used and security aspects being examined. Since many systems require both hardware and software components to work together to provide the system\u2019s promised security protections, it is not sufficient to verify just the software levels or just the hardware levels in a mutually exclusive fashion. This survey especially highlights system levels that are verified by the different existing projects and presents to the readers the state of the art in hardware and software system security verification. Few approaches come close to providing full-system verification, and there is still much room for\u00a0improvement.<\/jats:p>","DOI":"10.1145\/3564785","type":"journal-article","created":{"date-parts":[[2022,10,6]],"date-time":"2022-10-06T12:19:46Z","timestamp":1665058786000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Survey of Approaches and Techniques for Security Verification of Computer Systems"],"prefix":"10.1145","volume":"19","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6305-4266","authenticated-orcid":false,"given":"Ferhat","family":"Erata","sequence":"first","affiliation":[{"name":"Yale University, New Haven, CT, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9782-5038","authenticated-orcid":false,"given":"Shuwen","family":"Deng","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, CT, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5371-1231","authenticated-orcid":false,"given":"Faisal","family":"Zaghloul","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, CT, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7626-2651","authenticated-orcid":false,"given":"Wenjie","family":"Xiong","sequence":"additional","affiliation":[{"name":"Virginia Tech, Blacksburg, VA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1088-6461","authenticated-orcid":false,"given":"Onur","family":"Demir","sequence":"additional","affiliation":[{"name":"Yeditepe \u00dcniversitesi, Istanbul, Turkey"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9721-3640","authenticated-orcid":false,"given":"Jakub","family":"Szefer","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, CT, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,19]]},"reference":[{"key":"e_1_3_1_2_2","unstructured":"AMD. 2016. AMD Memory Encryption. Retrieved from http:\/\/amd-dev.wpengine.netdna-cdn.com\/wordpress\/media\/2013\/12\/AMD_Memory_Encryption_Whitepaper_v7-Public.pdf."},{"key":"e_1_3_1_3_2","volume-title":"Proceedings of the 2nd International Workshop on Hardware and Architectural Support for Security and Privacy","author":"Anati Ittai","year":"2013","unstructured":"Ittai Anati, Shay Gueron, Simon Johnson, and Vincent Scarlata. 2013. Innovative technology for CPU-based attestation and sealing. In Proceedings of the 2nd International Workshop on Hardware and Architectural Support for Security and Privacy."},{"key":"e_1_3_1_4_2","first-page":"1691","volume-title":"Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE\u201917)","author":"Ardeshiricham Armaiti","year":"2017","unstructured":"Armaiti Ardeshiricham, Wei Hu, Joshua Marxen, and Ryan Kastner. 2017. Register transfer level information flow tracking for provably secure hardware design. In Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE\u201917). IEEE, 1691\u20131696."},{"key":"e_1_3_1_5_2","article-title":"The rocket chip generator","volume":"4","author":"Asanovic Krste","year":"2016","unstructured":"Krste Asanovic, Rimas Avizienis, Jonathan Bachrach, Scott Beamer, David Biancolin, Christopher Celio, Henry Cook, Daniel Dabbelt, John Hauser, Adam Izraelevitz, et\u00a0al. 2016. The rocket chip generator. EECS Department, University of California, Berkeley, Tech. Rep. UCB\/EECS-2016-17, Vol. 4.","journal-title":"EECS Department, University of California, Berkeley, Tech. Rep. UCB\/EECS-2016-17,"},{"key":"e_1_3_1_6_2","first-page":"165","volume-title":"ACM SIGPLAN Notices","author":"Amorim Arthur Azevedo de","year":"2014","unstructured":"Arthur Azevedo de Amorim, Nathan Collins, Andr\u00e9 DeHon, Delphine Demange, C\u0103t\u0103lin Hri\u0163cu, David Pichardie, Benjamin C. Pierce, Randy Pollack, and Andrew Tolmach. 2014. A verified information-flow architecture. In ACM SIGPLAN Notices, Vol. 49. ACM, 165\u2013178."},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/2228360.2228584"},{"key":"e_1_3_1_8_2","volume-title":"Principles of Model Checking","author":"Baier Christel","year":"2008","unstructured":"Christel Baier, Joost-Pieter Katoen, et\u00a0al. 2008. Principles of Model Checking. MIT Press, Cambridge, MA."},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_1_11_2","volume-title":"Systems and Software Verification: Model-checking Techniques and Tools","author":"B\u00e9rard B\u00e9atrice","year":"2013","unstructured":"B\u00e9atrice B\u00e9rard, Michel Bidoit, Alain Finkel, Fran\u00e7ois Laroussinie, Antoine Petit, Laure Petrucci, and Philippe Schnoebelen. 2013. Systems and Software Verification: Model-checking Techniques and Tools. Springer Science & Business Media."},{"key":"e_1_3_1_12_2","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-319-08587-6_12","volume-title":"Automated Reasoning","author":"Berdine Josh","year":"2014","unstructured":"Josh Berdine and Nikolaj Bj\u00f8rner. 2014. Computing all implied equalities via SMT-based partition refinement. In Automated Reasoning. Springer, 168\u2013183."},{"key":"e_1_3_1_13_2","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Bertot Yves","year":"2013","unstructured":"Yves Bertot and Pierre Cast\u00e9ran. 2013. Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Springer Science & Business Media."},{"key":"e_1_3_1_14_2","first-page":"163","volume-title":"Proceedings of the International Symposium on Hardware Oriented Security and Trust (HOST\u201915)","author":"Bidmeshki M. M.","year":"2015","unstructured":"M. M. Bidmeshki and Y. Makris. 2015. Toward automatic proof generation for information flow policies in third-party hardware IP. In Proceedings of the International Symposium on Hardware Oriented Security and Trust (HOST\u201915). 163\u2013168."},{"key":"e_1_3_1_15_2","first-page":"29","volume-title":"Proceedings of the International Symposium on Circuits and Systems (ISCAS\u201915)","author":"Bidmeshki Mohammad-Mahdi","year":"2015","unstructured":"Mohammad-Mahdi Bidmeshki and Yiorgos Makris. 2015. VeriCoq: A verilog-to-coq converter for proof-carrying hardware automation. In Proceedings of the International Symposium on Circuits and Systems (ISCAS\u201915). IEEE, 29\u201332."},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"e_1_3_1_17_2","first-page":"917","volume-title":"Proceedings of the 26th USENIX Security Symposium (USENIXSecurity\u201917)","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 (USENIXSecurity\u201917). 917\u2013934."},{"key":"e_1_3_1_18_2","first-page":"463","volume-title":"BAP: A Binary Analysis Platform","author":"Brumley David","year":"2011","unstructured":"David Brumley, Ivan Jager, Thanassis Avgerinos, and Edward J. Schwartz. 2011. BAP: A Binary Analysis Platform. Springer, Berlin, 463\u2013469."},{"key":"e_1_3_1_19_2","first-page":"209","volume-title":"Proceedings of the USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908)","volume":"8","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, Dawson R. Engler, et\u00a0al. 2008. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908), Vol. 8. 209\u2013224."},{"key":"e_1_3_1_20_2","unstructured":"CADENCE. 2016. JasperGold Security Path Verification App. Retrieved from http:\/\/www.cadence.com\/products\/fv\/jaspergold_security\/pages\/default.aspx."},{"key":"e_1_3_1_21_2","first-page":"1","volume-title":"Proceedings of the International Symposium on High Performance Computer Architecture (HPCA\u201910)","author":"Champagne David","year":"2010","unstructured":"David Champagne and Ruby B. Lee. 2010. Scalable architectural support for trusted software. In Proceedings of the International Symposium on High Performance Computer Architecture (HPCA\u201910). IEEE, 1\u201312."},{"key":"e_1_3_1_22_2","first-page":"183","volume-title":"ACM SIGPLAN Notices","author":"Chen Juan","year":"2008","unstructured":"Juan Chen, Chris Hawblitzel, Frances Perry, Mike Emmi, Jeremy Condit, Derrick Coetzee, and Polyvios Pratikaki. 2008. Type-preserving compilation for large-scale optimizing object-oriented compilers. In ACM SIGPLAN Notices, Vol. 43. ACM, 183\u2013192."},{"key":"e_1_3_1_23_2","first-page":"93","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Cimatti Alessandro","year":"2013","unstructured":"Alessandro Cimatti, Alberto Griggio, Bastiaan Schaafsma, and Roberto Sebastiani. 2013. The MathSAT5 SMT solver. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 93\u2013107."},{"key":"e_1_3_1_24_2","first-page":"124","volume-title":"A Decade of Concurrency Reflections and Perspectives","author":"Clarke Edmund","year":"1993","unstructured":"Edmund Clarke, Orna Grumberg, and D. Long. 1993. Verification tools for finite-state concurrent systems. In A Decade of Concurrency Reflections and Perspectives. Springer, 124\u2013175."},{"key":"e_1_3_1_25_2","first-page":"1","volume-title":"Proceedings of the LASER Summer School on Software Engineering","author":"Clarke Edmund M.","year":"2011","unstructured":"Edmund M. Clarke, William Klieber, Milo\u0161 Nov\u00e1\u010dek, and Paolo Zuliani. 2011. Model checking and the state explosion problem. In Proceedings of the LASER Summer School on Software Engineering. Springer, 1\u201330."},{"key":"e_1_3_1_26_2","article-title":"Intel SGX Explained","author":"Costan Victor","year":"2016","unstructured":"Victor Costan and Srinivas Devadas. 2016. Intel SGX Explained. Cryptology ePrint Archive, Paper 2016\/086. Retrieved from https:\/\/eprint.iacr.org\/2016\/086.","journal-title":"Cryptology ePrint Archive, Paper 2016\/086"},{"key":"e_1_3_1_27_2","article-title":"Sanctum: Minimal Hardware Extensions for Strong Software Isolation","author":"Costan Victor","year":"2015","unstructured":"Victor Costan, Ilia Lebedev, and Srinivas Devadas. 2015. Sanctum: Minimal Hardware Extensions for Strong Software Isolation. Cryptology ePrint Archive, Paper 2015\/564. Retrieved from https:\/\/eprint.iacr.org\/2015\/564.","journal-title":"Cryptology ePrint Archive, Paper 2015\/564"},{"key":"e_1_3_1_28_2","volume-title":"Elements of Information Theory","author":"Cover Thomas M.","year":"2012","unstructured":"Thomas M. Cover and Joy A. Thomas. 2012. Elements of Information Theory. John Wiley & Sons."},{"key":"e_1_3_1_29_2","volume-title":"Toward a Foundational Typed Assembly Language","author":"Crary Karl","year":"2003","unstructured":"Karl Crary. 2003. Toward a Foundational Typed Assembly Language. ACM."},{"key":"e_1_3_1_30_2","doi-asserted-by":"crossref","unstructured":"Mike Dahlin Ryan Johnson Robert Bellarmine Krug Michael McCoyd and William Young. 2011. Toward the verification of a simple hypervisor. Retrieved from https:\/\/arXiv:1110.4672.","DOI":"10.4204\/EPTCS.70.3"},{"key":"e_1_3_1_31_2","doi-asserted-by":"crossref","first-page":"813","DOI":"10.1109\/SP.2015.55","volume-title":"Proceedings of the IEEE Symposium on Security and Privacy (SP\u201915)","author":"Amorim Arthur Azevedo De","year":"2015","unstructured":"Arthur Azevedo De Amorim, Maxime D\u00e9nes, Nick Giannarakis, Catalin Hritcu, Benjamin C. Pierce, Antal Spector-Zabusky, and Andrew Tolmach. 2015. Micro-policies: Formally verified, tag-based security monitors. In Proceedings of the IEEE Symposium on Security and Privacy (SP\u201915). IEEE, 813\u2013830."},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/2611765.2611773"},{"key":"e_1_3_1_34_2","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/3-540-61474-5_86","volume-title":"Computer Aided Verification","author":"Dill David L.","year":"1996","unstructured":"David L. Dill. 1996. The mur \\(\\phi\\) verification system. In Computer Aided Verification. Springer, 390\u2013393."},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.5555\/3437539.3437752"},{"key":"e_1_3_1_36_2","first-page":"994","volume-title":"Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE\u201919)","author":"Fadiheh Mohammad Rahmani","year":"2019","unstructured":"Mohammad Rahmani Fadiheh, Dominik Stoffel, Clark Barrett, Subhasish Mitra, and Wolfgang Kunz. 2019. Processor hardware security vulnerabilities and their detection by unique program execution checking. In Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE\u201919). IEEE, 994\u2013999."},{"key":"e_1_3_1_37_2","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1145\/3132747.3132782","volume-title":"Proceedings of the 26th Symposium on Operating Systems Principles","author":"Ferraiuolo Andrew","year":"2017","unstructured":"Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, and Bryan Parno. 2017. Komodo: Using verification to disentangle secure-enclave hardware from software. In Proceedings of the 26th Symposium on Operating Systems Principles. ACM, 287\u2013305."},{"key":"e_1_3_1_38_2","first-page":"1","volume-title":"Proceedings of the 54th Design Automation Conference (DAC\u201917)","author":"Ferraiuolo Andrew","year":"2017","unstructured":"Andrew Ferraiuolo, Weizhe Hua, Andrew C. Myers, and G. Edward Suh. 2017. Secure information flow verification with mutable dependent types. In Proceedings of the 54th Design Automation Conference (DAC\u201917). IEEE, 1\u20136."},{"key":"e_1_3_1_39_2","volume-title":"Lightweight Verification of Secure Hardware Isolation Through Static Information Flow Analysis","author":"Ferraiuolo Andrew","year":"2017","unstructured":"Andrew Ferraiuolo, Rui Xu, Danfeng Zhang, Andrew C. Myers, and G. Edward Suh. 2017. Lightweight Verification of Secure Hardware Isolation Through Static Information Flow Analysis. Technical report, Cornell University."},{"key":"e_1_3_1_40_2","first-page":"555","volume-title":"Proceedings of the 22nd International Conference on Architectural Support for Programming Languages and Operating Systems","author":"Ferraiuolo Andrew","year":"2017","unstructured":"Andrew Ferraiuolo, Rui Xu, Danfeng Zhang, Andrew C. Myers, and G. Edward Suh. 2017. Verification of a practical hardware security architecture through static information flow analysis. In Proceedings of the 22nd International Conference on Architectural Support for Programming Languages and Operating Systems. ACM, 555\u2013568."},{"key":"e_1_3_1_41_2","first-page":"1583","volume-title":"Proceedings of the ACM SIGSAC Conference on Computer and Communications Security","author":"Ferraiuolo Andrew","year":"2018","unstructured":"Andrew Ferraiuolo, Mark Zhao, Andrew C. Myers, and G. Edward Suh. 2018. HyperFlow: A processor architecture for nonmalleable, timing-safe information flow security. In Proceedings of the ACM SIGSAC Conference on Computer and Communications Security. 1583\u20131600."},{"key":"e_1_3_1_42_2","first-page":"187","volume-title":"Proceedings of the International Conference on Interactive Theorem Proving","author":"Fox Anthony","year":"2015","unstructured":"Anthony Fox. 2015. Improved tool support for machine-code decompilation in HOL4. In Proceedings of the International Conference on Interactive Theorem Proving. Springer, 187\u2013202."},{"key":"e_1_3_1_43_2","volume-title":"Attacking, Repairing, and Verifying SecVisor: A Retrospective on the Security of a Hypervisor","author":"Franklin Jason","year":"2008","unstructured":"Jason Franklin, Arvind Seshadri, Ning Qu, Sagar Chaki, and Anupam Datta. 2008. Attacking, Repairing, and Verifying SecVisor: A Retrospective on the Security of a Hypervisor. Technical Report CMU-CyLab-08-008, Carnegie Mellon University."},{"key":"e_1_3_1_44_2","first-page":"443","volume-title":"Proceedings of the 9th International Conference on Soft Computing Models in Industrial and Environmental Applications (SOCO\u201914), International Joint Conference Computational Intelligence in Security for Information Systems, 7th International Conference (CISIS\u201914) and European Transnational Education, 5th International Conference (ICEUTE\u201913)","author":"Garc\u0131a-Ferreira Iv\u00e1n","year":"2014","unstructured":"Iv\u00e1n Garc\u0131a-Ferreira, Carlos Laorden, Igor Santos, and Pablo Garcia Bringas. 2014. A survey on static analysis and model checking. In Proceedings of the 9th International Conference on Soft Computing Models in Industrial and Environmental Applications (SOCO\u201914), International Joint Conference Computational Intelligence in Security for Information Systems, 7th International Conference (CISIS\u201914) and European Transnational Education, 5th International Conference (ICEUTE\u201913). 443."},{"key":"e_1_3_1_45_2","unstructured":"Mentor Graphics. 2016. Mentor Graphics Questa Secure Check. Retrieved from https:\/\/www.mentor.com\/products\/fv\/questa-secure-check."},{"key":"e_1_3_1_46_2","first-page":"595","volume-title":"ACM SIGPLAN Notices","author":"Gu Ronghui","year":"2015","unstructured":"Ronghui Gu, J\u00e9r\u00e9mie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan Newman Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. 2015. Deep specifications and certified abstraction layers. In ACM SIGPLAN Notices, Vol. 50. ACM, 595\u2013608."},{"key":"e_1_3_1_47_2","first-page":"35","volume-title":"Proceedings of the 17th International Workshop on Microprocessor and SOC Test and Verification (MTV\u201916)","author":"Guo Xiaolong","year":"2016","unstructured":"Xiaolong Guo, Raj Gautam Dutta, Prabhat Mishra, and Yier Jin. 2016. Automatic RTL-to-formal code converter for IP security formal verification. In Proceedings of the 17th International Workshop on Microprocessor and SOC Test and Verification (MTV\u201916). IEEE, 35\u201338."},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.5555\/1018441.1021997"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050043"},{"key":"e_1_3_1_51_2","first-page":"165","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201914)","author":"Hawblitzel Chris","year":"2014","unstructured":"Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. 2014. Ironclad apps: End-to-end security via automated full-system verification. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201914). 165\u2013181."},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3466752.3480087"},{"key":"e_1_3_1_54_2","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson Daniel","year":"2012","unstructured":"Daniel Jackson. 2012. Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge, MA."},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3338843"},{"key":"e_1_3_1_56_2","first-page":"824","volume-title":"Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD\u201913)","author":"Jin Yier","year":"2013","unstructured":"Yier Jin and Yiorgos Makris. 2013. A proof-carrying-based framework for trusted microprocessor IP. In Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD\u201913). IEEE, 824\u2013829."},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_4"},{"key":"e_1_3_1_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_1_59_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00002"},{"key":"e_1_3_1_60_2","first-page":"389","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Kroening Daniel","year":"2014","unstructured":"Daniel Kroening and Michael Tautschnig. 2014. CBMC\u2013C bounded model checker. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 389\u2013391."},{"key":"e_1_3_1_61_2","volume-title":"Proceedings of the BSD Conference","volume":"5","author":"Lattner Chris","year":"2008","unstructured":"Chris Lattner. 2008. LLVM and clang: Next generation compiler technology. In Proceedings of the BSD Conference, Vol. 5."},{"key":"e_1_3_1_62_2","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"Leino K. Rustan M.","year":"2010","unstructured":"K. Rustan M. Leino. 2010. Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning. Springer, 348\u2013370."},{"key":"e_1_3_1_63_2","article-title":"The CompCert C verified compiler","author":"Leroy Xavier","year":"2012","unstructured":"Xavier Leroy. 2012. The CompCert C verified compiler. Documentation and User\u2019s Manual. INRIA Paris-Rocquencourt.","journal-title":"Documentation and User\u2019s Manual. INRIA Paris-Rocquencourt"},{"key":"e_1_3_1_64_2","volume-title":"Capability-based Computer Systems","author":"Levy Henry M.","year":"2014","unstructured":"Henry M. Levy. 2014. Capability-based Computer Systems. Digital Press."},{"key":"e_1_3_1_65_2","first-page":"97","volume-title":"ACM SIGARCH Computer Architecture News","author":"Li Xun","year":"2014","unstructured":"Xun Li, Vineeth Kashyap, Jason K. Oberg, Mohit Tiwari, Vasanth Ram Rajarathinam, Ryan Kastner, Timothy Sherwood, Ben Hardekopf, and Frederic T. Chong. 2014. Sapper: A language for hardware-level security policy enforcement. In ACM SIGARCH Computer Architecture News, Vol. 42. ACM, 97\u2013112."},{"key":"e_1_3_1_66_2","first-page":"109","volume-title":"ACM SIGPLAN Notices","author":"Li Xun","year":"2011","unstructured":"Xun Li, Mohit Tiwari, Jason K. Oberg, Vineeth Kashyap, Frederic T. Chong, Timothy Sherwood, and Ben Hardekopf. 2011. Caisson: A hardware description language for secure information flow. In ACM SIGPLAN Notices, Vol. 46. ACM, 109\u2013120."},{"key":"e_1_3_1_67_2","first-page":"123","volume-title":"ProQuest Dissertations and Theses","author":"Liang Sheng","year":"1998","unstructured":"Sheng Liang. 1998. Modular monadic semantics and compilation. ProQuest Dissertations and Theses. (1998), 123. https:\/\/www.proquest.com\/dissertations-theses\/modular-monadic-semantics-compilation\/docview\/304460399\/se-2."},{"key":"e_1_3_1_68_2","first-page":"166","volume-title":"Proceedings of the Symposium on Security and Privacy","author":"Lie David","year":"2003","unstructured":"David Lie, John Mitchell, Chandramohan A. Thekkath, and Mark Horowitz. 2003. Specifying and verifying hardware for tamper-resistant software. In Proceedings of the Symposium on Security and Privacy. IEEE, 166\u2013177."},{"key":"e_1_3_1_69_2","doi-asserted-by":"publisher","DOI":"10.1145\/356989.357005"},{"key":"e_1_3_1_70_2","first-page":"973","volume-title":"Proceedings of the 27th USENIX Security Symposium (USENIXSecurity\u201918)","author":"Lipp Moritz","year":"2018","unstructured":"Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Anders Fogh, Jann Horn, Stefan Mangard, Paul Kocher, Daniel Genkin, et\u00a0al. 2018. Meltdown: Reading kernel memory from user space. In Proceedings of the 27th USENIX Security Symposium (USENIXSecurity\u201918). 973\u2013990."},{"key":"e_1_3_1_71_2","volume-title":"VHDL: Hardware Description and Design","author":"Lipsett Roger","year":"2012","unstructured":"Roger Lipsett, Carl F. Schaefer, and Cary Ussery. 2012. VHDL: Hardware Description and Design. Springer Science & Business Media."},{"key":"e_1_3_1_72_2","first-page":"605","volume-title":"Proceedings of the IEEE Symposium on Security and Privacy","author":"Liu Fangfei","year":"2015","unstructured":"Fangfei Liu, Yuval Yarom, Qian Ge, Gernot Heiser, and Ruby B. Lee. 2015. Last-level cache side-channel attacks are practical. In Proceedings of the IEEE Symposium on Security and Privacy. 605\u2013622."},{"key":"e_1_3_1_73_2","volume-title":"Proceedings of the Workshop on Reproducible Research Methodologies (REPRODUCE\u201914)","author":"Lockhart Derek","year":"2014","unstructured":"Derek Lockhart and Christopher Batten. 2014. Hardware generation languages as a foundation for credible, reproducible, and productive research methodologies. In Proceedings of the Workshop on Reproducible Research Methodologies (REPRODUCE\u201914)."},{"key":"e_1_3_1_74_2","doi-asserted-by":"publisher","DOI":"10.1145\/2487726.2488368"},{"key":"e_1_3_1_75_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6_4"},{"key":"e_1_3_1_76_2","article-title":"RTL-ConTest: Concolic testing on RTL for detecting security vulnerabilities","author":"Meng Xingyu","year":"2021","unstructured":"Xingyu Meng, Shamik Kundu, Arun K. Kanuparthi, and Kanad Basu. 2021. RTL-ConTest: Concolic testing on RTL for detecting security vulnerabilities. IEEE Trans. Comput.-Aided Design Integr. Circ. Syst. 41, 3 (2021), 466\u2013477.","journal-title":"IEEE Trans. Comput.-Aided Design Integr. Circ. Syst."},{"key":"e_1_3_1_77_2","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319345"},{"key":"e_1_3_1_78_2","first-page":"568","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Myreen Magnus O.","year":"2007","unstructured":"Magnus O. Myreen and Michael J. C. Gordon. 2007. Hoare logic for realistically modelled machine code. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 568\u2013582."},{"key":"e_1_3_1_79_2","doi-asserted-by":"publisher","DOI":"10.1145\/1273442.1250746"},{"key":"e_1_3_1_80_2","first-page":"69","volume-title":"Proceedings of the 2nd ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE\u201904)","author":"Nikhil Rishiyur","year":"2004","unstructured":"Rishiyur Nikhil. 2004. Bluespec system verilog: Efficient, correct RTL from high level specifications. In Proceedings of the 2nd ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE\u201904). IEEE, 69\u201370."},{"key":"e_1_3_1_81_2","doi-asserted-by":"publisher","DOI":"10.5555\/1791547"},{"key":"e_1_3_1_82_2","first-page":"1","volume-title":"Proceedings of the Cryptographers\u2019 Track at the RSA Conference","author":"Osvik Dag Arne","year":"2006","unstructured":"Dag Arne Osvik, Adi Shamir, and Eran Tromer. 2006. Cache attacks and countermeasures: The case of AES. In Proceedings of the Cryptographers\u2019 Track at the RSA Conference. Springer, 1\u201320."},{"key":"e_1_3_1_83_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55602-8_217"},{"key":"e_1_3_1_84_2","first-page":"45","volume-title":"Tools for Practical Software Verification","author":"Paulin-Mohring Christine","year":"2011","unstructured":"Christine Paulin-Mohring. 2011. Introduction to the Coq proof-assistant for practical software verification. In Tools for Practical Software Verification. Springer, 45\u201395."},{"key":"e_1_3_1_85_2","first-page":"13","volume-title":"ACM SIGPLAN Notices","author":"Procter Adam","year":"2015","unstructured":"Adam Procter, William L. Harrison, Ian Graves, Michela Becchi, and Gerard Allwein. 2015. Semantics driven hardware design, implementation, and verification with ReWire. In ACM SIGPLAN Notices, Vol. 50. ACM, 13."},{"key":"e_1_3_1_86_2","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_3_1_87_2","unstructured":"Bruce Schneier. 2016. The Internet of Things Will Turn Large-Scale Hacks into Real World Disaster. Retrieved from https:\/\/motherboard.vice.com\/read\/the-internet-of-things-will-cause-the-first-ever-large-scale-internet-disaster."},{"key":"e_1_3_1_88_2","first-page":"27","volume-title":"Proceedings of the International Conference on Software Engineering and Formal Methods","author":"Schwarz Oliver","year":"2016","unstructured":"Oliver Schwarz and Mads Dam. 2016. Automatic derivation of platform noninterference properties. In Proceedings of the International Conference on Software Engineering and Formal Methods. Springer, 27\u201344."},{"key":"e_1_3_1_89_2","doi-asserted-by":"publisher","DOI":"10.1145\/1323293.1294294"},{"key":"e_1_3_1_90_2","first-page":"1","volume-title":"Proceedings of the 16th ACM\/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE\u201918)","author":"Seshia Sanjit A.","year":"2018","unstructured":"Sanjit A. Seshia and Pramod Subramanyan. 2018. UCLID5: Integrating modeling, verification, synthesis and learning. In Proceedings of the 16th ACM\/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE\u201918). IEEE, 1\u201310."},{"key":"e_1_3_1_91_2","doi-asserted-by":"crossref","first-page":"623","DOI":"10.1145\/2228360.2228472","volume-title":"Proceedings of the 49th Annual Design Automation Conference","author":"Shacham Ofer","year":"2012","unstructured":"Ofer Shacham, Megan Wachs, Andrew Danowitz, Sameh Galal, John Brunhaver, Wajahat Qadeer, Sabarish Sankaranarayanan, Artem Vassiliev, Stephen Richardson, and Mark Horowitz. 2012. Avoiding game over: Bringing design to the next level. In Proceedings of the 49th Annual Design Automation Conference. ACM, 623\u2013629."},{"key":"e_1_3_1_92_2","first-page":"138","volume-title":"Proceedings of the IEEE Symposium on Security and Privacy (SP\u201916)","author":"Shoshitaishvili Yan","year":"2016","unstructured":"Yan Shoshitaishvili, Ruoyu Wang, Christopher Salls, Nick Stephens, Mario Polino, Andrew Dutcher, John Grosen, Siji Feng, Christophe Hauser, Christopher Kruegel, et\u00a0al. 2016. SOK: (State of) the art of war: Offensive techniques in binary analysis. In Proceedings of the IEEE Symposium on Security and Privacy (SP\u201916). IEEE, 138\u2013157."},{"issue":"7","key":"e_1_3_1_93_2","doi-asserted-by":"crossref","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","article-title":"A survey of automated techniques for formal software verification","volume":"27","author":"Silva Vijay D.","year":"2008","unstructured":"Vijay D. Silva, Daniel Kroening, and Georg Weissenbacher. 2008. A survey of automated techniques for formal software verification. IEEE Trans. Computer-Aided Design Integr. Circ. Syst. 27, 7 (2008), 1165\u20131178.","journal-title":"IEEE Trans. Computer-Aided Design Integr. Circ. Syst."},{"key":"e_1_3_1_94_2","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908113"},{"key":"e_1_3_1_95_2","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813608"},{"key":"e_1_3_1_96_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134098"},{"key":"e_1_3_1_97_2","first-page":"437","volume-title":"ACM SIGPLAN Notices","author":"Szefer Jakub","year":"2012","unstructured":"Jakub Szefer and Ruby B. Lee. 2012. Architectural support for hypervisor-secure virtualization. In ACM SIGPLAN Notices, Vol. 47. ACM, 437\u2013450."},{"key":"e_1_3_1_98_2","doi-asserted-by":"publisher","DOI":"10.5555\/1502144"},{"key":"e_1_3_1_99_2","doi-asserted-by":"publisher","DOI":"10.1145\/358198.358210"},{"key":"e_1_3_1_100_2","doi-asserted-by":"publisher","DOI":"10.1145\/1508244.1508258"},{"key":"e_1_3_1_101_2","first-page":"947","volume-title":"Proceedings of the 51st Annual IEEE\/ACM International Symposium on Microarchitecture (MICRO\u201918)","author":"Trippel Caroline","year":"2018","unstructured":"Caroline Trippel, Daniel Lustig, and Margaret Martonosi. 2018. Checkmate: Automated synthesis of hardware exploits and security litmus tests. In Proceedings of the 51st Annual IEEE\/ACM International Symposium on Microarchitecture (MICRO\u201918). IEEE, 947\u2013960."},{"key":"e_1_3_1_102_2","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2019.2910010"},{"key":"e_1_3_1_103_2","volume-title":"TrustZone Information Page","author":"Trustzone ARM","year":"2016","unstructured":"ARM Trustzone. 2016. TrustZone Information Page. Technical Report. Retrieved from http:\/\/www.arm.com\/products\/processors\/technologies\/trustzone\/."},{"key":"e_1_3_1_104_2","first-page":"429","volume-title":"Advanced Course on Petri Nets","author":"Valmari Antti","year":"1996","unstructured":"Antti Valmari. 1996. The state explosion problem. In Advanced Course on Petri Nets. Springer, 429\u2013528."},{"key":"e_1_3_1_105_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.36"},{"key":"e_1_3_1_106_2","doi-asserted-by":"publisher","DOI":"10.1109\/52.28119"},{"key":"e_1_3_1_107_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-1539-9_6"},{"key":"e_1_3_1_108_2","first-page":"99","volume-title":"ACM Sigplan Notices","author":"Yang Jean","year":"2010","unstructured":"Jean Yang and Chris Hawblitzel. 2010. Safe to the last instruction: Automated verification of a type-safe operating system. In ACM Sigplan Notices, Vol. 45. ACM, 99\u2013110."},{"key":"e_1_3_1_109_2","doi-asserted-by":"publisher","DOI":"10.1145\/2043174.2043197"},{"key":"e_1_3_1_110_2","first-page":"719","volume-title":"Proceedings of the 23rd USENIX Security Symposium (USENIXSecurity\u201914)","author":"Yarom Yuval","year":"2014","unstructured":"Yuval Yarom and Katrina Falkner. 2014. FLUSH+ RELOAD: A high resolution, low noise, L3 cache side-channel attack. In Proceedings of the 23rd USENIX Security Symposium (USENIXSecurity\u201914). 719\u2013732."},{"key":"e_1_3_1_111_2","doi-asserted-by":"publisher","DOI":"10.1145\/2345156.2254078"},{"key":"e_1_3_1_112_2","first-page":"503","volume-title":"ACM SIGARCH Computer Architecture News","author":"Zhang Danfeng","year":"2015","unstructured":"Danfeng Zhang, Yao Wang, G. Edward Suh, and Andrew C. Myers. 2015. A hardware design language for timing-sensitive information-flow security. In ACM SIGARCH Computer Architecture News, Vol. 43. ACM, 503\u2013516."},{"key":"e_1_3_1_113_2","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2018.00071"},{"key":"e_1_3_1_114_2","doi-asserted-by":"publisher","DOI":"10.1145\/2664243.2664273"},{"key":"e_1_3_1_115_2","volume-title":"Secure Cache Modeling for Measuring Side-channel Leakage","author":"Zhang Tianwei","year":"2014","unstructured":"Tianwei Zhang and Ruby B. Lee. 2014. Secure Cache Modeling for Measuring Side-channel Leakage. Technical Report. Retrieved from http:\/\/palms.ee.princeton.edu\/node."}],"container-title":["ACM Journal on Emerging Technologies in Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3564785","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3564785","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:51:23Z","timestamp":1750182683000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3564785"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,19]]},"references-count":114,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,1,31]]}},"alternative-id":["10.1145\/3564785"],"URL":"https:\/\/doi.org\/10.1145\/3564785","relation":{},"ISSN":["1550-4832","1550-4840"],"issn-type":[{"value":"1550-4832","type":"print"},{"value":"1550-4840","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,19]]},"assertion":[{"value":"2021-12-23","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-01-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}