A Formally Verified Quantitative Analysis of the Information Flow in Hardware (Hardware Security):

This work will be done in collaboration with our research partners at TU Kaiserslautern.
The integrity and security of the hardware were taken for granted for quite some time. In the last years, more and more security problems in commercial hardware were made public, such as Meltdown and Spectre in certain processors. Nowadays a lot of research focuses on the topic of Hardware Security. Securing hardware and removing vulnerability issues before they are manufactured. A modern approach to achieving this is static analyses of the hardware architecture to assure certain security features.

In this work, we would like to address the development and evaluation of tools to elaborate the timing behavior of processor designs. The properties Confidentiality, Integrity (, Availability) and Authenticity (CI[A]A) need to be protected. And in this work, we focus on the combination of formal verification and information flow analysis.

We are looking to guarantee the four security features (CIAA) mentioned above for a processor design. Some example tasks are as follows:

• Researching state-of-the-art approaches
• Developing software tools to generate abstract models of the processor
• Researching vulnerabilities of processor architectures
• Developing schemes to elaborate the processor of those vulnerabilities
• Developing a software tool to identify vulnerabilities and quantify them

Lennart Reimann

Depending on the task the following is essential:

• Experience in object-oriented programming (python or C++)
• Linux OS
• Basic understanding of the hardware design and fabrication flow
• Basic understanding of processor architectures
• Some experience with Verilog and/or VHDL

In case of interest, please email me and include the following:

• Latest transcript of records
• A brief description of your background and motivation
• CV