Runtime Verification with TeSSLa on a CPU/FPGA hybrid system

This is the description of a fully working runtime verification system for ARM CoreSight traces running on a CPU/FPGA hybrid system.

Schmid P
Runtime Verification with TeSSLa on Enzian
MSc thesis in Computer Science at the Systems Group, Department of Computer Science, ETH Zürich, Switzerland, supervision by Prof. Dr. Timothy Roscoe and Dr. David Cock.
thesis | Systems Group ETH Zürich | Enzian | doi.org/10.3929/ethz-b-000362312 | PDF | presentation

Runtime verification (RV) is a methodology to verify whether the behaviour of a (software) system satisfies the defined properties of a specification. This is of interest for safety-critical reactive systems.

Examples of simple specifications in different application domains:

  • memory allocation: all allocated memory is deallocated
  • event handler: maximum queueing time; a simple and an advanced specification are shown
  • access to critical sections protected with locks in multi-threaded programs

Example specification

Figure: Example of a simple specification in the Temporal Stream-based Specification Language (TeSSLa) used in this project.

The implemented RV system can process ARM CoreSight program traces, added instrumentation traces, and signals from FPGA part. The instrumentation library for glibc functions optionally wraps the program-under-test at load-time. Thus, no source code is required for the program to be verified.

CoreSight trace parsing and processing according to the given specification are handled within the FPGA, which offers enough bandwidth to handle the required throughput. A CPU/FPGA hybrid system (Xilinx Zynq-7000 SoC) was used for the implementation.

The recently published Temporal Stream-based Specification Language (TeSSLa) is designed to allow processing on data streams, which is in particular suitable for data processing on FPGA. A prototype TeSSLa to Verilog compiler – developed at the Institut für Softwaretechnik und Programmiersprachen, Universität zu Lübeck, Germany – could be used in this project to build a new RV system.

Various aspects of this prototype compiler could be improved. In particular, a critical bottleneck could be removed during this project, which is crucial to scale the RV solution to multi-core systems like Enzian or even rack-scale runtime verification.

This new RV system parses CS traces (new modules written in VHDL) and evaluates them with the embedded TeSSLa specification on FPGA, which allows online runtime verification of programs running on Linux (Ubuntu 18.04). Additional contributions include the new instrumentation library, an extended Linux kernel module for data processing, and data visualization tools.

Test programs were written to satisfy and violate the properties of the example specifications mentioned above. All evaluations were correct.

Details are explained in the thesis and the presentation PDFs.

tags:  arm c coresight enzian fpga tessla thesis vhdl zynq