Towards a Formally Verified Security Monitor for VM-based Confidential Computing

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

The paper defines a processor-independent confidential-computing architecture, implements a RISC-V security monitor in Rust, and gives a proof outline for its memory tracker. Its proposed method links natural-language security goals to a mathematical model, Rust implementation, and machine-checkable Coq proof (Figure 2, p. 74). The paper provides “a proof outline of a security property of an internal component” (section 8, p. 81), not a finished Coq proof; the hardware, the monitor as a whole, and the end system are not proved.

abstraction from guarantees to proof

Start with a high-level guarantee, threat model, architecture, operational behavior, and implementation. The authors explain that “This methodology requires the expression of all system properties and software implementation in Coq” (section 2, p. 74). Define the architecture at several abstraction levels, progressively specializing until the model and implementation are mathematical expressions; prove that implementation behavior conforms to the model and preserves its invariants (section 2, p. 74). Inference: a Verus workflow should make the security state and transitions explicit in Rust/spec functions, state the invariant as invariant clauses and ensures, and prove refinement from each implementation operation to the model. The paper’s Coq and RefinedRust translation are not Verus syntax.

The trusted base is explicit. The authors “rely on correctness of formal verification tooling” (section 2, p. 74) and trust the formalization of Rust (λRust), the Coq kernel checker, and translation from the Rust intermediate representation to machine code (section 2, pp. 74–75). Hardware is omitted from functional verification and assumed to satisfy axioms; hardware design and implementation “must be performed separately” (section 2, p. 75). Skilled auditors must assess whether the natural-language architecture and model formalization are sound because the high-level specification itself cannot be formally verified (section 2, p. 74).

canonical architecture and threat model

The architecture has seven required hardware functions: interrupt control, immutable boot code, endorsement seed, atomic instruction, physical memory isolation, privilege separation, and random-number generation (Figure 3, p. 75). The monitor runs at the highest privilege, routes calls, transforms state, and reconfigures hardware. It partitions memory into monitor, control-data, confidential-VM, and uninitialized confidential regions (section 3, p. 75).

The software attacker controls the hypervisor, OS, user-space software, ordinary VMs, and some confidential VMs, and may start, stop, interrupt, or feed arbitrary input to the victim VM. The stated goals are to read victim data, force victim processing, alter execution flow, or impersonate the victim (section 3.1, p. 76). The architecture excludes denial of service and physical attacks on processor, memory, or buses; it “can be extended” with cryptographic protection of data leaving the processor against the physical vector (section 3.1, p. 76). Inference: a Verus product threat analysis must carry these exclusions as explicit assumptions and reject a proof claim that silently broadens the threat model.

initialization and finite-state invariants

Formalize hardware properties as axioms. The paper lists, for example, that highest privilege alone may reconfigure security-critical hardware, boot code is immutable, memory isolation denies access to confidential addresses, and microarchitectural state can be cleared (section 4.1, p. 76). Define initialization invariants: the monitor executes exclusively at highest privilege; confidential memory is accessible only from confidential code; non-confidential code cannot access it; designated interrupts enter the monitor; and endorsement-seed access is protected (section 4.2, p. 77). The paper says these invariants “guarantee 𝑆.𝐼𝑛𝑖𝑡 .1 and 𝑆.𝐼𝑛𝑖𝑡 .2” (section 4.2, p. 77).

Model runtime as a finite-state machine (Figure 4, p. 77) with a non-confidential part and a confidential part; the monitor exits to the hypervisor only from the NC-exit node and to the CVM only from the C-exit node (section 4.3, p. 77). Transitions between the two security domains “must apply state sanitization and protection mechanisms” (section 4.3, p. 77), such as memory-isolation reconfiguration and saving or restoring processor state and interrupt delivery configuration. The FSM maintains invariants I.FSM.1 to I.FSM.6, including disabled interrupts while the monitor runs, correct memory permissions on C-to-NC and NC-to-C transitions, saved state in confidential control data, and non-disclosure of one domain’s architectural state (section 4.2, pp. 77–78). Inference: in Verus, represent the FSM state as a datatype or enum, use a transition function with requires describing the source state and ensures describing the destination and preserved security predicate, and prove each transition separately.

memory tracker and ownership proof

