Hot (or at least warm) on the tail of substratum, I’d like to introduce censor, a tool for identifying microarchitectural timing vulnerabilities in cryptographic software.
substratum scans compiled or disassembled assembly code statically to identify non-data-independent time instructions and secret-dependent branches or addresses. It can easily detect variable-time algorithmic errors and surprises introduced by optimizing compilers, ruling those classes of vulnerability out entirely. But as substratum works on instructions, its analysis cannot penetrate below that, i.e. to the so-called microarchitectural level of how a particular machine will execute those instructions.
censor exists for this purpose. It performs dynamic statistical testing of hypotheses based on actual runtime, as measured by e.g. wall-clock time, number of instructions actually executed, processor ticks (cycles) counted, and so on. It is thus capable of detecting microarchitectural timing variation introduced by anything measurable by time, including processor cache or branch predictor state, power or frequency effects, and even vendor error (e.g. if a supposed data-independent-time instruction were not such in practice).
censor is thus very useful for the “last mile” of constant-time verification. It is sort of the acid test as to whether a constant-time hypothesis really holds up on some particular hardware.
My aim in developing censor was to construct a flexible tool that could detect timing variations 1) on arbitrary targets, 2) over generic measurement backends (e.g. wall-clock time, cycle or instructions retired counts), 3) using a coherent and powerful statistical methodology. I don’t believe any other tools in this space accomplish anything close to (2) or (3), and certainly not to my satisfaction.
Regarding a “coherent statistical methodology,” censor is uncompromising and righteous. Many statistical methods, especially those from classical frequentist statistics, make assumptions about data that are typically absurd in practice. censor does none of that: it basically assumes that one has set up the test harness correctly, i.e. that one is actually testing what he thinks he’s testing, and otherwise its guarantees hold by construction.
Formally, censor assumes that if a target indeed runs in constant time, then measurements on it are exchangeable between classes. This is about the least-demanding assumption that one can make in statistics. In addition, violations of this kind of exchangeability are testable empirically, and, indeed, censor automatically checks these assumptions whenever it rejects a constant-time hypothesis.
What does it not require? Normality, absence of fat tails, fixed sample sizes, independence or stationarity across measurements, and so on. Classical statistical methods typically require many or all of these, the violation of which typically degrades, invisibly, false positive rates or statistical power. And these assumptions are frequently, if not usually, violated in practice.
Not so with censor: its results are intuitive, easy to understand, and honest. When you choose an acceptable false positive rate, you are guaranteed to get at most that false positive rate, or censor will call you out on having messed up your test harness. censor uses a so-called anytime-valid sequential testing methodology: an “online” framework which means that the current state of a test is always valid, no matter how often one looks at it, stops it, or resumes it.
I should note that I’ve checked the theory, not merely trusted it. censor contains a battery of validation tests that ensure that observed false positive rates on tens of thousands of adversarially-chosen example distributions are bounded by what theory predicts.
censor is also extremely powerful in the statistical sense. It is capable of detecting almost any form of measurable timing differential: subtle, consistent slowdowns; rarely-taken slow paths; slowdowns materialising as variations in distribution shape; slowdowns having identical shape but different variance; and so on. If censor rejects a constant-time hypothesis, it can even attribute the rejection to which particular form of differential was observed.
Moreover, censor tends to identify timing differentials rapidly. It detects gross timing leaks almost instantly, while more subtle leaks are detected using only as many samples as are necessary to accumulate sufficient evidence.
Like a good, albeit mostly-lapsed, statistician, I’ve characterised censor’s power empirically by injecting leaks into a number of base distributions and measuring the detection rate. Perhaps the best one-liner summary is that censor can reliably detect a one-nanosecond average difference in a ten-microsecond operation (a timing leak of 0.01%) in only about a thousand samples.
censor supports a number of meters, where a “meter” is basically a probe that can attach a number to an execution. So, in practice, one of: wall-clock time, hardware counts of retired instructions/branches, or processor cycles.
Each meter is useful for interrogating a different layer of the machine. The retired instructions and retired branches meters measure how many instructions the machine actually executed when running the code, whereas the cycles meter measures microarchitectural effects, viz. data-dependent latency and cache state. The wall-clock meter is, plainly, observed wall-clock time, which includes both architectural and microarchitectural effects, and is what an attacker observes in practice.
censor’s anytime-valid sequential testing framework is oblivious to meter, and functions identically, no matter which one is employed.
An interesting example on which to demonstrate censor is the message authentication code (MAC) equality comparison operator from ppad-sha256 v0.3.2. I’ll show it below for clarity:
instance Eq MAC where
-- Runs in variable-time only for invalid inputs.
(MAC a@(BI.PS _ _ la)) == (MAC b@(BI.PS _ _ lb))
| la /= lb = False
| otherwise = BS.foldl' (B..|.) 0 (BS.packZipWith B.xor a b) == 0The comparison has constant-time semantics: every byte in the first MAC is exclusive-or’d against the corresponding byte in the other MAC, then the resulting bytes are folded up via bytewise or, and the result is compared to zero. The semantics are constant time because a constant amount of work is performed, no matter what the value of each MAC is.
A substratum run on the LLVM backend-produced assembly highlights all non-runtime-related variable-time aarch64 instructions reachable from the MAC equality comparison symbol:
ppad substratum v0.2.3
input lib/Crypto/Hash/SHA256/Internal.s · aarch64 att · ghc (llvm)
profile aarch64, csel available
src lib/Crypto/Hash/SHA256/Internal.hs
note llvm backend
_czMq_info$def
7891 cond-branch b.lt LBB64_4 · load(Sp)
7903 cond-branch b.ne LBB64_3 · 87:55-59 counter [loop]
7905 cond-branch cbz x9, LBB64_14 · 87:37 ~load(Sp)
7908 cond-branch b.ne LBB64_7 · 87:37 ~load(Sp)
7928 cond-branch b.ne LBB64_8 · 87:37 counter [loop,vec]
7932 cond-branch b.eq LBB64_12 · 87:37 ~load(Sp) [vec]
7940 cond-branch b.ne LBB64_11 · 87:29-35 ~acc(load)+counter [loop]
7942 cond-branch cbz w11, LBB64_14 · 87:69 ~acc(load) [verdict]
ppad-sha256-0.3.2-inplace:Crypto.Hash.SHA256.Internal:$w$c==
7820 cond-branch b.ne LBB63_4 · 85-87 load(Sp)+entry(R4)
7822 cond-branch tbnz x25, #63, LBB63_5 · entry(R4)
root ppad-sha256-0.3.2-inplace:Crypto.Hash.SHA256.Internal:$w$c==
reach 8 symbols · 2 with findings · 10 nct events
verdict-format aarch64-v3An LLM confirms, via reference to the source, that every non-constant-time finding is benign:
- Every loop back-edge is counter [loop] derived from la (public length).
- Vector-tail dispatch branches (7905/7908/7932) are ~load(Sp) / [vec] on the public length.
- The only branch reading the accumulator is cbz w11 at 87:69, marked [verdict]; this reveals exactly the Boolean the caller observes.
So, algorithmically and architecturally, the assembly has clear constant time semantics. But, interestingly, censor detects that the code has measurable input-dependent variation on macOS:
(ppad-sha256 v0.3.2 MAC equality, aarch64/darwin)
$ cabal run -fllvm -fsha censor-sha wall
meter: wall, batch=2856 (auto), budget=50000
H0 control @0 vs @0 PASS after 50000 pairs
position @0 vs @7 REJECT after 194 pairs
position @0 vs @15 REJECT after 99 pairs
position @0 vs @31 REJECT after 475 pairsEach of these rows represents a constant-time test in which censor measures the wall-clock time of the equality operator between MACs drawn from each of two classes. You can visualise the test described by the first row, for example, as follows:
class A
MAC A0: ........ // a random MAC
MAC A1: x....... // A0, but different byte at index 0
class B
MAC B0: ........ // a random MAC
MAC B1: x....... // B0, but different byte at index 0The test is looking for a timing differential between A0 == A1 and B0 == B1. In this case, the classes A and B are identical, so we shouldn’t expect to see any difference at all, and indeed censor can’t reject the constant time hypothesis after sampling 50k pairs.
The test described in the second row looks like this:
class A
MAC A0: ........ // a random MAC
MAC A1: x....... // A0, but different byte at index 0
class B
MAC B0: ........ // a random MAC
MAC B1: .......x // B0, but different byte at index 7This test is again looking for a timing differential between A0 == A1 and B0 == B1, but note that class B genuinely differs from class A. What we don’t want to see is A0 == A1 taking less time than B0 == B1, but indeed, censor is able to reject the constant-time hypothesis here after sampling less than 200 pairs, and the same result holds for the other classes. This is very strong evidence that there is a material timing differential between these classes.
The aarch64 assembly analysis indicated no architectural source of variable time behaviour, so this leak must be microarchitectural, and specific to Apple Silicon. Of note, censor can’t detect a leak for the same code on x86-64/linux:
(ppad-sha256 v0.3.2 MAC equality, x86-64/linux)
$ cabal run -fllvm -fsha censor-sha wall
meter: wall, batch=449 (auto), budget=50000
H0 control @0 vs @0 PASS after 50000 pairs
position @0 vs @7 PASS after 50000 pairs
position @0 vs @15 PASS after 50000 pairs
position @0 vs @31 PASS after 50000 pairsThe exact reason for the evident microarchitectural variation is unknown to me, and I haven’t delved into it in any detail. ppad-sha256 v0.3.4 uses the following algorithm for its MAC equality comparison instead:
instance Eq MAC where
-- Runs in variable-time only for invalid inputs.
(MAC a@(BI.PS _ _ la)) == (MAC b@(BI.PS _ _ lb))
| la /= lb = False
| otherwise = go 0 0
where
go :: Word8 -> Int -> Bool
go !acc !i
| i == la = acc == 0
| otherwise =
let !x = BU.unsafeIndex a i
!y = BU.unsafeIndex b i
in go (acc B..|. B.xor x y) (i + 1)censor’s run on it on macOS detects no variation:
(ppad-sha256 v0.3.4 MAC equality, aarch64/darwin)
$ cabal run -fllvm -fsha censor-sha wall
meter: wall, batch=920 (auto), budget=50000
H0 control @0 vs @0 PASS after 50000 pairs
position @0 vs @7 PASS after 50000 pairs
position @0 vs @15 PASS after 50000 pairs
position @0 vs @31 PASS after 50000 pairscensor, like substratum, cannot prove that some particular code executes in constant time on some particular hardware, but I hazard that it comes pretty close! A timing vulnerability that can survive censor’s scrutiny (let alone an exploitable one) would be a very formidable vulnerability indeed.
Interested in using censor to understand or improve your constant-time profile? Merely get in touch.