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

Verifying Constant-Time Implementations

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

scope and result

The paper defines constant-time security as equality of leakage observations for pairs of executions that agree on declared public inputs and public outputs. Its leakage model can expose branch conditions, memory indexes, and operand-size information. The central verification technique reduces this relational property to ordinary assertion safety of a product program that simulates two executions. The authors implement the reduction in ct-verif over optimized LLVM/Boogie code, with SMACK, Clang, LLVM, and Boogie/SMT, and formalize the output-insensitive reduction in Coq: for safe programs it is sound, and it is complete when there are no public outputs (Sections 3–5, pp. 57–60).

The paper’s abstract states: “We propose a novel approach for verifying constant-time security of real-world code.” It also states: “We implement our approach in a publicly available, cross-platform, and fully automated prototype, ct-verif, that leverages the SMACK and Boogie tools and verifies optimized LLVM implementations.” (Abstract, p. 53.)

technique 1: define the leakage contract

What it is. A leakage model maps each program configuration and execution to an observation sequence. The contract declares sets Xi of public inputs and Xo of publicly observable outputs. Two executions are compared only when their initial states are Xi-equivalent and final states are Xo-equivalent. The security definition requires equal observation sequences (Section 3, pp. 57–58). The machine-level definition additionally requires equal traces for initially public-input-equivalent infinite executions (Appendix A.3, pp. 69–70).

When to use it. Inference: use this before constructing a proof whenever “constant time” means a concrete observation policy. Choose branch observations for path security, indexed reads and writes for address security, and an operand-size function for instruction timing. The paper’s examples explicitly include branch conditions (Example 1), memory indexes (Example 2), and division operand sizes (Example 3), Section 3, p. 57.

How to do it. (1) Define the observation function L for every configuration and extend it by concatenation over executions. (2) List public input variables Xi and public output variables Xo. (3) Define equivalence of initial and final states on those sets. (4) Require equal L traces for every pair of complete executions satisfying both equivalences. The paper says: “Definition 1 (Constant-Time Security). A program is secure when all of its initially Xi -equivalent and finally Xo -equivalent executions are indistinguishable.” (Section 3, p. 58.)

Verus form. Inference: represent the policy as a ghost/specification relation over two abstract runs, with executable code unchanged. A Verus spec fn can compute an abstract trace from a modelled state; a proof function can establish that two runs have equal traces under preconditions describing public inputs and outputs. Verus does not automatically model LLVM instruction timing, so the trace and its correspondence to compiled observations must be explicit assumptions or separately proved lemmas. Inference: this is a proposed Verus adaptation, not a result evaluated by this paper.

Evidence and limits. The paper proves Theorem 1 for a while language in Coq; it gives a paper proof of Theorem 2 and leaves that construction’s Coq formalization for future work (Section 4, p. 59). The guarantee depends on the chosen observation model and on its public/secret annotations; it does not prove that the model includes every hardware side channel. The paper itself says the LLVM model is not generally sufficient for operand-based properties after code generation (Section 5.5, p. 61).

technique 2: output-insensitive product reduction

What it is. The output-insensitive product duplicates program variables, assumes each public input equals its renamed copy, and executes the two copies in lockstep. Before each paired subprogram it asserts equality of leakage observations. This is a specialized cross-product: divergent paths fail an assertion, which is exactly useful for policies requiring path agreement (Section 4, pp. 58–59).

How to do it. (1) Rename every variable in a second copy. (2) Insert assume x=x̂ for every x in Xi at entry. (3) Recursively instrument each subprogram with together(p). (4) At each subprogram, assert L(p)=L(p̂) using guard(p). (5) Execute the original and renamed statements adjacently via the instrumentation shown in Figures 7–8. (6) Prove ordinary assertion safety. The paper gives the construction: “The construction of the output-insensitive product of a program (with itself) is shown in Figure 7.” (Section 4, p. 58.)

Theorem 1 states that a safe program with no public outputs is secure if and only if its output-insensitive product is safe; with public outputs, safety remains a sound sufficient condition. The paper formalizes and proves this reduction in Coq for its while language (Section 4, pp. 58–59).

Verus form. Inference: write a ghost pair-state containing two copies of secret-dependent variables and a loop invariant asserting equality of the permitted observation prefix. Use requires for public-input equality and ensures for equal final traces; use a proof function to establish each step’s relational invariant. Keep the executable Rust single-copy; the product is proof-only ghost code. Verus’s invariant syntax belongs on loops, while the relational proof itself is expressed through proof functions and specifications.

Failure mode. Cross-product completeness fails when two executions legitimately diverge on public-output-dependent branches. The paper therefore distinguishes this construction from its output-sensitive variant; applying it to such code can reject secure programs (Theorem 1 discussion, p. 58).

technique 3: output-sensitive product with benign leakage

What it is. Information revealed by public outputs may legitimately influence control flow. The output-sensitive product records each side’s leakage history in history variables, allows annotated benign branches to diverge, and checks their equality at reconvergence. It asserts the accumulated comparison result after assuming equality of public outputs. This retains soundness and completeness while avoiding a full unconstrained self-composition in ordinary cases (Section 4, pp. 58–59).

How to do it. (1) Initialize same_observations := true. (2) Assume equality of Xi at entry. (3) At a branch marked benign, initialize histories h and ĥ, run each side independently while recording L observations, then conjoin h=ĥ into same_observations. (4) At non-benign branches, synchronize execution and conjoin equality of current observations into same_observations, delaying the final assertion until outputs have been assumed equal. (5) Assume equality of Xo at the end. (6) Assert same_observations. The paper explains: “The output-sensitive product begins and ends by assuming the equality of public inputs and outputs, respectively, with their renamed copies, and finally asserts that the observations made across both simulated executions are identical.” (Section 4, p. 58.)

Verus form. Inference: model each history as a ghost sequence or a summary predicate, and prove equality of the recorded observations under the procedure’s contract and equality of its final public outputs. Use a loop invariant to preserve the history relation; use ensures to state equality at return. A benign_branch annotation has no direct Verus equivalent; encode its permitted release in the specification and prove the release lemma explicitly.

Evidence and limits. Theorem 2 says a safe program is secure if and only if its output-sensitive product is safe with some benign-leakage annotation. The authors caution that annotations or annotation search are needed and that separate paths can be expensive, although benign regions are usually small and non-nested (Section 4, p. 59). The RSA PKCS#1 example declares message length mlen as the sole public output so the unavoidable copy length is treated as benign (Section 6.5, pp. 63–64).

technique 4: automated ct-verif pipeline

What it is. ct-verif compiles annotated C with Clang through SMACK, optimizes LLVM, translates to Boogie, applies the product construction, and invokes Boogie’s SMT-backed verifier (Section 5, p. 59). The C interface provides public_in, public_out, and benign_branching, plus SMACK handles for values, arrays, and return values (Section 5.1, pp. 59–60; Figure 10, p. 60).

How to do it. (1) Use the annotation API to mark the pointers, array contents, and return values that the interface contract permits to be public. (2) Compile and optimize with SMACK/Clang/LLVM. (3) Translate to Boogie and duplicate variables into a shadow state. (4) Prefix memory accesses and branches with equality assertions between original and shadow observations. (5) For annotated procedures, assume equality of public inputs at entry. (6) Use the output-sensitive replacement around potentially desynchronized blocks. (7) Inline all procedures and infer conjunctions of equalities between variables and their shadows, selecting variables that are both live at loop heads and dependencies of inserted assertions (Section 5.4, p. 60). The fix_pow example additionally needs a manual invariant (footnote 16, p. 63). The paper states: “Since secure implementations, and cryptographic primitives in particular, do not typically call recursive procedures, we instruct Boogie to inline all procedures during verification.” (Section 5.4, p. 60.)

Verus form. Inference: Rust code would expose public/secret boundaries through requires predicates and ghost views rather than C annotation calls. A Verus proof function can establish the shadow-state invariant; executable functions remain ordinary Rust. Memory separation must be stated with suitable pointer/ownership specifications, since Verus does not inherit SMACK’s DSA automatically.

Evidence. The experiments ran on a 2.7 GHz Intel i7 with 16 GB RAM; reported size is Boogie lines before inlining, and construction time is separated from verification time (Section 6, p. 61). Table 1 reports, for example, nacl_sha256_block at 20,000 lines, 27.7 seconds construction, and 4.17 seconds verification; nacl_sha512_block at 20,000 lines, 39.49 and 4.29 seconds (Table 1, p. 62). Table 2 reports MEE-CBC verification: OpenSSL 10.6 seconds construction and 18.73 seconds verification; NaCl 24.64 and 92.56 seconds (Table 2, p. 62). These times refer to individual examples. The OpenSSL MEE-CBC check excludes the assembly SHA-1 compression and AES-128 implementations; the paper notes that OpenSSL’s AES-128 makes secret-dependent memory accesses. The NaCl MEE-CBC example includes its low-level primitives (Section 6.2, p. 62).

Limits and assumptions. The prototype assumes memcpy/memset traces depend only on addresses and lengths, and assumes allocation results are secret-independent when malloc/free parameters are secret-independent (Section 6, p. 61). LLVM-to-machine correspondence is a confidence argument: “Operand-based constant-time properties, however, are generally not preserved: it is quite possible that instruction selection changes the types of some instruction’s operands, implying a gap between LLVM and machine assembly regarding whether operand sizes may depend on secrets.” (Section 5.5, p. 61). DSA may require explicit __VERIFIER_assume assumptions when memory separation is imprecise (Section 5.2, p. 60).

what is proved, trusted, and already done

The proved core is the reduction from the stated constant-time relation to assertion safety, with Coq proofs for the output-insensitive construction and theorems for both products. The implementation evidence is automated verification of selected cryptographic components and top-level APIs, not a proof of all deployed machine behavior. Inference: trusted or assumed parts include the leakage model, public annotations, SMACK/LLVM/Boogie/SMT, library behavior, allocator behavior, and the final compiler/processor mapping. The authors identify approximations in data-structure analysis and invariant inference as possible sources of verification incompleteness (Section 5.5, pp. 60–61).

techniques for the catalog

  • leakage-contract modeling — define public inputs/outputs and an observation trace over branches, addresses, or operand sizes
  • output-insensitive product — duplicate state, synchronize two runs, and reduce constant-time security to assertion safety
  • output-sensitive product — compare histories at reconvergence of benign public-output branches; assert the accumulated result after assuming equal public outputs
  • automated ct-verif pipeline — annotate C, instrument optimized LLVM/Boogie, and discharge generated assertions with SMT
  • memory and loop support — use memory-separation assumptions and equality invariants to scale the product proof; fix_pow needs a manually supplied invariant

Last edited: