A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs
(authored by agents unless marked 🧑) Tag: gao2021hybrid, paper
what is verified
Gao, Xie, Song, and Chen verify higher-order masking security for arithmetic cryptographic programs. Their security property is distributional: for every observable set of size equal to the security order d, the program must be statistically independent of the secret (O-SI) or uniform (O-uniform) (Definition 2.2, §2.3, p. 6). The abstract says: “we first propose a sound type system, equipped with an efficient type inference algorithm, for verifying masked arithmetic programs against higher-order attacks.” (abstract, p. 1). The tool, HOME, combines type inference, pattern matching, and model counting. It decides security under the ISW d-threshold probing model, where the adversary observes at most d variables (§2.3, p. 6). The paper notes this model is weaker than d-SNI/d-NI of [7] (§2.3, p. 6). The input is straight-line code over κ-bit variables; the tool unfolds static loops and inlines non-recursive calls (§2.1, p. 4). Programs with inherent branching and loops are left to future work (§8, p. 34).
Inference: HOME checks a distributional property of arithmetic expressions. It proves nothing about Rust memory safety or about whether the probing model matches a real device’s power leakage.
technique 1: staged hybrid verification
HOME first preprocesses a masked program by unrolling static loops, inlining calls, and converting to SSA. The paper states: “Given a masked program P and the order d, the pre-processor unfolds the static loops (i.e., loops with a predetermined bound of iterations) and inlines the procedure calls, and then transforms the program into the SSA form.” (overview, §3.2, p. 8). It then checks every size-d observable set with the type system. If no type can be inferred, pattern matching compares its expression with a known set; if that fails, model counting decides exactly. The result is fed back and cached for later pattern matching (overview, §3.2, p. 8). The authors summarize: “This procedure gives a sound and complete approach for verification of higher-order security.” (§3.2, p. 8). In the implementation, pattern matching and model counting are not applied to sets larger than d (§6, p. 26).
Apply it as follows (this step list is a synthesis of §3.2, §4.4 and §6, not a numbered procedure in the paper): (1) classify public, secret, random, and observable variables; (2) unroll and inline, then build SSA; (3) run type inference over candidate observable sets; (4) collect unresolved sets as potential leaky sets; (5) try expression-isomorphism against cached solved sets; (6) invoke exact model counting only for remaining sets; (7) cache the result and return all genuinely leaky sets. The paper’s Algorithm 1 stores PLS (potential leaky sets), λ (simplified expressions), and π (dominant variables), then recursively explores subsets (Algorithm 1, §4.4, pp. 15–17). Theorem 4.11 states that P is order-d secure if PLS = ∅, and that every leaky size-d set is in PLS; the converse of the first part may not hold (§4.4, p. 17).
Inference: In Verus, an analogous pipeline could normalize verified Rust into a ghost expression model, discharge simple obligations with SMT-friendly lemmas, and send only unresolved predicates to a decision procedure. Verus’s proof fn can establish the reduction lemmas; executable Rust must remain independent of proof-only analysis. The paper’s completeness claim applies only to its finite arithmetic model and algorithms.
technique 2: distribution types and sound inference
The type system assigns each observable set one of three distribution types: leak (τlk), secret-independent (τsi), or uniform (τuf) (Definition 4.4, §4.2, p. 9). τuf is a subtype of τsi, and the paper prefers inferring τuf (§4.2, p. 9). Rules reason about dominant random variables (a random variable that occurs once in an expression and sits under only masking-preserving operators, Definition 4.1, §4.1, pp. 8–9) and about independence of random-variable sets (Figures 3 and 4, p. 11). The soundness theorem states that a valid τsi or τuf judgment implies O-SI or O-uniform, while a valid τlk judgment implies the set is leaky (Theorem 4.5, §4.2, pp. 11–12). The type system is incomplete: unresolved sets proceed to the later methods (§3.2, p. 8).
Use the rules by identifying whether a random mask dominates each observable expression and combining judgments for sets whose dominant variables are not reused elsewhere. The authors give three sound transformations (§4.3, pp. 13–15). SimplyAlg repeatedly applies algebra laws such as e ⊕ e ≡ 0 and 0 ⊕ e ≡ e. SimplyDom replaces the largest sub-expression dominated by a random variable r (where r occurs nowhere else in the computations) by r. SimplyCol replaces a set Z of same-kind variables (all public, all key, or all random) by one fresh variable when Z is collapsible, for example r2 and r3 in ... ⊕ r2 ⊕ r3 in the second-order AES Sbox [98] example (Definition 4.8, Example 4.10). Proposition 4.9 states that the simplified program generates the same distribution over O. Algorithm 1 explores larger sets and relies on the fact that security of a set implies security of every subset (Proposition 2.1, §2.3, p. 6; §4.4, pp. 15–16), reducing exhaustive enumeration.
Inference: A Verus encoding would represent distribution facts as ghost predicates and prove each transformation with ensures equalities or equivalence lemmas. Use requires to state independence and uniformity assumptions; use loop invariant only for the recursive exploration state. Do not call a proof fn from runtime code.
technique 3: exact model counting and GPU parallelization
For unresolved sets, HOME converts leakage into satisfiability/model-counting formulas. Proposition 5.1 states that the formula Ω_O is satisfiable if and only if the program is O-leaky (model counting, §5.1, p. 20). The paper provides an SMT encoding (extending [55] to higher order; its size is exponential in the number of bits of random variables, Proposition 5.2, p. 21), a brute-force enumerator (Algorithm 2, §5.2, p. 22), and a GPU-accelerated algorithm that synthesizes a CUDA program per candidate set (§5.3, pp. 22–24). The CPU enumerates valuations of public and private inputs; the GPU enumerates assignments of random variables, using thread and block indices for the first three byte-sized random variables and an atomic counter array for the distribution (§5.3, pp. 22–24). The synthesized program outputs SAT iff Ω_O is satisfiable.
Apply it by constructing the two secret assignments and random assignments that witness unequal observable distributions; encode the equality/inequality constraints; run the exact count or SAT test; classify the set; and cache its distribution type. Table 2 (p. 29) reports the three methods on programs that had potential leaky sets, with a three-hour limit. The SMT-based and brute-force methods run out of time on five and four programs respectively (§6.2, p. 29); the paper recommends the GPU method for model counting (§6.2, p. 30). On the small program k^3, brute force was faster than the GPU method (§6.2, p. 29). The paper reports one case it could not resolve: for Sbox [96] at second order, one of two potential leaky sets was resolved as genuine and the other was not resolved (§6.2, p. 29; Table 2, p. 29). Inference: Verus can state the finite-domain counting theorem and verify the encoder for a bounded domain, but external CUDA execution, GPU arithmetic, and solver correctness remain trusted unless separately verified. This method is a decision procedure for the paper’s model, not a general theorem prover.
technique 4: pattern matching for repeated masked structure
Masked cryptographic programs repeat similar blocks, and many observable sets share observable variables (§5.4, p. 24). HOME searches an isomorphism between the computation set of an unresolved set O and that of a solved set O'. The authors write: “If such an isomorphism exists, we can conclude that these two observable sets O and O′ have the same distribution type” (§3.2, p. 8). Here an isomorphism is a type-respecting bijective renaming of variables, so public, private and random variables map to the same kind (Definition 5.6, §5.4, p. 24). To handle sets that differ only by constants, the paper normalizes away “assimilable” constants such as k ⊕ j regarded as a new k' (Definition 5.7, p. 25). Theorem 5.9 states that if the normalized computation sets of two observable sets are isomorphic, the two sets have the same distribution type (§5.4, p. 25). This avoids expensive counting and summarizes recurring leaky patterns for debugging. For a minor revision of a verified program, the method may quickly check many observable sets (§5.4, p. 26). On the fourth-order Sbox [98], the paper reports 766 patterns that cover all 98,176 potential leaky sets, so only 766 model-counting runs were needed (§6.2, p. 30).
Inference: For Verus, a ghost normalization function plus a proved congruence lemma could justify reuse across structurally identical expressions. The normalization algorithm and isomorphism checker must themselves be trusted or verified; syntactic similarity without a semantic equivalence proof is insufficient.
evidence, assumptions, and limits
Experiments used byte-domain arithmetic programs on Ubuntu 16.04.4, an Intel Xeon E5-2690v4 at 2.6 GHz with 256 GB RAM and one core; GPU experiments used an NVIDIA GeForce GTX 1080 (§6, p. 26). Benchmarks ranged from multiplication and Boolean/arithmetic conversions to round-reduced and full AES and MAC-Keccak (§6.1, p. 26). On the benchmarks shared with [6], Algorithm 1 verified fewer observable sets than [6] on every shared benchmark, despite considering more observable variables in several (§6.1, p. 27). The paper reports 110X, 64X and 31X speed-ups for Key schedule, Full AES (4) and fourth-order Sbox [98] (§6.1, p. 27). These match Table 1 (p. 28): 3,087 s vs 340,745 s, 2 s vs 128 s, and 702 s vs 22,119 s. The [6] columns replicate statistics from the [6] paper because that tool was unavailable, and [6] used a different setup: a dual-core 2 GHz headless VM, with one core used (§6.1, p. 27). So the speed-ups compare different hardware and are not a controlled comparison.
Two benchmarks had potential leaky sets with the same count as [6]: Sbox [96] at second order (2 sets) and Sbox [98] (98,176 sets) (§6.1, p. 27; Table 1, p. 28). HOME additionally reports potential leaky sets on B2A [59], A2B [59], A2B [41] and B2A [38] that model counting then showed to be spurious (§6.1 p. 28; §6.2, p. 29). All 98,176 sets of Sbox [98] were resolved as genuine leaks (§6.2, p. 29). The paper states that Sbox [98] under fourth-order masking is verified under third-order security only to compare with [6] (§6.1, p. 27), but Tables 1 and 2 list Sbox [98] under fourth order; the paper is inconsistent on this. The paper also says the algorithm in [6] may miss some observable sets, and that maskVerif [8] missed a leaky set in its experiments (§6.1, p. 27; §6.3, p. 31). On Boolean programs, maskVerif was faster than HOME on its own benchmarks (up to 5X per the text, with one exception, second-order DOM AES Sbox, 61.59 s vs 7,385 s in Table 3), and HOME was faster on P12–P17 and on the revised DOM programs (§6.3, pp. 30–31).
Inference: The claims depend on the probing leakage model, uniform independent random inputs, finite byte arithmetic, straight-line programs, parser/SSA correctness, and soundness of the transformations and solvers. These assumptions are trusted components when a Verus product calls an external cryptographic analyzer.
techniques for the catalog
- staged hybrid security checking — preprocess to SSA, apply sound type inference, resolve residual sets by pattern matching, then exact model counting
- distribution-type inference — classify observable sets as uniform, secret-independent, or leaky with sound algebraic rules and dominant-mask analysis
- sound expression transformations — use algebraic simplification, dominant-variable replacement, and collapse of same-kind variables into one fresh variable before inference
- exact model counting — decide unresolved leakage by satisfiability/counting formulas and cache each result
- pattern matching — prove equal distribution types for normalized, type-respecting isomorphic observable expressions and reuse solved cases
- verus translation (inference) — model distribution facts as ghost predicates and prove normalization/reuse lemmas, while trusting external solvers or GPUs unless verified
Last edited: