Gollmann, DieterDieterGollmann1132276268Friemann, JannikJannikFriemann2020-07-302020-07-302020-06-09Technische Universität Hamburg (2020)http://hdl.handle.net/11420/6908Constant-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.enhttps://creativecommons.org/licenses/by/4.0/verificationcache-timingside-channellow-leveltype checkingInformatikTechnikIngenieurwissenschaftenBachelor Thesis10.15480/882.285210.15480/882.2852Gourjon, Marc OlivierMarc OlivierGourjonOther