Options
Detecting timing side-channels in executables
Citation Link: https://doi.org/10.15480/882.2852
Publikationstyp
Bachelor Thesis
Date Issued
2020-06-09
Sprache
English
Author(s)
Advisor
Gollmann, Dieter
Referee
Title Granting Institution
Technische Universität Hamburg
Place of Title Granting Institution
Hamburg
Examination Date
2020-06-26
TORE-DOI
TORE-URI
Citation
Technische Universität Hamburg (2020)
Constant-time implementations are a popular approach for defending against cache-timing attacks. It is necessary to verify the resulting executables of such implementations, because the compiler might introduce timing side-channels during code optimization, leaving the program vulnerable even though the source code has no indication of possible timing side-channels. This thesis proposes a novel approach for formally verifying executables to be constant-time, by developing a type system for scVerif's low-level, assembly-like intermediate language, which features explicit leak statements. The resulting type checker can detect timing side-channels for arbitrary leakage models, including data-dependent instruction timings. However, the implementation needs further work before it can be applied on real world cryptographic implementations. Once a better implementation of the approach exists, it can easily be used for automatic checks of executables for cache-timing side-channels. Users only have to specify the initial secrecy of every variable using easy to use source code comments.
Subjects
verification
cache-timing
side-channel
low-level
type checking
DDC Class
004: Informatik
600: Technik
620: Ingenieurwissenschaften
Loading...
Name
Detecting-Timing-Side-Channels-in-Executables.pdf
Size
309.84 KB
Format
Adobe PDF