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