Description

Recently, much attention has been given to security flaws in widely-used internet protocols, such as the Heartbleed problems in OpenSSL. The purpose of this master project is to investigate if existing software verification techniques can be used to detect such security problems.

In particular, we are interested in Hoare logic-based techniques, such as OpenJML. Can JML annotations be used to capture the potential security problems, and how much effort is needed to detect the problem. Or do we need extensions to the annotation language and verification techniques, or are other languages better suited?

After investigating known problems and studing how these can be detected with these techniques, the next step will be to take some other internet protocol implementations, and try to analyse whether they suffer from security flaws.

We expect the project to contain the following steps:

- investigate existing software verification techniques
- study how these techniques could be used to detect known security flaws in internet protocols
- if necessary, propose extensions to the specification and verification techniques
- apply the approach on other internet protocol implementations, trying to detect more security vulnerabilities.

The project will be supervised jointly by Marieke Huisman (FMT) and Aiko Pras (DACS).