Detecting Possible Timing Attack Vulnerabilities in OpenTitan Big Number Accelerator Programs

Nielsen, Simon Svendsgaard ; Fjeldsø, Rasmus Nørgaard

4. term

Software, Master

2022

2022-06-10

54 pages

OpenTitan is a chip designed to secure a wide range of devices. We focus on the OpenTitan Big Number Accelerator, a co-processor of the OpenTitan chip, used for security-sensitive asymmetric cryptographic algorithms. In this work, we implement a tool to detect potential timing attack vulnerabilities in OTBN programs. The tool utilises different techniques, such as model checking, statistical model checking and symbolic execution. For model checking and statistical model checking, we use UPPAAL and UPPAAL SMC, respectively. We first construct a control flow graph (CFG) representing the OTBN program, which we use to construct various UPPAAL models representing the program. We then apply model checking and statistical model checking to find possible time differences. Some models are over-approximating, detecting time-differing traces unreachable in the original OTBN program. We extend the implemented interpreter to work with symbolic values, which we use for the TraceChecker capable of testing whether the traces are unreachable. Lastly, we use the implemented tool to show a timing difference in the RSA 3072 verify. We then remove the timing difference and use the implemented tool to verify that the program run in constant time.

OTBN ; OpenTitan ; Model Checking ; Symbolsk Eksekvering ; UPPAAL ; Time-channels

Download
View record in AAU Student Projects