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

Page view(s)

Last Week
Last month
checked on Nov 24, 2020


checked on Nov 24, 2020

Google ScholarTM


Note about this record


This item is licensed under a Creative Commons License Creative Commons