Please use this identifier to cite or link to this item:
Title: Detecting timing side-channels in executables
Language: English
Authors: Friemann, Jannik 
Keywords: verification;cache-timing;side-channel;low-level;type checking
Issue Date: 9-Jun-2020
Examination Date: 26-Jun-2020
Abstract (english): 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.
DOI: 10.15480/882.2852
Institute: Sicherheit in verteilten Anwendungen E-15 
Type: Bachelor Thesis
Advisor: Gollmann, Dieter 
Referee: Gourjon, Marc Olivier 
License: CC BY 4.0 (Attribution) CC BY 4.0 (Attribution)
Appears in Collections:Publications with fulltext

Files in This Item:
File Description SizeFormat
Detecting-Timing-Side-Channels-in-Executables.pdfAbschlussarbeit309,84 kBAdobe PDFThumbnail
Show full item record

Google ScholarTM


Note about this record


This item is licensed under a Creative Commons License Creative Commons