Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verifying components of Arm(R) Confidential Computing Architecture with ESBMC

Tong Wu, Shale Xiong, Edoardo Manino, Gareth Stockwell, Lucas C. Cordeiro

TL;DR

This paper addresses the verification of Arm Confidential Computing Architecture's Realm Management Monitor (RMM) by applying ESBMC, an SMT-based software model checker, to supplement existing CBMC verification. It demonstrates ESBMC's ability to parse C source accurately, reproduce known failures, uncover 23 new RMM violations, and reveal inconsistencies with CBMC results, all while highlighting the impact of loop bound configuration and multi-property verification. The study shows that ESBMC can enhance real-world firmware verification but also exposes challenges in scalability and result readability, suggesting integration with industrial compilers and iterative improvements to ESBMC's algorithms. Overall, the work reinforces the value of diverse formal verification tools in industry-scale firmware verification and points to future work in speeding SMT solving for multi-property checks and detecting data races in multi-threaded contexts.

Abstract

Realm Management Monitor (RMM) is an essential firmware component within the recent Arm Confidential Computing Architecture (Arm CCA). Previous work applies formal techniques to verify the specification and prototype reference implementation of RMM. However, relying solely on a single verification tool may lead to the oversight of certain bugs or vulnerabilities. This paper discusses the application of ESBMC, a state-of-the-art Satisfiability Modulo Theories (SMT)-based software model checker, to further enhance RRM verification. We demonstrate ESBMC's ability to precisely parse the source code and identify specification failures within a reasonable time frame. Moreover, we propose potential improvements for ESBMC to enhance its efficiency for industry engineers. This work contributes to exploring the capabilities of formal verification techniques in real-world scenarios and suggests avenues for further improvements to better meet industrial verification needs.

Verifying components of Arm(R) Confidential Computing Architecture with ESBMC

TL;DR

This paper addresses the verification of Arm Confidential Computing Architecture's Realm Management Monitor (RMM) by applying ESBMC, an SMT-based software model checker, to supplement existing CBMC verification. It demonstrates ESBMC's ability to parse C source accurately, reproduce known failures, uncover 23 new RMM violations, and reveal inconsistencies with CBMC results, all while highlighting the impact of loop bound configuration and multi-property verification. The study shows that ESBMC can enhance real-world firmware verification but also exposes challenges in scalability and result readability, suggesting integration with industrial compilers and iterative improvements to ESBMC's algorithms. Overall, the work reinforces the value of diverse formal verification tools in industry-scale firmware verification and points to future work in speeding SMT solving for multi-property checks and detecting data races in multi-threaded contexts.

Abstract

Realm Management Monitor (RMM) is an essential firmware component within the recent Arm Confidential Computing Architecture (Arm CCA). Previous work applies formal techniques to verify the specification and prototype reference implementation of RMM. However, relying solely on a single verification tool may lead to the oversight of certain bugs or vulnerabilities. This paper discusses the application of ESBMC, a state-of-the-art Satisfiability Modulo Theories (SMT)-based software model checker, to further enhance RRM verification. We demonstrate ESBMC's ability to precisely parse the source code and identify specification failures within a reasonable time frame. Moreover, we propose potential improvements for ESBMC to enhance its efficiency for industry engineers. This work contributes to exploring the capabilities of formal verification techniques in real-world scenarios and suggests avenues for further improvements to better meet industrial verification needs.
Paper Structure (16 sections, 4 figures, 2 tables)

This paper contains 16 sections, 4 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Background
  3. Bounded Model Checking (BMC)
  4. Realm Management Monitor
  5. RMM Verification with ESBMC
  6. Bounded Verification
  7. Multi-Property Check
  8. Experiment Results
  9. Experimental Setup.
  10. Number of Violations Found.
  11. Confirmed and Unconfirmed Violations.
  12. Impact of step $k$ in incremental BMC.
  13. Performance Comparison.
  14. Syntax Errors.
  15. Conclusions
  16. ...and 1 more sections

Figures (4)

  • Figure 1: An architecture of an Arm CCA fox2023verification. The physical memory space is separated into four worlds: Non-secure, Secure, Root and the Realm.
  • Figure 2: RMI_GRANULE_DELEGATE command specification (draft) fox2023verification
  • Figure 3: Verification time for different k-steps during each loop rolling. The red node at the bottom left represents unrolling the loops completely until the given bounds.
  • Figure 4: Experiment result, where x-axis represents the RMM testcases, and y-axis represents the verification time in seconds. Different colors: blue on the left is for ESBMC single-property check, red on the middle is for CBMC multi-property check, and yellow on the right is for ESBMC multi-property check.