The implementation’s proof example is a memory tracker that assigns page tokens. Its three invariants are: “The fixed set of Page tokens is created only by the initialization function”; initialization creates one token per aligned physical page and every pair defines disjoint regions; and a read or write requires owning the associated token (section 6.2, p. 80). These invariants establish security guarantee S.MT.1: two disjoint security domains, such as two confidential VMs, cannot own the same physical memory region (section 6, p. 78). The Rust listings in the paper are described as “conceptual” (section 6.1, p. 79).

Apply the proof in three steps. First, show the init() constructor is the only monitor code creating Page values and is referenced only from the initialization function called by the boot firmware; the authors say “One could show this with a simple grep tool or using Rust’s scopes that limit visibility of the function within the SM, like pub(super)” (section 6.3, p. 80). Second, prove the constructor’s functional correctness: it creates one token per page and no overlapping regions. The paper says this requires translating the code into a formalized Rust representation such as λRust and proving it with Coq (section 6.3, p. 80). Third, the contradiction argument for S.MT.1 (section 6.3, p. 80): assume two page tables define the same physical address in different security domains; then either both use the same Page token, which is false because of Rust ownership, memory safety, and I.MT.3, or two different tokens describe overlapping addresses, which is false because of I.MT.1 and I.MT.2. The paper adds that proving I.MT.3 “requires more complete Rust representation that covers unsafe Rust”, provided by RefinedRust (section 6.3, p. 80).

Inference: a Verus implementation would encode token ownership in Rust types and ghost state, specify constructor postconditions for token count and disjointness, and use assert/assert forall proofs or lemmas to derive contradiction. The paper does not provide Verus code, so exact ghost representation and solver strategy are design choices. The unchanged principle is to prove both constructor correctness and preservation of the three invariants at every operation.

evidence and limitations

The paper implements initialization and transformations for VM-to-CVM conversion, CVM resume and termination, page sharing, a limited number of hypercalls, and VirtIO via MMIO load/store requests, in open-source Rust targeting RISC-V (section 5, p. 78). It presents a proof direction for one internal component, not measured proof coverage or a complete machine-checked monitor. The conclusion says future work will focus on formal modelling of all components, proving them using Coq, and refining the canonical architecture for RISC-V (section 8, pp. 80–81). Inference: no denominator of fully verified monitor functions is reported. The evidence is architectural axioms, explicit invariants, Rust ownership reasoning, and a proof outline for the memory tracker.

Trusted or assumed elements include hardware axioms, secure boot (A.HW.2), the formalization of Rust, translation of the Rust intermediate representation to machine code, Coq kernel correctness, and auditor judgment about the high-level specification. Inference: agent-written verified Rust is a high product threat for confidential computing because omitted hardware assumptions or an incomplete threat model can make a locally proved invariant irrelevant to isolation. Inference: the paper offers a pattern to reuse (architecture, model, Rust, Coq as a planned chain, token-based memory isolation, and a contradiction argument), but it has not completed that chain, so VL should reuse the patterns without citing them as a finished proof.

techniques for the catalog

• abstraction-linked verification — connect high-level guarantees, formal model, Rust implementation, and machine-checkable proof through explicit refinement obligations
• axiomatized hardware boundary — state required hardware properties as axioms while clearly identifying hardware and translation components outside the proof
• finite-state security invariants — model privilege and domain transitions as an FSM and preserve memory, interrupt, saved-state, and non-disclosure invariants across the monitor’s enter, exit, and domain-crossing transitions
• ownership-backed page isolation — represent each physical page with a unique token, prove token creation and disjointness, and require token ownership for access
• contradiction proof of non-overlap — assume two page tables share an address and eliminate same-token and overlapping-distinct-token cases using ownership and invariants Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Initially the security monitor provides the full-isolation of the confidential workload, preventing any form of communication with other security domains.”): I read the whole paper text and checked every quotation, section and page reference, the axiom, invariant and FSM descriptions, the memory-tracker invariants and three proof steps, the implementation scope, and the conclusion; I changed the link to the DOI printed in the paper (10.1145/3623652.3623668), corrected pages (section 5 is p. 78, hardware “must be performed separately” is p. 75), replaced unsupported claims (an ordered transition list, a “complete chain” shown, a compiler among the trusted items, DoS needing an extension, the claim that every edge preserves the invariants, a claim about different confidential VMs sharing a physical page) with the paper’s wording, and marked the denominator point as inference; I did not check the Verus inferences against any Verus documentation, the cited related work, or the open-source code, and I did not read figures beyond their text.

Last edited: 2026-10-17