A Verified Confidential Computing as a Service Framework for Privacy Preservation

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

The paper defines Proof of Being Forgotten (PoBF) for confidential computing as a service (CCaaS). Its requirements are NO LEAKAGE during execution and NO RESIDUE after execution, within its enclave model. The authors state: “It requires that secrets are not leaked during the enclave execution and are zeroized immediately after use.” (§1, p. 4734). They formalize an abstract enclave, prove sufficient security constraints, and implement PoCF using a Rust typestate library, enclave prototypes, and a verifier. Side channels and denial of service are outside the threat model (§3, p. 4735).

technique: formal tagged-enclave model and PoBF theorems

What it is and when to use it. The model represents execution modes, memory locations, and secret tags independently of a particular hardware TEE. The authors explain: “We formally define the concept of ‘Being Forgotten’ and its two requirements for the purpose of establishing theoretic foundations to develop trustworthy enclave programs.” (§4, p. 4736). Inference: use this approach when a service needs explicit obligations for both secret confinement and erasure.

Steps in the paper (§§4.1–4.4, pp. 4736–4738): (1) tag values Secret, NotSecret, or Nonsense; represent enclave and normal modes, locations, and cells, with a confined Zone inside the enclave; (2) represent execution state as memory, mode, and accumulated errors, and programs using a modified Imp language with assignments, control flow, and enclave entry/exit; (3) define leakage as a Secret value outside Zone, strong residue as any remaining Secret value, and weak residue as allowing Secret in the return-value location; (4) prove Theorem 4.1: a nonleaking initial state, secret writes confined to Zone, and aborting on errors suffice for NO LEAKAGE; (5) prove Theorem 4.2: appending zeroization to a procedure satisfying NO LEAKAGE gives NO RESIDUE; (6) allow intermediate procedures to pass secrets through return values, but require the final procedure to leave no secrets, including in its return value. The model omits raw pointers and abstracts memory errors on the assumption that the implementation language enforces memory safety: “This aligns with our model and eliminates the need to model memory safety properties.” (§4.1, p. 4736).

Inference: a Verus adaptation could represent tags and abstract state with spec fn and encode transition lemmas as proof fn with requires and ensures. Such proofs would establish properties of that model; correspondence to TEE hardware, actual memory erasure, and excluded channels would require separate justification. The paper uses Coq for the formal model, not Verus.

Evidence and limits. These are sufficient constraints, not a characterization of every secure implementation (§4.3). The paper states: “CFI is an implicit prerequisite for PoCF.” (§5.2, p. 4739), where CFI means control flow integrity. Concurrent tasks must avoid shared state (§4.3, pp. 4737–4738).

technique: typestate state machine with contracts and zeroization

What it is and when to use it. PoCF encodes workflow states in Rust generic parameters and constrains transitions using trait bounds. The authors write: “Benefiting from Rust’s powerful type system, we encode a state machine with transition functions in typestate [77], where states are represented as generic parameters in pure Rust data structures (i.e., struct).” (§6.1, p. 4740). Inference: this approach suits a fixed decrypt–compute–encrypt workflow whose callers must not skip encryption or reuse an invalidated key.

Steps (§6.1, pp. 4740–4741; Figure 3, p. 4740): (1) define Task<S,K,D> with task state, key type, and data type; (2) constrain S with TaskState + DataState + KeyState, K with Zeroize + Default, and D with EncDec<K>; (3) specify states with pure predicates and Prusti annotations; (4) implement transitions consuming the old task and returning a task in the new state; (5) keep task fields and plaintext transitions private, exposing cc_compute() at DataReceived to decrypt, run the task, and encrypt its result; (6) invalidate and zeroize the key on output encryption; (7) instrument function epilogues to clear stack and registers except return values, and patch heap deallocation to zero freed memory. The paper warns: “Although the state machine based on the typestate scrubs residue at the language level, sensitive data may linger in memory.” (§6.1, p. 4741). Its spelling varies between Zeroize in code and Zerorize in prose.

Inference: a Verus version could retain typestate and specify key invalidation and ciphertext output in transition postconditions. Proving a logical state change alone would not demonstrate physical erasure by the allocator or epilogue instrumentation.

Evidence and limits. Prusti checks the typestate implementation against specifications; Rust checks the state contracts through its type system (§6.1). The authors identify verification limits: “Prusti strikes a balance between usability and complexity but can fail to verify some of the Rust features like nested generics and complex trait objects; the verification also takes a longer time.” (§8, p. 4746). The benchmarks configure stack cleanup for at most 20 pages, which the authors say is enough for those benchmarks (§7.2, pp. 4744–4745). Inference: those measurements do not establish sufficient stack cleanup for arbitrary tasks.

technique: layered verifier and attestation workflow

What it is and when to use it. PoCF combines compiler checks, contract verification, and taint analysis, then compares a locally obtained enclave measurement with remote attestation before provisioning secrets. The authors state: “The attestation report and verification result together serve as the ‘proof’ to the data provider, guaranteeing that the enclave is not able to threaten her private data.” (§5.1, p. 4739). Inference: the useful pattern is to bind the code that was checked to the service that receives the data.

Steps (§§6.2–6.3, pp. 4741–4743): (1) Rust checks memory and type safety; enclave source disallows unsafe code except ciphertext input conversion; (2) Prusti checks consistency between typestate implementation and specifications; (3) MIRAI tracks secret tags and checks that edge-call parameters lack Secret; (4) assess dependencies that could invoke edge functions; the authors report that their dependencies contain no system interfaces and the library has no external calls; (5) rebuild the enclave, obtain its measurement, and confirm the remote measurement before sending secrets. For proprietary task code, the paper proposes a trusted build system running inside an attested TEE as a verification broker. That is an alternative to the data provider rebuilding public source, not a prerequisite for every deployment. “First, the Rust compiler checks memory and type safety.” and “Finally, MIRAI performs taint analysis based on abstract interpretation.” (§6.3, p. 4742).

Inference: a Verus adaptation could require public or encrypted arguments at boundary functions and prove tag propagation through task operations. Attestation and compiler correctness would still require separate trust or verification.

Evidence, trust, and threat. The prototypes target Intel SGX and AMD SEV. Table 4 (p. 4744) reports four expected leaks but only one detected in each of the pointer and complex-struct tests; missed pointer cases include Rc<T>, Box<T>, and *const T. The authors concede: “However, it could fail when dealing with pointers and specific structs that need to propagate tags from their fields.” (§7.1, p. 4743). Inference: safe Rust alone does not remove the demonstrated smart-pointer and struct tracking limits.

The reported average overheads are 1.24% for identity and 0.28% for Polybench on SGX, and 0.86% and 0.94%, respectively, on SEV (§7.2, p. 4744). Each subtask has 10 repetitions per experiment setting. NATIVE runs inside an SGX enclave or encrypted SEV VM without PoCF mitigations. The paper states: “We measure the elapsed service time inside the enclave for the identity task and the elapsed time to execute the CC Task in Polybench.” (§7.2, p. 4744). Hardware and manufacturer SDKs are trusted; third-party tasks and other users’ inputs are untrusted (§3). Inference: the model proofs, imperfect taint analysis, instrumentation assumptions, and excluded channels must remain distinct when assessing the authors’ confidentiality claims.

techniques for the catalog

• formal tagged-enclave model — define secret-tagged states and prove sufficient confinement and erasure constraints
• typestate workflow contracts — encode CCaaS transitions in Rust generic states and combine key invalidation with stack, register, and heap cleanup
• layered verification and attestation — combine compiler, Prusti, MIRAI, dependency assessment, and measurement comparison before provisioning secrets

Checked 2026-10-16 against the full paper by a Codex agent (mid-paper quote: “The PoCF Enclave forbids the use of unsafe code in its source code, except for specific places where encrypted input from the untrusted world is received and converted to vectors in safe Rust.”): checked the full paper, quotations, technique steps, numbers, section and printed-page references, and publisher link; corrected model versus typestate distinctions, theorem conditions, quotation wording, page references, and trust and verification limits; did not inspect artifact code, reproduce proofs or benchmarks, or validate the proposed Verus adaptations.

Last edited: 2026-10-16