Verifying Components of Arm® Confidential Computing Architecture with ESBMC
Abstract elided by the publisher.
Related papers
- A Verification Methodology for the Arm® Confidential Computing Architecture: From a Secure Specification to Safe Implementations OOPSLA 2023
- ESBMC v6.0: Verifying C Programs Using k-Induction and Invariant Inference - (Competition Contribution) TACAS 2019
- Who guards the guards? formal validation of the Arm v8-m architecture specification OOPSLA 2017
- A verified information-flow architecture POPL 2014
- Verified Security for the Morello Capability-enhanced Prototype Arm Architecture ESOP 2022
- An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic POPL 2024
- Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware Architecture PLDI 2025
- First Steps towards the Certification of an ARM Simulator Using Compcert CPP 2011