I am working on the verification of security properties under the supervision of Prof. Gollmann from security in distributed applications department at TUHH. A special focus is placed on the growing threat from side-channels which can defeat even formally proven properties or protocols if not taken correctly into account. My work started with masking of software, a process for making programs resilient against physically observable side-channels. It extends to the assessment of quantitative information flow metrics, also outside the domain of covert channels.
In general, I am interested in verifying security properties of programs. My current investigations are based on trace- and hyperproperties which relate all possible executions of a program. Eventually, I wish to extend existing formal methods to improve verification of multi-faceted properties and their preservation during composition of systems. Ideally, composing multiple smaller programs into a greater system leaves all their individual security properties intact. I believe dependent type systems, relational logic, as well as the verification framework F* to be a good match for my undertaking.
My work is sponsored by NXP Semiconductors and the research project VeriSec funded by the Federal Ministry of Education and Research (BMBF).
Supervised Student Theses
- Security Analysis of USB Host Controller - A. Marotzke