research-article

Open access

A Verification Methodology for the Arm® Confidential Computing Architecture: From a Secure Specification to Safe Implementations

Authors:

Anthony C. J. Fox,

Gareth Stockwell,

Dominic P. Mulligan,

Nathan ChongAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 7, Issue OOPSLA1

Article No.: 88, Pages 376 - 405

https://doi.org/10.1145/3586040

Published: 06 April 2023 Publication History

Abstract

We present Arm's efforts in verifying the specification and prototype reference implementation of the Realm Management Monitor (RMM), an essential firmware component of Arm Confidential Computing Architecture (Arm CCA), the recently-announced Confidential Computing technologies incorporated in the Armv9-A architecture. Arm CCA introduced the Realm Management Extension (RME), an architectural extension for Armv9-A, and a technology that will eventually be deployed in hundreds of millions of devices. Given the security-critical nature of the RMM, and its taxing threat model, we use a combination of interactive theorem proving, model checking, and concurrency-aware testing to validate and verify security and safety properties of both the specification and a prototype implementation of the RMM. Crucially, our verification efforts were, and are still being, developed and refined contemporaneously with active development of both specification and implementation, and have been adopted by Arm's product teams.

We describe our major achievements, realized through the application of formal techniques, as well as challenges that remain for future work. We believe that the work reported in this paper is the most thorough application of formal techniques to the design and implementation of any current commercially-viable Confidential Computing implementation, setting a new high-water mark for work in this area.

References

[1]

Martín Abadi and Leslie Lamport. 1991. The Existence of Refinement Mappings. Theor. Comput. Sci., 82, 2 (1991), 253–284. https://doi.org/10.1016/0304-3975(91)90224-P

Digital Library

[2]

Amazon Inc. Last viewed June 2022. AWS CBMC viewer. https://github.com/model-checking/cbmc-viewer

[3]

Arm Ltd. 2008. ARM Security Technology. Building a Secure System using TrustZone Technology. https://documentation-service.arm.com/static/5f212796500e883ab8e74531

[4]

Arm Ltd. 2021. Arm Confidential Compute Architecture. https://www.arm.com/architecture/security-features/arm-confidential-compute-architecture

[5]

Arm Ltd. 2022. Realm Management Monitor beta0 specification. https://developer.arm.com/documentation/den0137/a/ Accessed 25^ th October 2022, final version to be published 2022

[6]

Arm Ltd. Last viewed June 2022. Arm Architecture Reference Manual for A-profile architecture. https://developer.arm.com/documentation/ddi0487/latest

[7]

Arm Ltd. Last viewed June 2022. Introducing Iris, the new generation of debug and trace interface in Arm Models. https://community.arm.com/arm-community-blogs/b/tools-software-ides-blog/posts/iris-the-new-debug-and-trace-interface-in-arm-models

[8]

William R. Bevier. 1989. Kit: A Study in Operating System Verification. IEEE Trans. Software Eng., 15, 11 (1989), 1382–1396. https://doi.org/10.1109/32.41331

Digital Library

[9]

Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, and Frédéric Loulergue. 2015. A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C. In Formal Methods for Industrial Critical Systems - 20th International Workshop, FMICS 2015, Oslo, Norway, June 22-23, 2015 Proceedings, Manuel Núñez and Matthias Güdemann (Eds.) (Lecture Notes in Computer Science, Vol. 9128). Springer, 15–30. https://doi.org/10.1007/978-3-319-19458-5_2

[10]

Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. 2018. A Lesson on Verification of IoT Software with Frama-C. In 2018 International Conference on High Performance Computing & Simulation, HPCS 2018, Orleans, France, July 16-20, 2018. IEEE, 21–30. https://doi.org/10.1109/HPCS.2018.00018

[11]

Bruno Blanchet. 2013. Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif. In Foundations of Security Analysis and Design VII - FOSAD 2012/2013 Tutorial Lectures, Alessandro Aldini, Javier López, and Fabio Martinelli (Eds.) (Lecture Notes in Computer Science, Vol. 8604). Springer, 54–87. isbn:978-3-319-10081-4 https://doi.org/10.1007/978-3-319-10082-1_3

[12]

Hao Chen, Xiongnan (Newman) Wu, Zhong Shao, Joshua Lockerman, and Ronghui Gu. 2018. Toward Compositional Verification of Interruptible OS Kernels and Device Drivers. J. Autom. Reason., 61, 1-4 (2018), 141–189. https://doi.org/10.1007/s10817-017-9446-0

