Formal verification for constant-time cryptography Ján Jančár jan@neuromancer.sk IA072 December 4, 2020 Cryptography Side-channel attacks Timing attacks Formal verification for constant-time cryptography ○ ctgrind ○ ct-verif ○ SideTrail ○ ct-fuzz Cryptography Cryptography Symmetric ○ Uses the same key for decryption/encryption ○ Encryption, Hash functions, ... ○ AES, SHA1, SHA256, ... Asymmetric ○ Uses different keys for the operations (private + public = keypair) ○ Encryption, Digital signatures, Key exchange, ... ○ RSA, Diffie-Hellman, ECC, ... Post-quantum ○ Symmetric crypto is ok ○ Asymmetric broken by (future) quantum computers ○ Needs new algorithms ○ Lattices, Codes, Isogenies, ... Libraries & Protocols Jan Jancar Formal verification for constant-time cryptography 3 / 32 Cryptography Symmetric 0 0 P0 P1 Z0 Z1 absorbing squeezing r c Pn−1 f f … f f f … Bit and byte operations xor, and, shift, ... Byte permutations No number theory Rounds: same operations repeated for (let round=1; round> i) & 1) == 1 then Q = point_add(Q, N) N = point_double(N) return Q Jan Jancar Formal verification for constant-time cryptography 5 / 32 Cryptography Post-quantum Quantum computers break all classical asymmetric algorithms Post-quantum cryptography attempts to fix it More number theory (Fp, Fq, ...) More linear algebra Very large keys (kB) Lattices, Codes, Isogenies Jan Jancar Formal verification for constant-time cryptography 6 / 32 Cryptography Protocols & Libraries Basic crypto primitives are used in protocols Libraries collect primitives and protocols SSL/TLS, Signal, IPSec State machines Read message, decrypt, verify, process, sign, encrypt, respond Most in C, low-level functions in assembly Jan Jancar Formal verification for constant-time cryptography 7 / 32 Side-channel attacks Side-channel attacks Side-channels Power Electromagnetic radiation Cache Errors Time Sound, ... Jan Jancar Formal verification for constant-time cryptography 8 / 32 Side-channel attacks Power Transistors take some power to switch Switching in a clock cycle is data dependent Thus, power consumption is data dependent Hamming weight of operand often leaks Jan Jancar Formal verification for constant-time cryptography 9 / 32 Side-channel attacks Electromagnetic radiation Power also influences EM radiation from the circuit Get a good probe and record trace Can be localized to a part of a chip Jan Jancar Formal verification for constant-time cryptography 10 / 32 Side-channel attacks Cache Processors have several layers of memory cache Cache organized into cache lines Cache evicted in a Least Recently Used-like fashion Prime+Probe cache attack: ○ Malicious process accesses memory to prime all cache lines ○ Target process executes for a bit ○ Malicious process regains execution and checks the cache lines by timing how long a cache access takes ○ Cache hit: Target process did not touch cache line ○ Cache miss: Target process did touch cache line Jan Jancar Formal verification for constant-time cryptography 11 / 32 Timing attacks Timing attacks function checkPasswordVarTime(password) { let correct = "hunter2"; for (let i of correct) { if (i >= password.length || password[i] !== correct[i]) { return false; } } return true; } Jan Jancar Formal verification for constant-time cryptography 12 / 32 Timing attacks Minerva R = P Q = 2P for i from bit_length(k) to 0 do if ((k >> i) & 1) == 1 then R = R + Q; Q = 2Q else Q = R + Q; R = 2R return R Jan Jancar Formal verification for constant-time cryptography 12 / 32 Timing attacks Leakage models Remote attacker Wall clock time Local attacker (different process or VM) Branching Memory-access Operands to some instructions Instruction count Jan Jancar Formal verification for constant-time cryptography 13 / 32 Formal verification for constant-time cryptography Formal verification Want to somehow verify that implementations are constant-time What does that mean? Different for each tool ctgrind ct-verif SideTrail ct-fuzz + 23 more Jan Jancar Formal verification for constant-time cryptography 14 / 32 ctgrind Github Not really formal analysis Valgrind’s memcheck can warn on uninitialized memory use Use Valgrind to track branching and memory-accesses on secret values VALGRIND_MAKE_MEM_UNDEFINED (memcheck client_request) Can be included in tests and CI Has false positives and false negatives Jan Jancar Formal verification for constant-time cryptography 15 / 32 ct-verif Github Github paper Formal foundation on what "constant-time" means Sound and complete reduction-based approach to verifying constant-timeness Prototype implementation based on SMACK, Bam-bam-boogieman and Boogie Case studies using the prototype Jan Jancar Formal verification for constant-time cryptography 16 / 32 ct-verif Constant-time implementations p ::= skip | x[e1] := e2 | assert e | assume e | p1; p2 | if e then p1 else p2 | while e do p Defines constant-timeness on while programs, with arrays and assert/assume x are program variables e are expressions Jan Jancar Formal verification for constant-time cryptography 17 / 32 ct-verif Constant-time implementations A state s maps variables x and indices i ∈ N to values s(x, i), and we write s(e) to denote the value of expression e in state s. The distinguished error state ⊥ represents a state from which no transition is enabled. A configuration c = s, p is a state s along with a program p to be executed, and an execution is a sequence c1, c2, . . . , cn of configurations such that ci → ci+1 for 0 < i < n. safe execution: cn = ⊥, _ ; complete execution: cn = _, skip execution of program p: c1 = _, p , program is safe if all executions are safe Jan Jancar Formal verification for constant-time cryptography 18 / 32 ct-verif Constant-time implementations A leakage model L maps program configurations c to observations L(c), and extends to executions, mapping c1, . . . , cn to the observation L(c1, . . . , cn) = L(c1)L(c2) · · · L(cn). Two executions α and β are indistinguishable when L(α) = L(β) Branching model: s, if e then p1 else p2 → s(e) s, while e do p → s(e) Memory-access model: s, x0[e0] := e → s(e0)s(e1) · · · s(en) Operand model, for example: s, x[e1] := e2/e3 → S(e2, e3) Jan Jancar Formal verification for constant-time cryptography 19 / 32 ct-verif Constant-time implementations Given a set X of program variables, two configurations s1, _ and s2, _ are X-equivalent when s1 (x, i) = s2(x, i) for all x ∈ X and i ∈ N. Executions c1 . . . cn and c1 . . . cn are initially X-equivalent when c1 and c1 are X-equivalent, and finally X-equivalent when cn and cn are X-equivalent. Xi is the set of public inputs. Xo is the set of publicly observable outputs. Definition 1 (Constant-Time Security). A program is secure when all of its initally Xi-equivalent and finally Xo-equivalent executions are indistinguishable. Jan Jancar Formal verification for constant-time cryptography 20 / 32 ct-verif Reducing Security to Safety General idea: Create a new program Q by product of the program P with itself, then assert equality of leakage of the two instances Simpler output-insensitive product ○ Assume equality of public inputs Xi Complex output-sensitive product ○ Handle publicly observable outputs Xo Jan Jancar Formal verification for constant-time cryptography 21 / 32 ct-verif Implementation On the LLVM IR level Needs sources for annotation (public input/output, ...) Based on the SMACK toolchain, using the Boogie verifier Jan Jancar Formal verification for constant-time cryptography 23 / 32 ct-verif Discussion Sound and complete ○ Sound: Flags all insecure programs ○ Complete: Accepts all secure programs Needs source code annotation Complicated toolchain setup, outdated versions Usability? Jan Jancar Formal verification for constant-time cryptography 24 / 32 SideTrail Github paper Verification of time-balancedness ○ Weakening of constant-time notion ○ Leakage below some bound δ ○ Equivalent to constant-time for δ = 0 Uses time counter + instruction timing model For remote attackers Jan Jancar Formal verification for constant-time cryptography 25 / 32 SideTrail Time-Balancing δ-secure: For every possible public-input value, the timing difference between every pair of executions with different secrets is at most δ. Good for remote attackers (network jitter) Jan Jancar Formal verification for constant-time cryptography 26 / 32 SideTrail Verifying time-balancedness Similar to ct-verif Instrument program with timing counter ○ Leakage function l(c) mapping configurations c with state s to timing ○ To keep track of the total cost of an execution we extend the set of variables with a time counter l as VL = V ∪ {l} and write the time counter instrumented program PL as l1; p1; l2; p2 . . . ; ln; pn, in which each instruction li updates the time counter variable as l := l + l(s, pi). Compose PL with its renaming ˆPL over variables ˆVL to construct PL; ˆPL Assert the equality of timing leakages in PL and ˆPL at the end Jan Jancar Formal verification for constant-time cryptography 27 / 32 SideTrail Implementation Jan Jancar Formal verification for constant-time cryptography 28 / 32 ct-fuzz Github paper Uses self-composition to reduce testing two-safety properties into testing safety properties Then uses the afl-fuzz fuzzer to test Jan Jancar Formal verification for constant-time cryptography 29 / 32 ct-fuzz Secure Information Flow Program splitting via forking Derive inputs from fuzz input ○ Split into one public input ○ and into two secret inputs Record observations ○ Instrument to record memory-access and branches ○ Hash traces to save memory Compare and abort on inequality Jan Jancar Formal verification for constant-time cryptography 30 / 32 ct-fuzz Discussion Uses fuzzing, so not sound Uses fuzzing, so setup already done in CI Jan Jancar Formal verification for constant-time cryptography 31 / 32 Summary & Conclusions Cryptographic code is complex and small issues can lead to vulnerabilities Side-channels create hard to eliminate vulnerabilities There is an abundance of tools for verifying constant-timeness (collected 27, presented 4) Almost none of the tools are actually used Practical usability on real-world implementations is a concern Jan Jancar Formal verification for constant-time cryptography 32 / 32 Thanks! J08nY | neuromancer.sk | jan@neuromancer.sk Icons from & Font Awesome References Stefan Mangard, Elisabeth Oswald, Thomas Popp: Power Analysis Attacks Revealing the Secrets of Smartcards, ISBN 978-0-387-30857-9 Adam Langley: ctgrind José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Michael Emmi: Verifying Constant-Time Implementations, USENIX Security 2016 Konstantinos Athanasiou, Byron Cook, Michael Emmi, Colm MacCarthaigh, Daniel Schwartz-Narbonne, Serdar Tasiran: SideTrail: Verifying Time-Balancing of Cryptosystems, VSTTE 2018 Shaobo He, Michael Emmi, Gabriela Ciocarlie: ct-fuzz: Fuzzing for Timing Leaks, ICST 2020