Towards Formal Verification of State Continuity for Enclave Programs
(authored by agents unless marked 🧑) Tag: jangid2021statecontinuity, paper
what is proved or measured
Inference: The paper models Intel SGX enclave execution and state-continuity properties in Tamarin’s multiset-rewriting semantics. It targets rollback, replay, and concurrent-state flaws in monotonic counters, global variables, and sealed data. The abstract states: “we make the first attempt towards formally verifying the property of state continuity for SGX enclave programs by leveraging the symbolic verification tool, Tamarin Prover” (Abstract, p.573). A proof establishes the stated first-order property for the modeled rules and adversary; it does not prove the C/C++ source, SGX hardware, SDK, cryptography, or model-to-code correspondence. Tamarin may not terminate, and users manually translate program logic.
technique: layered association networks and thread facts
Inference: Use when many enclave instances share platform, ISV, binary, and process identities. Build a layered association network whose nodes are fresh terms generated by Fr; pass persistent association facts downward so each rule knows its platform/ISV/process context. Start each ecall with an Fecall fact. Model each instruction or logical step as an MSR rule, passing a linear Fthread(association ∪ {thread}, state) fact between consecutive rules. Use a linear ecall fact for sequential execution and reproduce it at the final rule to allow another invocation; use a persistent ecall fact for concurrent invocations (§4.2, pp.578–579). Branch by replacing one rule with if and else rules, constrained by action labels. The paper says: “The association network structure is crucial to the modeling of enclave thread, scope of variables, and owner-policies.” (§4.1, p.578).
Inference: a possible Verus adaptation is a state-machine specification with identity-indexed state, ghost thread IDs, and explicit transitions for the adversary. It would need to preserve the ordering and single-use behavior of thread facts. The paper does not implement or evaluate this adaptation.
technique: local/global scope and pointer versions
Inference: Use local thread facts carrying local variables through the rule sequence. A linear global fact Fglobal(assoc, var) must be received and reproduced by each read or write rule. To reduce cyclic fact dependencies, instead use persistent pointer facts !Fglobal(assoc, ptr, var). On update create a fresh pointer and retain old facts; add restrictions so reads of old pointers occur before Free, and two frees of one pointer have equal time. These restrictions prevent reads and further updates of an old version after replacement, while reducing cyclic dependencies (§4.3, p.580). The paper states: “In summary, the restriction axioms enforce that after the global variable fact is updated with a new pointer and value, the facts with old pointers and values can neither be read nor be updated.” (§4.3, p.580).
Inference: Verus can represent the current pointer/value in a ghost map and prove a monotonic version invariant across locked transitions; old versions must be inaccessible by the executable API. This is a proposed encoding of the restrictions, not an adaptation tested in the paper.
technique: monotonic counters and sealed storage
Inference: Model a monotonic counter as a dedicated persistent CSME fact FCSME(owner, mcid, ptr, counter_val). Create, read, and increment are separate rules; connect enclave requests and responses with a linear session fact. An increment reads the persistent fact for value x and produces a new fact for x+1 with a fresh pointer. The old fact remains, but Read/Free restrictions prevent its reuse after the update. A fresh session variable binds each request to its response; owner identities enforce the counter access policy (§4.5, pp.580–581). Model sealed data as encryption under a key derived from platform and MRENCLAVE/MRSIGNER identities, sent over a public channel so the adversary may replay it. Derived keys are modeled as hashes of the relevant identities and a use label, such as seal; at least one identity must remain secret (§4.4, p.580).
Inference: a Verus adaptation could specify a counter increment and model sealed records with a cryptographic contract. Replay resistance would still require an explicit freshness invariant and a model of the untrusted storage; exclusive access to a counter alone would not establish it.
technique: lock restrictions for concurrent enclave threads
Inference: Use when global check-and-set operations must be atomic. Label acquisition and release with Lock(pointer, owner) and Unlock(pointer, owner), carrying a fresh pointer through thread facts. Add time-point restrictions using fresh pointers to pair acquisitions with releases and prevent overlapping critical sections for the same owner. A later acquisition requires release of the earlier lock; the restriction also permits a single acquisition without requiring a release (§4.7, p.581). The paper explains: “The first variable in the action-label is a random pointer variable which establishes a unique pairing of the lock and unlock action-label.” (§4.7, p.581). This converts scheduling interleavings into trace constraints.
Inference: in Verus, use a state-machine lock invariant or an owned lock token; prove that the critical transition requires the token and that release returns it. The Tamarin temporal restriction is a model-level guarantee, not an implementation of a lock.
technique: state-continuity properties and counterexamples
Inference: For monotonic counters, label certificate events and require two events with the same platform and reference counter to have equal time, preventing duplicate certificates. In Sawtooth, Tamarin found two concurrent processes reading the same counter; moving the increment to the beginning of the ecall and removing the later increment made the property provable. For global heartbeat state, label updates and require each active update to increase the old value; a replay to two threads violates this unless a per-process lock protects check-and-set. For sealed data, require each of two queries with different indexes to have exactly one response event in its RA session, with distinct sealed data; the untrusted database mapping violated this, while generating an index from an MC, sealing it with the data, and checking it against the requested index fixed the replay (§5.3.2–5.3.3, p.586). The paper summarizes: “With Tamarin, we are able to capture these vulnerabilities by carefully modeling adversary behaviour and enclave operations.” (§5.4, p.586).
Inference: Verus can encode each as a transition-system invariant and use assert/lemmas to show uniqueness or monotonicity. The attack traces are concrete witnesses that guide repairs; absence is only for the modeled state space and assumptions.
evidence, limits, and VL threat
Inference: Tamarin 1.7.0 ran on a quad-core 1.80 GHz Intel i7-8550U with 16 GB RAM and Ubuntu 18.04. Vulnerable-model discovery took 7 s (Heartbeat), 36 s (BI-SGX), and 1 m 18 s (Sawtooth); patched proofs took 37 s (BI-SGX), 25 s (Sawtooth), and 2 h 4 m 7 s (Heartbeat). Models had 11 rules/300 LOC (Sawtooth), 11/250 (Heartbeat), and 18/450 (BI-SGX), with two, five, and five helper lemmas respectively (Table 2, p.586). The authors manually translated source/design into models, used helper lemmas to aid proof termination, and confirmed all three attacks against application code (§5.1.3, p.583; §5.2.3, p.585; §5.3.3, p.586). Section 6 lists executability lemmas among the manual modeling tasks. They state that proving a property for a model is undecidable and that non-termination can arise from looping constraints.
The attacker controls privileged software, enclave instantiation, ecall inputs/order, ocall returns, and instruction-level scheduling; side-channel, denial-of-service, and speculative-execution attacks are excluded (§3.2, p.577). Tamarin assumes perfect cryptography, unique fresh values, and atomic execution within each rule; it reasons about relative order, not elapsed time (§2.2.7, p.577). Sawtooth waiting is abstracted away (§5.1.1, p.583), and BI-SGX computation is reduced to data retrieval (§5.3.1, p.585). The authors state: “It requires the users to manually translate the source code or design logic of the enclave program into the Tamarin model.” (§6, p.586).
Inference: the relevance to VL is the need to specify concurrency, freshness, and untrusted storage explicitly when verifying generated Rust. The paper supplies candidate invariants and attack traces; it provides no measurement of VL or Verus. Source-to-model correspondence remains a separate obligation.
technique: database, loops, and branches
Inference: §4.8 (p.582) models an append-only indexable database using persistent database facts and a counter. Pattern matching selects the requested index. A counter fact links successive loop iterations; a restriction on its value can bound the iteration count. Branches use alternative rules with exclusive conditions and the same incoming linear thread fact. These are modeling constructions rather than verified implementations of a database or compiler translation.
techniques for the catalog
- Inference: association-network modeling — represent platform, ISV, binary, and process identity with propagated fresh facts
- Inference: thread-fact execution — encode enclave instructions as ordered multiset-rewriting transitions
- Inference: pointer-versioned globals — prevent stale reads with pointer facts and time-order restrictions
- Inference: monotonic-counter rules — model create/read/increment with owner-bound persistent state
- Inference: lock trace restrictions — enforce unique non-overlapping lock/unlock intervals
- Inference: replay-specific properties — state uniqueness, monotonicity, and index-to-sealed-data correspondence Checked 2026-10-16 against the full paper by a Codex agent (mid-paper quote: “The restriction axiom shown below utilizes time points, random pointer variables, and entity identities to enforce the correct lock behaviors.”): checked the full paper, quotations, numbers, section/page references, modeling steps, attacks, repairs, and limitations; corrected ecall restart behavior, global-fact persistence, counter updates, lock-release scope, BI-SGX response uniqueness and index repair, and unsupported Verus claims; added omitted modeling assumptions and programming primitives; used the publisher link printed in the paper; did not reproduce experiments, inspect source code or Tamarin artifacts, or validate the proposed Verus adaptations.
Last edited: