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.