In a nutshell

The thesis will explore the possibilities to combine BPF instrumentation facilities with formal specifications of software execution in order to assert be- haviour of desired properties.

Background & motivation

Runtime verification is a system analysis approach based on extracting information from a running system and using it to assert violation or verification of specific properties. System properties can be expressed by formal specifications, such as temporal logics and regular expressions, and, by synthesis with moni- toring facilities, allow for precise formal reasoning about software execution.

BPF (Berkley Packet Filtering) is an exciting new tool for observing the Linux operating system. Originally designed for network packet filtering, it has since been extended to support a wide array of kernel functions, and is now widely used by e.g., Facebook, Netflix, and Google to monitor or debug services. A variety of system monitoring tools are already present in most Linux distributions. The novelty of BPF, however, is the ability to execute user code in kernel space in a thoroughly safe manner with negligible performance overhead.

Problem setting

More specifically, the thesis seeks to examine what capabilities BPF provides for runtime verification in terms of BPF language expressiveness, performance, observability (and it’s resolution), and complexity of implementation. Thesis work packages are organised as follows:

  1. Investigate BPF technology, understanding its capabilities and inner workings as well as conducting simple practical experiments in order to familiarise with technology.
  2. Study formal specification languages and automata theory that will provide the theoretical basis for system verification, and monitor generation tool.
  3. Implement the monitor generation tool.
  4. Conduct and evaluate case studies for the implemented tool. They will provide the opportunity to discuss eventual practical and/or theoretical pitfalls of tool and monitor implementation,

The work done in this thesis will shed light on the utilization of BPF monitoring facility, for formal specifications of automata, thus allowing for precise and formal reasoning about software execution.