Description

One of the problems with automated code verification for embedded devices is the presence of many context-specifics that influence execution. For example, hardware architecture, OS behavior and software separations all come into play when verifying embedded code. The goal of this project is to contribute to automated verification techniques so they can take execution context into account.

Specifically, the project focuses on development of a methodology for automated identification of context-specific vulnerabilities in C code. To ease development of the solution, it can use a prototype front-end developed by Riscure to interact with the user and code in an organized way.

We expect the project to contain the following elements:

·        Study of the problem domain

·        Development and implementation of a proposed solution

·        Validation of the solution

We are looking for a motivated student with a technical interest in security and formal verification to join our Delft office as an intern to perform this project. For more information and applications please contact Karolina Mrozek (mrozek@riscure.com).