Digital Library

[13]

Nathan Chong and Bart Jacobs. 2021. Formally Verifying the FreeRTOS IPC Mechanism. In Embedded World Conference. 202–211. https://www.amazon.science/publications/formally-verifying-freertos-interprocess-communication-mechanism

[14]

Koen Claessen and John Hughes. 2000. QuickCheck: a lightweight tool for random testing of Haskell programs. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP ’00), Montreal, Canada, September 18-21, 2000, Martin Odersky and Philip Wadler (Eds.). ACM, 268–279. https://doi.org/10.1145/351240.351266

Digital Library

[15]

George Coker, Joshua D. Guttman, Peter A. Loscocco, Amy L. Herzog, Jonathan K. Millen, Brian O’Hanlon, John D. Ramsdell, Ariel Segall, Justin Sheehy, and Brian T. Sniffen. 2011. Principles of remote attestation. Int. J. Inf. Sec., 10, 2 (2011), 63–81. https://doi.org/10.1007/s10207-011-0124-7

Digital Library

[16]

Byron Cook, Björn Döbel, Daniel Kroening, Norbert Manthey, Martin Pohlack, Elizabeth Polgreen, Michael Tautschnig, and Pawel Wieczorkiewicz. 2020. Using model checking tools to triage the severity of security bugs in the Xen hypervisor. In 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020. IEEE, 185–193. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_26

[17]

Mads Dam, Roberto Guanciale, Narges Khakpour, Hamed Nemati, and Oliver Schwarz. 2013. Formal verification of information flow security for a simple arm-based separation kernel. In 2013 ACM SIGSAC Conference on Computer and Communications Security, CCS’13, Berlin, Germany, November 4-8, 2013, Ahmad-Reza Sadeghi, Virgil D. Gligor, and Moti Yung (Eds.). ACM, 223–234. https://doi.org/10.1145/2508859.2516702

Digital Library

[18]

Mads Dam, Roberto Guanciale, and Hamed Nemati. 2013. Machine code verification of a tiny ARM hypervisor. In TrustED’13, Proceedings of the 2013 ACM Workshop on Trustworthy Embedded Devices, Co-located with CCS 2013, November 4, 2013, Berlin, Germany, Ahmad-Reza Sadeghi, Frederik Armknecht, and Jean-Pierre Seifert (Eds.). ACM, 3–12. https://doi.org/10.1145/2517300.2517302

Digital Library

[19]

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, Shanghai, China, October 28-31, 2017. ACM, 287–305. https://doi.org/10.1145/3132747.3132782

Digital Library

[20]

Joseph A. Goguen and José Meseguer. 1982. Security Policies and Security Models. In 1982 IEEE Symposium on Security and Privacy, Oakland, CA, USA, April 26-28, 1982. IEEE Computer Society, 11–20. https://doi.org/10.1109/SP.1982.10014

[21]

Liang Gu, Alexander Vaynberg, Bryan Ford, Zhong Shao, and David Costanzo. 2011. CertiKOS: a certified kernel for secure cloud computing. In APSys ’11 Asia Pacific Workshop on Systems, Shanghai, China, July 11-12, 2011, Haibo Chen, Zheng Zhang, Sue Moon, and Yuanyuan Zhou (Eds.). ACM, 3. https://doi.org/10.1145/2103799.2103803

Digital Library

[22]

Ronghui Gu, Zhong Shao, Hao Chen, Jieung Kim, Jérémie Koenig, Xiongnan (Newman) Wu, Vilhelm Sjöberg, and David Costanzo. 2019. Building certified concurrent OS kernels. Commun. ACM, 62, 10 (2019), 89–99. https://doi.org/10.1145/3356903

Digital Library

[23]

Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016, Kimberly Keeton and Timothy Roscoe (Eds.). USENIX Association, 653–669. https://www.usenix.org/conference/osdi16/technical-sessions/presentation/gu

Digital Library

[24]

Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, and Tahina Ramananandro. 2018. Certified concurrent abstraction layers. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018. 646–661. https://doi.org/10.1145/3192366.3192381

Digital Library

[25]

Inzemamul Haque, Deepak D’Souza, Habeeb P, Arnab Kundu, and Ganesh Babu. 2020. Verification of a Generative Separation Kernel. In Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, Dang Van Hung and Oleg Sokolsky (Eds.) (Lecture Notes in Computer Science, Vol. 12302). Springer, 305–322. https://doi.org/10.1007/978-3-030-59152-6_17

Digital Library

[26]

Cliff B. Jones. 1983. Tentative Steps Toward a Development Method for Interfering Programs. ACM Trans. Program. Lang. Syst., 5, 4 (1983), 596–619. https://doi.org/10.1145/69575.69577

Digital Library

[27]

Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2010. seL4: formal verification of an operating-system kernel. Commun. ACM, 53, 6 (2010), 107–115. https://doi.org/10.1145/1743546.1743574

Digital Library

[28]

Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: formal verification of an OS kernel. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, SOSP 2009, Big Sky, Montana, USA, October 11-14, 2009, Jeanna Neefe Matthews and Thomas E. Anderson (Eds.). ACM, 207–220. https://doi.org/10.1145/1629575.1629596

Digital Library

[29]

Bernhard Kragl and Shaz Qadeer. 2021. The Civl Verifier. In Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, October 19-22, 2021. IEEE, 143–152. isbn:978-3-85448-046-4 https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23

[30]

Daniel Kroening and Michael Tautschnig. 2014. CBMC – C Bounded Model Checker. In Tools and Algorithms for the Construction and Analysis of Systems, Erika Ábrahám and Klaus Havelund (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 389–391. https://doi.org/10.1007/978-3-642-54862-8_26

[31]

Dirk Leinenbach and Thomas Santen. 2009. Verifying the Microsoft Hyper-V Hypervisor with VCC. In FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings, Ana Cavalcanti and Dennis Dams (Eds.) (Lecture Notes in Computer Science, Vol. 5850). Springer, 806–809. https://doi.org/10.1007/978-3-642-05089-3_51

Digital Library

[32]

K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers, Edmund M. Clarke and Andrei Voronkov (Eds.) (Lecture Notes in Computer Science, Vol. 6355). Springer, 348–370. https://doi.org/10.1007/978-3-642-17511-4_20

[33]

Rebekah Leslie-Hurd, Dror Caspi, and Matthew Fernandez. 2015. Verifying Linearizability of Intel® Software Guard Extensions. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II, Daniel Kroening and Corina S. Pasareanu (Eds.) (Lecture Notes in Computer Science, Vol. 9207). Springer, 144–160. https://doi.org/10.1007/978-3-319-21668-3_9

[34]

Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, and John Zhuang Hui. 2021. Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor. In 30th USENIX Security Symposium, USENIX Security 2021, August 11-13, 2021, Michael Bailey and Rachel Greenstadt (Eds.). USENIX Association, 3953–3970. https://www.usenix.org/conference/usenixsecurity21/presentation/li-shih-wei

[35]

Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, and John Zhuang Hui. 2021. A Secure and Formally Verified Linux KVM Hypervisor. In 42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24-27 May 2021. IEEE, 1782–1799. https://doi.org/10.1109/SP40001.2021.00049

[36]

Xupeng Li, Xuheng Li, Christoffer Dall, Ronghui Gu, Jason Nieh, Yousuf Sait, and Gareth Stockwell. 2022. Design and Verification of the Arm Confidential Compute Architecture. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22). USENIX Association, Carlsbad, CA. 465–484. isbn:978-1-939133-28-1 https://www.usenix.org/conference/osdi22/presentation/li

[37]

Linaro Ltd. 2022. The Open Portable Trusted Execution Environment (OP-TEE). https://www.op-tee.org Accessed 23^ rd June 2022

[38]

Linaro Ltd. 2022. TrustedFirmware-A. https://www.trustedfirmware.org/projects/tf-a/

[39]

Frédéric Mangano, Simon Duquennoy, and Nikolai Kosmatov. 2016. Formal Verification of a Memory Allocation Module of Contiki with Frama-C: A Case Study. In Risks and Security of Internet and Systems - 11th International Conference, CRiSIS 2016, Roscoff, France, September 5-7, 2016, Revised Selected Papers, Frédéric Cuppens, Nora Cuppens, Jean-Louis Lanet, and Axel Legay (Eds.) (Lecture Notes in Computer Science, Vol. 10158). Springer, 114–120. https://doi.org/10.1007/978-3-319-54876-0_9

[40]

Michael McCoyd, Robert Bellarmine Krug, Deepak Goel, Mike Dahlin, and William D. Young. 2013. Building a Hypervisor on a Formally Verifiable Protection Layer. In 46th Hawaii International Conference on System Sciences, HICSS 2013, Wailea, HI, USA, January 7-10, 2013. IEEE Computer Society, 5069–5078. https://doi.org/10.1109/HICSS.2013.121

Digital Library

[41]

Simon Meier, Benedikt Schmidt, Cas Cremers, and David A. Basin. 2013. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, Natasha Sharygina and Helmut Veith (Eds.) (Lecture Notes in Computer Science, Vol. 8044). Springer, 696–701. isbn:978-3-642-39798-1 https://doi.org/10.1007/978-3-642-39799-8_48

[42]

Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang. 2019. Scaling symbolic evaluation for automated verification of systems code with Serval. In Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP 2019, Huntsville, ON, Canada, October 27-30, 2019, Tim Brecht and Carey Williamson (Eds.). ACM, 225–242. https://doi.org/10.1145/3341301.3359641

Digital Library

[43]

Hamed Nemati, Roberto Guanciale, and Mads Dam. 2015. Trustworthy Virtualization of the ARMv7 Memory Subsystem. In SOFSEM 2015: Theory and Practice of Computer Science - 41st International Conference on Current Trends in Theory and Practice of Computer Science, Pec pod Sněžkou, Czech Republic, January 24-29, 2015. Proceedings, Giuseppe F. Italiano, Tiziana Margaria-Steffen, Jaroslav Pokorný, Jean-Jacques Quisquater, and Roger Wattenhofer (Eds.) (Lecture Notes in Computer Science, Vol. 8939). Springer, 578–589. https://doi.org/10.1007/978-3-662-46078-8_48

Digital Library

[44]

Gábor Pék, Levente Buttyán, and Boldizsár Bencsáth. 2013. A survey of security issues in hardware virtualization. ACM Comput. Surv., 45, 3 (2013), 40:1–40:34. https://doi.org/10.1145/2480741.2480757

Digital Library

[45]

Alastair Reid. 2016. Trustworthy specifications of ARM® v8-A and v8-M system level architecture. In 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, October 3-6, 2016, Ruzica Piskac and Muralidhar Talupur (Eds.). IEEE, 161–168. https://doi.org/10.1109/FMCAD.2016.7886675

[46]

Alastair Reid, Rick Chen, Anastasios Deligiannis, David Gilday, David Hoyes, Will Keen, Ashan Pathirane, Owen Shepherd, Peter Vrabel, and Ali Zaidi. 2016. End-to-End Verification of Processors with ISA-Formal. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, Swarat Chaudhuri and Azadeh Farzan (Eds.) (Lecture Notes in Computer Science, Vol. 9780). Springer, 42–58. https://doi.org/10.1007/978-3-319-41540-6_3

[47]

Muhammad Usama Sardar, Rasha Faqeh, and Christof Fetzer. 2020. Formal Foundations for Intel SGX Data Center Attestation Primitives. In Formal Methods and Software Engineering - 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1-3, 2021, Proceedings, Shang-Wei Lin, Zhe Hou, and Brendan P. Mahony (Eds.) (Lecture Notes in Computer Science, Vol. 12531). Springer, 268–283. https://doi.org/10.1007/978-3-030-63406-3_16

Digital Library

[48]

Muhammad Usama Sardar, Saidgani Musaev, and Christof Fetzer. 2021. Demystifying Attestation in Intel Trust Domain Extensions via Formal Verification. IEEE Access, 9 (2021), 83067–83079. https://doi.org/10.1109/ACCESS.2021.3087421

[49]

Muhammad Usama Sardar, Do Le Quoc, and Christof Fetzer. 2020. Towards Formalization of Enhanced Privacy ID (EPID)-based Remote Attestation in Intel SGX. In 23rd Euromicro Conference on Digital System Design, DSD 2020, Kranj, Slovenia, August 26-28, 2020. IEEE, 604–607. https://doi.org/10.1109/DSD51259.2020.00099

[50]

Thomas Sewell, Simon Winwood, Peter Gammie, Toby C. Murray, June Andronick, and Gerwin Klein. 2011. seL4 Enforces Integrity. In Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings, Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk (Eds.) (Lecture Notes in Computer Science, Vol. 6898). Springer, 325–340. https://doi.org/10.1007/978-3-642-22863-6_24

[51]

Runzhou Tao, Jianan Yao, Xupeng Li, Shih-Wei Li, Jason Nieh, and Ronghui Gu. 2021. Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware. In SOSP ’21: ACM SIGOPS 28th Symposium on Operating Systems Principles, Virtual Event / Koblenz, Germany, October 26-29, 2021, Robbert van Renesse and Nickolai Zeldovich (Eds.). ACM, 866–881. https://doi.org/10.1145/3477132.3483560

