Detecting Possible Timing Attack Vulnerabilities in OpenTitan Big Number Accelerator Programs
Authors
Nielsen, Simon Svendsgaard ; Fjeldsø, Rasmus Nørgaard
Term
4. term
Education
Publication year
2022
Submitted on
2022-06-10
Pages
54
Abstract
OpenTitan is a chip designed to secure a wide range of devices. This thesis focuses on its Big Number Accelerator (OTBN), a helper processor for asymmetric cryptography. We build a tool that detects potential timing-attack risks in OTBN programs, meaning differences in execution time that could reveal secret data. Our approach combines model checking (systematic exploration), statistical model checking (sampling-based analysis), and symbolic execution (running with symbolic inputs). We first translate the OTBN program into a control-flow graph, then into UPPAAL and UPPAAL SMC models to search for possible timing differences. Because some models deliberately over-approximate the program and may raise false alarms, we extend the interpreter to handle symbolic values and add a TraceChecker to test whether the reported timing traces are actually reachable. Finally, we apply the tool to RSA 3072 verification, find a timing difference, remove it by modifying the code, and use the tool to confirm constant-time behavior, i.e., runtime independent of secret data.
OpenTitan er en chip, der er designet til at sikre en bred vifte af enheder. Denne afhandling fokuserer på OpenTitans Big Number Accelerator (OTBN), en hjælper-processor til asymmetrisk kryptografi. Vi udvikler et værktøj, der finder potentielle timingangreb i OTBN-programmer, dvs. forskelle i køretid, som kan afsløre hemmelige data. Metoden kombinerer modeltjek (systematisk udforskning), statistisk modeltjek (prøvebaseret undersøgelse) og symbolsk eksekvering (kørsel med symbolske input). Først omsætter vi OTBN-programmet til en kontrolflowgraf, som danner grundlag for UPPAAL- og UPPAAL SMC-modeller, der bruges til at søge efter mulige tidsforskelle. Nogle modeller over-approksimerer bevidst programmet og kan derfor give falske alarmer. For at filtrere dem udvider vi fortolkeren til at håndtere symbolske værdier og tilføjer en TraceChecker, der tester, om de rapporterede tidsforløb faktisk kan opstå. Til sidst anvender vi værktøjet på RSA 3072-verifikation, finder en tidsforskel, fjerner den med en kodeændring og bruger værktøjet til at bekræfte, at programmet kører i konstant tid, dvs. uafhængigt af hemmelige data.
[This apstract has been rewritten with the help of AI based on the project's original abstract]
Keywords