1# Constant Time Verification Tests for s2n 2 3This repository contains tests which ensure that key s2n functions 4are not susceptible to timing attacks and are indeed constant time. 5 6For more details, see https://github.com/awslabs/s2n/issues/463 7 8 9## What are timing side channels 10 11Crypographic protocols such as TLS are supposed to keep secret information secret. 12They do this by ensuring that WHICH bytes go over the wire is hidden using encryption. 13However, if the code is not carefully written, WHEN bytes go over the wire may depend 14on values that were supposed to remain secret. 15 16For example, if code checks a password as follows 17 18``` 19for (i = 0; i < length; ++i) { 20 if password[i] != input[i] { 21 send("bad password"); 22 } 23} 24``` 25then the amount of time until the reply message is received will depend on which byte in the password 26is incorrect. An attacker can simply guess 27 * a******* 28 * b******* 29 * c******* 30 31until the time to receive the error message changes, and then they know the first letter in the password. 32Repeating for the remaining characters turns an exponential guessing challenge into a linear one. 33 34There are two major ways that timing side channels appear in code 35 36### Branches that depend on secret data 37In this case, the program may execute more code, and hence take more time, in one branch than another. The password example above is a branch based timing side-channel. 38 39### Memory accesses that depend on secret data 40In this case, if one memory location is in cache, while another is not, there will be a detectable 41delay fetching the location from main memory. For example, an AES computation that uses 42software lookup tables can leak the secret key over the network based on cache timing 43https://cr.yp.to/antiforgery/cachetiming-20050414.pdf 44 45### The implication 46The runtime of code should not depend on the value of secret data, and therefore, cryptographic code should ensure that 47 1. No branch depends on secret data 48 2. No memory access depends on secret data 49 50 51 52 53## The tests 54 55Currently, we have constant-time proofs of two functions from utils/s2n_safety.c 561. s2n_constant_time_equals 572. s2n_constant_time_copy_or_dont 58 59 60A proof proceeds in the following steps: 611. Annotate public inputs using S2N_PUBLIC_INPUT(). All other inputs are assumed to be private 622. Use the ct-verif tool, which compiles the program into the Boogie intermediate representation, and adds assertions that: 63 1. No branch depends on secret data 64 2. No memory access depends on secret data 653. Use the Boogie program-analysis framework to convert the code under test into an SMT formula 664. Use the z3 prover to prove that either: 67 * None of the assertions can be violated (in which case the code is constant time) OR 68 * Some of the assertions can be violated, in which case the code is not guaranteed to be constant time. 69 70 71## How to execute the tests 72 73### Install the dependencies 74Running these tests will require the following dependencies 75(tested on Ubuntu 14.04). To see how to install this on a clean ubuntu machine, 76take a look at the ci scripts in this repo. 77 78- ct-verif (available from https://github.com/imdea-software/verifying-constant-time/) 79 - Export its base directory as $CTVERIF_DIR 80- SMACK and all its dependencies 81 - The easiest way to get these is to use the build.sh in smack/bin 82 - Ensure that all of the installed depencies are on the $PATH 83 - source the smack.environment that the smack build script creates 84 85### Move the code you want to test into place 86``` 87cp ../../utils/s2n_safety.c . 88``` 89### Execute the test 90 91``` 92make clean 93EXPECTED_PASS=2 94EXPECTED_FAIL=0 95make 2>&1 | ./count_success.pl $EXPECTED_PASS $EXPECTED_FAIL 96``` 97 98If both tests pass, you will see 99``` 100verified: 2 errors: 0 as expected 101``` 102 103If not all tests pass, you will see a message like: 104 105``` 106ERROR: Expected verified: 2 errors: 0. 107 Got verified: 1 errors: 1. 108``` 109 110 111## Questions? 112contact dsn@amazon.com