PhD position in Verification
Symbolic Validation Against Micro-Architecture Based Side-Channel Timing Attacks
Linköping University invites applications for a fully-funded position at the Embedded Systems Laboratory
Micro-architecture based timing side-channel attacks are difficult to uncover and defend against. To achieve such attacks, dynamic software properties resulting from micro-architectural details, such as cache behavior or branch prediction, are observed in order to retrieve secret and protected information.
The project develops a framework that allows to systematically assess, validate and possibly mitigate arbitrary programs against realistic classes of timing-channel attacks. The project aims for strong theoretical guarantees by combining symbolic execution and verification techniques with suitable models of micro-architectural components. The main goals of the project are the following:
- Derive realistic symbolic micro-architectural models (e.g., cache-behavior, out-of-order executions, branch predictions) on which timing-attacks are based.
- Combine the obtained micro-architectural models with efficient verification algorithms in order to assess and quantify the vulnerability of arbitrary programs against realistic timing-attack models.
- Propose compile-time transformations and runtime monitors to improve the resistance of programs to timing-channel attacks.
- At least a Bachelor degree in Computer Science or related fields.
- Solid knowledge in computer architecture and its modeling.
- Excellent programinng skills with kernel programming experience.
- Experience with using and implementing program analysis, including symbolic execution.
- Good background in discrete mathematics and logic.
Contact Ahmed Rezine for more information about the position or the project.
Date added: January 28, 2021