Digital Library

[52]

Viktor Vafeiadis and Matthew J. Parkinson. 2007. A Marriage of Rely/Guarantee and Separation Logic. In CONCUR 2007 - Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings, Luís Caires and Vasco Thudichum Vasconcelos (Eds.) (Lecture Notes in Computer Science, Vol. 4703). Springer, 256–271. isbn:978-3-540-74406-1 https://doi.org/10.1007/978-3-540-74407-8_18

Cited By

Broy MBrucker AFantechi AGleirscher MHavelund KKuppe MMendes APlatzer ARingert JSullivan A(2024)Does Every Computer Scientist Need to Know Formal Methods?Formal Aspects of Computing10.1145/3670795Online publication date: 10-Jun-2024
https://dl.acm.org/doi/10.1145/3670795
Schulze MLindenmeier CRöckl J(2024)BarriCCAde: Isolating Closed-Source Drivers with ARM CCA2024 IEEE European Symposium on Security and Privacy Workshops (EuroS&PW)10.1109/EuroSPW61312.2024.00033(245-251)Online publication date: 8-Jul-2024
https://doi.org/10.1109/EuroSPW61312.2024.00033
Sardar MFossati TFrost SXiong S(2024)Formal Specification and Verification of Architecturally-Defined Attestation Mechanisms in Arm CCA and Intel TDXIEEE Access10.1109/ACCESS.2023.334650112(361-381)Online publication date: 2024
https://doi.org/10.1109/ACCESS.2023.3346501

Index Terms

A Verification Methodology for the Arm® Confidential Computing Architecture: From a Secure Specification to Safe Implementations
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Dynamic analysis
        Model checking
        Software verification

Recommendations

A logical verification methodology for service-oriented computing

We introduce a logical verification methodology for checking behavioral properties of service-oriented computing systems. Service properties are described by means of SocL, a branching-time temporal logic that we have specifically designed for ...
Q: A Sound Verification Framework for Statecharts and Their Implementations
FTSCS 2022: Proceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems

We present Q Framework: a verification framework used at Sandia National Laboratories. Q is a collection of tools used to verify safety and correctness properties of high-consequence embedded systems and captures the structure and compositionality of ...
Formal specification and verification of data separation in a separation kernel for an embedded system
CCS '06: Proceedings of the 13th ACM conference on Computer and communications security

Although many algorithms, hardware designs, and security protocols have been formally verified, formal verification of the security of software is still rare. This is due in large part to the large size of software, which results in huge costs for ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 7, Issue OOPSLA1

April 2023

901 pages

EISSN:2475-1421

DOI:10.1145/3554309

Editor:
Michael Hicks
Amazon, USA

Issue’s Table of Contents

Copyright © 2023 Owner/Author.

This work is licensed under a Creative Commons Attribution 4.0 International License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 06 April 2023

Published in PACMPL Volume 7, Issue OOPSLA1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Artifacts Evaluated & Reusable / v1.1

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
1,714
Total Downloads

Downloads (Last 12 months)1,127
Downloads (Last 6 weeks)91

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Broy MBrucker AFantechi AGleirscher MHavelund KKuppe MMendes APlatzer ARingert JSullivan A(2024)Does Every Computer Scientist Need to Know Formal Methods?Formal Aspects of Computing10.1145/3670795Online publication date: 10-Jun-2024
https://dl.acm.org/doi/10.1145/3670795
Schulze MLindenmeier CRöckl J(2024)BarriCCAde: Isolating Closed-Source Drivers with ARM CCA2024 IEEE European Symposium on Security and Privacy Workshops (EuroS&PW)10.1109/EuroSPW61312.2024.00033(245-251)Online publication date: 8-Jul-2024
https://doi.org/10.1109/EuroSPW61312.2024.00033
Sardar MFossati TFrost SXiong S(2024)Formal Specification and Verification of Architecturally-Defined Attestation Mechanisms in Arm CCA and Intel TDXIEEE Access10.1109/ACCESS.2023.334650112(361-381)Online publication date: 2024
https://doi.org/10.1109/ACCESS.2023.3346501
Beyer DLee N(2024)The Transformation Game: Joining Forces for VerificationPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75778-5_9(175-205)Online publication date: 18-Nov-2024
https://doi.org/10.1007/978-3-031-75778-5_9

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents