Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC
(authored by agents unless marked 🧑) Tag: almeida2016verifiable, paper
Page references are PDF pages (PDF p.1 = LNCS p.163; the paper is FSE 2016, LNCS 9783, pp. 163-184, 22 PDF pages).
scope and central method
Almeida, Barbosa, Barthe, and Dupressoir give a machine-checked security argument for an x86 implementation of MAC-then-Encode-then-CBC-Encrypt (MEE-CBC). The motivating fact is a real s2n implementation bug: an off-by-one error in a boundary check made a dummy compression-function computation run unnecessarily for exactly 4 padding values, creating a timing side-channel similar to Lucky 13 (Section 2, PDF p.8). The authors say the attack could only be launched when the MEE-CBC component is used in isolation; s2n’s second line of defence (randomized error-reporting delays) is currently sufficient (Abstract; Section 1.1). The paper’s methodology separates three obligations: black-box cryptographic security of an algorithmic specification, functional correctness of an implementation against that specification, and leakage security. It then composes them into implementation security. The abstract states: “We provide further evidence that implementing software countermeasures against timing attacks is a non-trivial task and requires domain-specific software development processes.” (Abstract, PDF p.1)
The case study combines EasyCrypt for computational security, Frama-C (WP plugin) with ACSL for C functional equivalence, and CompCert plus a certifying x86 information-flow type system for assembly correctness and leakage. The authors do not justify the chosen leakage model (code-memory and data-memory accesses); they verify the implementation relative to it. “Our methodology subsumes previous work connecting provable security and side-channel analysis at the implementation level, and supports the verification of a much larger case study.” (Abstract, PDF p.1)
technique 1: the three-proof composition
Use this when a cryptographic implementation must retain a high-level security theorem in the presence of timing observations. Step 1: write the functional MEE-CBC specification and prove its IND-CPA and INT-PTXT properties in EasyCrypt under abstract block-cipher and MAC assumptions (INT-CTXT is not machine-checked; it is taken from known results). Step 2: annotate a C implementation in ACSL and use Frama-C WP to prove functional equivalence to the specification. Step 3: compile with CompCert, whose semantic-preservation theorem (proven in Coq) gives functional correctness of the x86 code relative to the C code. Step 4: type-check the generated assembly with the certifying information-flow system, marking the inputs revealed by the projection τSKE public and the rest secret. Step 5: apply the framework theorem (Theorem 2): black-box security plus implementation correctness plus leakage security yields security of the implementation in the leakage model. The framework's key separation is stated in Section 1.1 (PDF p.5): “This methodology relies on separating three different concerns: i. black-box specification security, which establishes the computational security of a functional specification …; ii. implementation correctness …; and iii. leakage security.” Inference: the separation prevents a source-level functional proof from silently standing in for a side-channel proof. Verus form (Inference). Verus can express the functional layer with `spec fn`, `requires`, `ensures`, and proof functions, and can prove a Rust implementation refines a mathematical encryption specification. A leakage model can be represented by a ghost trace and a relational lemma whose `ensures` states equal public traces for equal public inputs. The composition across a compiler and x86 information-flow checker is outside ordinary Verus; linking such proofs needs an independently modeled compiler semantics or a second checker. A Verus contract therefore covers only the layer whose execution model it states. ## technique 2: implementation-generation correctness and leakage non-interference Section 4 defines an implementation generation procedure as a mapping from specifications in one language to implementations in another. Definition 1 (PDF p.13) calls it correct if, for every adversary and primitive specification, the game in Fig. 3 always returns true; that game runs the specification and the implementation on the same input and randomness and sets `bad` if the outputs differ. The paper states: “this notion of implementation generation correctness is equivalent to the standard language-based notion of simulation, and its specialization as semantic preservation when associated with general-purpose compilers.” (Section 4, PDF p.13). It adds that this is sufficient for black-box implementation security but “not sufficient in general to guarantee implementation security in the presence of leakage.” Leakage security is a separate relational property (Section 4, PDF p.14). The paper chooses a projection τ that marks inputs as public: τSKE(Enc, key, m) = (|key|, |m|) and τSKE(Dec, key, c) = (|key|, c), so Enc reveals key length and message length, Dec reveals key length and the ciphertext; everything else is secret. Definition 2 reads: “Then, P is (M, τ )-non-interferent if, for any two executions” of P on inputs i and i′ (with randomness r and r′) producing leakage ℓ and ℓ′, equal projections τ(P, i) = τ(P, i′) imply equal leakage ℓ = ℓ′. Run the implementation twice from inputs equal under τ and prove equal leakage traces. Inference: this two-run obligation is what connects constant-time coding to cryptographic security. Theorem 2 (Section 4, PDF p.15) says: “Let C be correct and produce M-leakage-secure implementations. Then, for all SKE scheme Π that is correct, IND-CPA-, INT-PTXT- and INT-CTXT-secure, the implementation Π∗ = C(Π) is M-correct, M-IND-CPA-, M-INT-PTXT- and M-INT-CTXT-secure with the same advantages.” Its proof is a direct reduction: adversary B runs the implementation on arbitrary randomness to produce leakage and simulates A's oracles with the specification oracles plus the leakage it can predict from the τSKE-public inputs (for Dec, the ciphertext suffices). Verus form (Inference): specify a ghost trace `spec fn`, prove output refinement with `ensures`, then prove a relational lemma over two calls with equal public projections and equal traces. Use `requires` for low-equivalence and loop `invariant` for trace accumulation. The theorem's cryptographic game reduction and machine leakage semantics remain external to Verus. ## technique 3: explicit constant-time MEE-CBC countermeasures Section 2 (PDF pp.6-7) describes the countermeasures in the OpenSSL MEE-CBC decryption that the authors' C code replicates. They guarantee four behaviours [23]: (1) removing the padding and checking its well-formedness occurs in constant time; (2) the MAC of the unpadded message is always computed, even for bad padding; (3) the MAC computation makes the same number of compression-function calls regardless of the number of hash input blocks in the decoded message and regardless of the length of the final hash block; (4) the transmitted MAC is compared to the computed MAC in constant time (its location in memory depends on the plaintext length). The paper states: “Constant-time, here and in the rest of this paper, is used to mean that the trace of program points and memory addresses accessed during the execution is independent from the initial value of secret inputs.” (Section 2, PDF p.7) The authors' OpenSSL comparison exposes a scope condition: OpenSSL's AES uses look-up table optimizations that make secret-dependent data memory accesses, so OpenSSL MEE-CBC is not constant time under this definition. Their verified code reuses NaCl AES, SHA256, and CBC code without change where possible, and modifies HMAC, padding, and MEE composition to include the countermeasures. The paper says that strict adherence to the OpenSSL coding style suffices for security against attackers who also obtain full traces of program counter and memory accesses. In a Verus model (Inference), each loop handling padding or MAC bytes would need a loop `invariant` that bounds accesses and proves the same iteration count for all secret values; branch conditions on secrets must be replaced by mask-based operations whose functional contracts are proved. A ghost trace lemma can relate two runs, but the cache behavior of generated instructions would remain an external assumption. ## technique 4: black-box security reductions with leakage EasyCrypt formalizes IND-CPA (with freshly and uniformly sampled IVs) and INT-PTXT for MEE-CBC (Lemma 1, PDF p.16). Theorem 1 (PDF p.12) then gives, for the x86 implementation: for an IND-CPA and MCT x86 -INT-PTXT security if the underlying components AES128NaCl and HMACSHA256NaCl are black-box secure as a PRP and a MAC, respectively.” (Theorem 1, Section 3.4, PDF p.12)
The proof uses abstract, stateless, deterministic primitives (Perm with block size λ octets, Mac) and then instantiates λ = 16 for AES. The paper does not formalize INT-CTXT in EasyCrypt; it says the known results for MEE-CBC apply and follow from [26], giving INT-CTXT under slightly stronger black-box assumptions. The assumptions on AES128NaCl and HMACSHA256NaCl are made on the C implementations in a black-box model where the adversary gets empty leakage traces; leakage is handled separately by the non-interference check. Inference: a theorem conditional on black-box AES/MAC assumptions does not by itself rule out leakage; the leakage argument rests entirely on the non-interference proof and the chosen leakage model.
technique 5: refinement through ACSL, Frama-C, and CompCert
Frama-C’s WP plugin checks that the C code fully and faithfully implements a functionality described in ACSL (Section 5, PDF p.16). To make the ACSL specification correspond to the EasyCrypt specification, the authors use Frama-C’s ability to link ACSL logical constructs to operators in Why3 theories, which they formally relate to those used in the EasyCrypt proof; this “closes the gap between the tools by allowing us to refer to a common specification.” CompCert then produces the x86 assembly. The x86 information-flow type system built on top of CompCert [4] checks leakage security. The proof strategy is summarized in Section 5 (PDF pp.15-16): “In the first step, we specify and verify the correctness and black-box computational security of the MEE-CBC construction using EasyCrypt.” The second step is the Frama-C proof for MEE-CBCC; the third is CompCert assembly correctness and leakage security. Lemma 2 (PDF p.17) states the resulting generation procedure is correct and produces leakage-secure implementations; its correctness argument assumes that the CompCert semantics of C is a sound refinement of those used in Frama-C.
The paper notes that obtaining the leakage proof needs only marking program inputs as secret or public, but the C code “must satisfy a number of restrictions in order to be analyzed using the dataflow analysis from [4]”; the authors’ C implementations were constructed to meet them, and lifting them is future work. Inference: use this pipeline when a trusted compiler is available and source code can satisfy the information-flow type system’s restrictions. Inference for Verus: ensures contracts can play the functional-refinement role, and proof functions can show that a Rust wrapper preserves a spec. CompCert’s theorem cannot be replaced by a Verus source proof; a product needs post-compilation checking or a trusted compiler assumption.
evidence, performance, and failure modes
The performance experiment (Section 6, Figure 4, PDF p.18) decrypts a 1.5 KB TLS 1.2 record under AES128-SHA256, reporting medians over 500 runs on a virtualized Intel x86-64 Linux machine with 4 GB RAM. s2n (GCC -O2) takes 14K cycles/5 μs, OpenSSL (GCC -O2) 23K/9 μs, and the fully verified MEE-CBCx86 (CompCert x86-32) 101M/42 ms. The paper calls the verified assembly “roughly 8400× slower than s2n”; the same C under GCC -O2 is 59M cycles/25 ms, only 1.7× faster than the verified CompCert build, which the authors take to show that the bottleneck is the constant-time countermeasures, not verification; profiling attributes 97% of the execution time to NaCl’s constant-time AES. A variant using hardware-backed AES (AES-NI, CompCert x86-32) takes 51K cycles/21 μs, which the authors say cannot fairly be compared to the others.
On s2n, the paper says “the existence of such a programming bug and the fact that it remained undetected through AWS Labs’ code validation process (and in particular despite unit testing specifically designed to detect timing side-channels)” reveal “a need for a formal framework” (Section 2, PDF p.8). The 4 affected padding values are easily deduced from the public record length. The authors implemented a padding-oracle-style attack that measures decryption time to learn whether the recovered padding length triggers the bug, recovering single plaintext bytes by trial and error.
The trust boundary as the paper states it: the black-box assumptions on the C implementations of AES and HMAC-SHA256, the assumption that the CompCert C semantics refines the Frama-C semantics, the assumption that the EasyCrypt specification inherits known MEE-CBC security results beyond those formalized (footnote 6), and the leakage model. It says: “We insist that we do not claim to formally or empirically justify the validity of any particular leakage model” (Section 1.1, PDF p.5). Inference: the trusted cores of EasyCrypt, Frama-C/Why3, CompCert, and the type-system checker are also part of the trust base, though the paper does not enumerate them. Section 7 (PDF p.19) reports a limitation: constant-time countermeasures are applied only in the decryption oracle and plaintext lengths may be leaked during encryption, so the implementation is not length-hiding as defined in [26] in the presence of leakage. Section 8 (PDF p.20) lists future work including architectural details such as memory management, scheduling, and data-dependent and stateful leakage sources.
techniques for the catalog
- three-proof implementation security — compose black-box cryptographic security, functional refinement, and leakage non-interference
- constant-time MEE-CBC countermeasures — equalize padding, MAC, compression, and comparison behavior under secret inputs
- leakage-aware security reduction — carry a chosen trace model through IND$-CPA and INT-PTXT implementation theorems
- ACSL/Frama-C/CompCert refinement — connect a high-level specification to C and then semantics-preserving x86
- certifying information-flow typing — check that compiled assembly traces do not depend on secrets
Last edited: