Secrets, kept

What is kept, and from what

A program is constant time when what it branches on, the addresses it reads and writes, and the operands of instructions whose time varies (the divider) depend on public inputs only (the model of ct-verif, Almeida et al., 2016, and of Barthe et al., 2018). The source keeps it; sysi must keep it too. A wipe is the other half: a buffer that held a key is zeroed before it is freed, and the stores must reach the machine.

Which inputs are secret is said, until sysp has secret types, in sysc's corpus, sysc/tests/secret/cases.rktd: per function, its secret parameters, or one field of a struct at any depth, (field a w) or (field s sha w) (specs/021: Noise's state holds SHA-256's beside its public count), and what it may make public, (declassify result out). sysi reads it and checks at two levels:

In sysi: what each value may be

sysi/secret.rkt gives each value two things: whether it is secret, and which places it may point to, a region and an offset. A region is the memory a parameter addresses, a buffer field's elements, a stack slot or a datum. A struct's bytes are told apart by offset, so a struct may hold a secret buffer beside a public flag. Here is sysc's Rnd, the random generator's state, as rnd-fill's case marks it (its words secret):

Red: secret. A load reads what may be at its bytes; a store adds its value there for every later load (memory has no order in the analysis). A load through an address of unknown origin is secret.

Calls are followed: the callee runs under its arguments' states, in the caller's regions, once per distinct state, and the whole runs until nothing changes. A function whose case declassifies its result gives it public to its callers: poly-check's answer, on which aead-open branches. Refused: a branch on a secret, an address from one, a div or rem with a secret operand (even by a constant, which the backend makes multiplications), a secret given to an extern, and a secret that ends in the result, a public field or buffer, or data, unless declassified.

In the machine code: what each term names

validate already runs each block's machine code symbolically, from symbols for the values live into the block, a load's bytes and a call's results. With #:secrets it marks the symbols that stand for secret values, so a term is secret when it names one: spills, moves and register shuffles carry the mark with them. It refuses a branch whose condition is secret, a secret memory address, a division of a secret, and a secret operand of any instruction not in this table:

The two levels are independent: sysi's check finds the secrets, and the machine check asks whether the backend introduced a dependence the source did not have (a branch inside a block, a division it chose). What nothing defines on a path (a clobbered register, a frame word no path wrote) counts as secret.

Wipes

sysi removes no store. The backend drops only instructions that write a register nobody reads, and both checks match stores one to one (refine against sysp, validate against sysi), so the stores of sysc's ct-wipe are in the machine code that passes them. tests/secret-test.rkt checks that its sysi stores and that validate accepts its code. It also runs a program of sysi's own, tests/programs/secrets.sysp: a buffer of secret words beside a public count, in a struct beside a public flag, where (field s in w) lets the code branch on the count and the flag, and (field s in) does not.

On sysc's corpus

tests/secret-test.rkt lowers sysc's library as its make check names it, and every file a case names: since sysc 036 sysp refuses the mistakes itself, from their secret clauses (sysp 102), so make check leaves tests/secret/mistakes.sysp out, and the test lowers them though sysp refuses them for where a secret goes (S001, S002), as sysi's check is a second one (specs/049), with a run for the runtime (tests/programs/secret-driver.sysp), and runs both levels on every case. In specs/020 its first run refused seven accepted cases, all for one reason: Poly1305's public byte count was word 22 of its secret state, and the code branched on it. No mark per argument or per field could say "secret but word 22", so sysc moved the count out (sysc 019, as libsodium and HACL* keep theirs), and all seven passed.

Cleared on return

Timing is not all a secret can leave: a value the allocator spills stays in the stack after the return, and one in a caller-saved register outlives the call. Built with --clear-cases (specs/022), each function of the corpus' accepted cases that no other of them calls zeroes, before it returns, the stack it and its callees may have written, and every caller-saved register but ra and its results, as -fzero-call-used-regs and HACL*'s stack clearing do:

Red: what the return zeroes. The depth is the function's frame and its deepest callee's, known statically: sysc's code has no recursion and calls nothing sysi cannot see, and a function that did is refused.

Inner functions do not clear: their frames lie below the outer one's, which clears them all once. On sysc's library the zeroing adds 768 instructions to 6,901. validate, given the same functions, computes the depth itself (not taking the backend's), forgets at every call what lies below the caller's stack pointer (the callee may write there), and proves at every return that each of those doublewords and registers is zero. tests/secret-test.rkt builds sysc's library so and validates it, and checks that validate refuses aead-seal built without clearing (since specs/027 it is aead-seal, which still makes calls and so has a stack to clear: chacha-block's calls are inlined).

The files