Author: Nemanja Lakicevic (Github profile)
Supervisor: Volker Stolz
Thesis: https://www.duo.uio.no/handle/10852/103923
As software systems become increasingly complex, there is a growing need for better tools and concepts to analyse and understand them. This requires practical instrumentation tools that can provide safe and efficient insights into running systems. Tools that enable better ways of reasoning about systems are required, especially as their state and behaviour change over time. Runtime verification is a promising field of research, which focuses on rigorously specifying properties of software systems and creating corresponding automata-based monitors. It positions itself as a lightweight formal method, by verifying whether the system under scrutiny satisfies specification under runtime. New observability and security enforcement tools are emerging in parallel. A novel tracing framework within the Linux ecosystem, eBPF, has quickly garnered attention for its to its versatility and effective tracing. This thesis explores the use of Linux eBPF for conducting runtime verification, and presents dottobpf, a tool which generates eBPF programs from three-valued LTL specification. The effectiveness of the tool, as well as suitability of eBPF for Runtime Verification is evaluated through the analysis of both single- and multi-process systems.