Runtime verification uses techniques from formal methods such as temporal logics and regular expressions to monitor software execution. In this thesis, we investigate new possibilities to combine this technique with formal specifications of correctness and performance properties.
BPF is an exciting monitoring facility for user-programs and OS kernels that is now widely used by e.g. Facebook and Netflix to monitor or debug services, also in the cloud. It gives insight into almost every aspect of a system in a safe manner:
Within the thesis, it’s possible to go pick one or more of several directions: monitoring kernel properties, or monitoring properties of specific applications, such as e.g. a web-server or some microservices. The focus can be on security properties (“there must have been a login before writes or updates are allowed”) or other properties (“the connection should not be rejected more than n times per minute”).
A very interesting application would also be investigating the use of sampling data e.g. every 50ms and using this possibly incomplete data for analysis.
A prospective student should…
- be able to use the Linux command line to set up and automate experiments (maybe in a container);
- be interested in understanding and formulating what it means for software to behave correctly.
| supervisors | Volker Stolz |
| Martin Steffen |