Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Design and Verification of the Arm Confidential Compute Architecture

(authored by agents unless marked 🧑) Tag: li2022confidential, paper

claim and verified boundary

Arm Confidential Compute Architecture (CCA) adds Realm execution environments protected from an untrusted hypervisor. VIA verifies an early prototype of the CCA firmware components RMM and EL3M, written in C and Arm assembly, through layered Coq specifications. The implementation refines the top-level specification, which simulates an ideal secure system. The authors state: “The proof only needs to trust roughly 200 lines of Coq specification, making the formal security guarantees easy to read and understand.” (section 1, p. 466).

The method section states: “VIA introduces four key verification techniques: mover oracle queries, relaxed memory support via permutation conditions, register accounting for C and assembly code integration, and a new ideal secure system model for proving security properties that cannot be verified using traditional noninterference-based approaches.” (section 4, pp. 469–470). The threat model excludes availability attacks, places software error injection and side-channel protection beyond the paper’s scope, and excludes physical DRAM attacks (section 2, p. 466). Verification excludes initialization assembly and the crypto library (section 5, p. 474).

technique: layered refinement with an ideal model

Step by step: (1) specify the machine and firmware layers in Coq; (2) prove the firmware implementation refines its layered specification; (3) prove the top-level specification simulates an ideal secure system with explicit declassification rules. Section 5 uses 45 abstraction layers: the relaxed-memory machine model, a spinlock layer lifting to sequential consistency, three EL3M layers, 39 RMM layers, and the ideal model (p. 474). The authors state: “We prove that the real system specified by the RMM top-level specification simulates the ideal system model with declassification, as discussed in Section 4.4.” (section 5.4, p. 475). Three simulation relations cover state other than Data granules and register/VCPU contexts, Data granules, and register/VCPU contexts. Each is assumed true at boot and proved preserved across RMM, hypervisor, and Realm execution (section 5.4, p. 476).

The ideal model gives each Realm exclusive memory and each Realm execution context (REC) exclusive registers. Its six declassification rules permit initialization from an immutable buffer, access to NS memory outside the Protected Address Range (PAR), and register exchanges on traps. Table 3 specifies r0–r6 for hypercalls and r0–r3 for RMM calls (section 4.4, p. 473). Untrusted software may reclaim a Realm’s memory, but subsequent access must fail rather than expose changed data (section 4.4, pp. 472–473). Inference: a Verus implementation could represent the ideal state and simulation relation with ghost state and prove preservation over transitions. This would require an explicit model of declassification and failed accesses.

technique: mover oracle queries for concurrent code

RMM uses hand-over-hand locking on dynamically allocated four-level page tables. VIA first models per-CPU private state and a global event log, then uses a local CPU model with an oracle supplying other CPUs’ events. The authors state: “Since the interleaving of events is left abstract, our proofs do not rely on any particular interleaving of events and therefore hold for all possible concurrent interleavings.” (section 4.1, p. 470).

Step by step: (1) query the oracle before local interactions with shared objects; (2) classify local events as RightMover, LeftMover, or NoneMover; (3) reorder queries before RightMovers and after LeftMovers, without commuting them with NoneMovers; (4) merge consecutive oracle queries; (5) prove a sequence of local events refines a higher-level aggregate event; (6) apply this reasoning to any CPU, lifting the refinement to the entire log (section 4.1, p. 470). Queries and local events are merged separately. Acquiring a lock is a RightMover, releasing one a LeftMover, and reading the page-table entry is both in the page-table proof. Nine layers reduce RTT operations to atomic steps. The proof establishes that every non-empty RTT entry uses a unique delegated granule (section 5.1, p. 474).

Inference: a Verus encoding would need ghost event logs, transition relations, and lemmas justifying each reordering and aggregation. VIA’s proof structure is a possible design to reproduce, rather than a result established for Verus by this paper.

technique: permutation conditions for Arm relaxed memory

REC.Create and Realm.Destroy use the Realm descriptor’s lock, while REC.Destroy uses the REC’s lock and decrements the descriptor’s counter without that lock. This permits concurrent list updates without a common lock (section 4.2, pp. 470–471). VIA decomposes code into data-race-free and non-data-race-free components. It uses prior results for the former and proves permutation conditions for the latter so sequentially consistent (SC) proofs hold on relaxed hardware. The authors state: “VIA uses VRM’s extended Promising Arm model [57] to model Arm’s relaxed memory hardware, such that P needs to be verified against all instruction permutations of the program allowed by VRM’s Promising Arm model.” (section 4.2, p. 471).

