Growing pains: how to guarantee safety in systems with many components

A deafening beep keeps ringing in the hallway on the third floor of the high-rise building. One by one, the smoke detectors on the other floors go off to warn the residents of the fire - long before the smoke has spread throughout the building in thick clouds. This is because the detectors are connected and communicate with each other. CISPA faculty member Swen Jacobs is researching techniques that can help guarantee that systems with multiple communicating components run error-free and safely.

Many systems present themselves to users as a whole but are actually a mesh of multiple independent processors. The advantage of these so-called distributed systems is that they can execute several processes simultaneously. In addition, their performance can be increased if necessary by adding further processors. They are used, for example, in cloud computing, industrial control systems, or peer-to-peer applications such as Skype voice chat. Since the systems handle sensitive data and safety-critical applications, it is important that they are safe from attack and run without errors.

However, building distributed systems is complex and prone to errors, as many disruptive factors such as hardware or network failures and cyber-attacks must be taken into account, explains Swen Jacobs. Depending on where the systems are deployed, failures and disruptions can be annoying or even life-threatening. Therefore, an important part of the design process of hardware and software is their verification. It often happens fully automatically with the help of so-called model checking, in which a model of the program or hardware under investigation is used to formally prove that it will adhere to the specifications made and perform its functions.

However, in a growing system with multiple components that interact and communicate with each other, model checking reaches its limits. After all, what runs demonstrably error-free on a small scale does not necessarily work on a large scale. Jacobs’ goal is therefore to develop formal methods and tools that can provide security guarantees even for growing systems that execute different processes simultaneously. "The topic itself has definitely already arrived in practice and at large companies such as Amazon and Google, which, for example, also offer cloud services and have to guarantee their security. But what I'm doing is mainly concerned with the theoretical basics," explains the 41-year-old. Until now, security guarantees for such systems have depended on the number of their components, or interactive processes are used in which humans are involved in the testing. Jacobs wants to change that: "Our dream is to be able to trigger a fully automated verification after every change to the components, which would give us safety guarantees for a system of any size made up of these components."

In addition to advancing model checking, his research group is working on how results from model checking can be applied to automatic synthesis, the mechanical generation of systems that work safely from the ground up. Every year, Jacobs calls on researchers from all over the world to submit new tools for automatic synthesis at the Reactive Synthesis Competition.  

Jacobs received his PhD from the Max Plack Institute for Computer Science (MPI-INF) in Saarbrücken in 2010 and then spent two years at the École Polytechnique Fédérale (EPFL) in Lausanne, Switzerland, followed by two more years at the TU Graz. In 2014, he returned to Saarland and the University in Saarbrücken, where he was initially affiliated with Bernd Finkbeiner's group as a postdoc. However, a grant from the German Research Foundation (DFG) quickly provided him with his own project group, which he led for three years. In 2019, he finally habilitated at Saarland University, where he gives several lectures every semester. He has also been a research group leader at CISPA since the summer of 2018. "A stroke of luck for me."

This text was translated by: Oliver Schedler