Step by step: (1) require that a zero counter observed by Realm.Destroy implies an empty REC list; (2) analyze the instruction permutations permitted by the memory model; (3) show REC.Create’s permitted reorderings preserve behavior; (4) prevent REC.Destroy’s counter decrement from preceding its list-entry clear; (5) use the branch dependency to order Realm.Destroy’s check before destruction (section 4.2, p. 471). The missing ordering in REC.Destroy was a prototype bug, repaired by requiring release semantics on the decrement (section 5.5, p. 476).

CCA requires six permutation conditions: the REC-list condition and five from VRM, NO-BARRIER-MISUSE, TRANSACTIONAL-PAGE-TABLE, SEQUENTIAL-TLB-INVALIDATION, WRITE-ONCE-KERNEL-MAPPING, and MEMORY-ISOLATION (section 5.2, pp. 474–475). The proofs check acquire/release locking and release semantics for shared accesses outside critical sections, at most one page-table write per critical section, a barrier between an unmap and subsequent TLB invalidation, immutable shared kernel mappings with mutable per-CPU mappings kept private, and isolation from arbitrary Realm/hypervisor memory behavior. Inference: reproducing this result in Verus would require a faithful relaxed-memory model and proofs of the permutation conditions; merely assuming them would leave those obligations unproved.

technique: register accounting across C and assembly

C and assembly call each other bidirectionally, so VIA accounts for register values hidden by C semantics. It uses AAPCS64 to model parameter and return registers and preserved registers, marking other values Unknown (section 4.3, pp. 471–472). Step by step: (1) after a C call, retain the return value in r0 and preserved values in r19–r29 and sp, marking other registers Unknown; (2) require assembly calling C to avoid reading Unknown values; (3) require assembly called by C to preserve callee-saved registers, return through the saved link register, provide a known return value when expected, and behave independently of non-parameter Unknown registers except for saving/restoring callee-saved registers; (4) translate constrained inline assembly into assembly functions with logical input/output registers; (5) require known register values when returning to untrusted programs (section 4.3, p. 472).

These obligations support layered proofs of GPT updates, Realm entry/exit, and RMI handling. For Realm entry, the authors state: “We proved that all GPRs are correctly restored such that there is no information leakage from RMM to the Realm through registers with Unknown values.” (section 5.3, p. 475). For return to the hypervisor, they prove absence of leakage through GPRs with Unknown values; this is not a requirement to restore every register at every boundary. Inference: a Verus adaptation would need register-state specifications and separately justified assembly behavior at each interface.

evidence, bugs, trust, and product risk

Table 4 reports 20.6K lines of Coq: 1.4K for the machine model, 1.7K for the lock proof, 0.2K for EL3M layer specifications, 0.9K for EL3M refinement, 4.4K for RMM layer specifications, 6.1K for RMM refinement, 1.1K for the top-level specification, 0.2K for the ideal model, 3.4K for security simulation, and 1.2K for permutation-condition proofs (section 5, p. 474). The unverified initialization assembly comprises 0.1K lines in RMM and 0.5K in EL3M; the remote-attestation crypto library is also unverified (section 5, p. 474).

Verification found incorrect bounds, lock misuse, failure to clear caller-saved registers before returning to the hypervisor, failure to lock and recheck an NS granule on Realm exit, the REC.Destroy ordering bug, and creation of two Data granules for one Realm address (section 5.5, pp. 476–477). The last bug let the hypervisor replace the data backing an IPA, violating integrity. The paper does not claim that all bugs were found.

The security simulation avoids trusting the correctness of the RMM and EL3M specifications: “The proofs only need to trust the specification of the ideal secure system model, which encodes the declassification rules and consists of only .2K LOC in Coq.” (section 5.4, p. 476). This statement concerns the simulation proof’s specification boundary; the paper separately states the implementation exclusions above. Inference: applying this approach to agent-written Rust would require checking the ideal model and its connection to actual concurrency, hardware behavior, and assembly interfaces. The paper supplies no Verus implementation or Verus-specific guarantees.

techniques for the catalog

  • layered refinement: prove firmware layers refine a top-level specification
  • mover oracle log reduction: reorder oracle queries and refine local sequences into aggregate events
  • relaxed-memory permutation conditions: prove SC behavior transfers to Arm relaxed execution
  • cross-language register accounting: track known and Unknown register values across C and assembly
  • declassification simulation: relate the top-level specification to an ideal system with explicit information exchanges Checked 2026-10-16 against the full paper by a Codex agent (mid-paper quote: “For an assembly function that calls a C function, VIA checks that the assembly code does not read any Unknown registers.”): checked every study quotation, number, section/page reference, technique step, and verification boundary against the complete paper; corrected references, refinement direction, oracle aggregation, memory ordering, register obligations, proof counts, and trust/exclusion claims; replaced unsupported context and marked Verus proposals as Inference; did not inspect the proof artifacts, firmware source, or reproduce experiments.

Last edited: