Linux kernel 6.0 includes a runtime verification subsystem from Daniel Bristot de Oliveira

Oct 17, 2022 | Featured News, News

Red Hat Research’s Dr. Daniel Bristot de Oliveira continues to deliver practical improvements to the Linux kernel, this time with the addition of the Runtime Verification subsystem to the Linux kernel 6.0.

Daniel has been exploring methods to improve the analysis of the real-time properties of Linux over the past ten years. His research explores the tracing features of Linux to derive fine-grained properties of the kernel, overcoming a known limitation of the usage of black-box testing by developers while increasing confidence in Linux usage on safety-critical real-time systems. In May 2022, Red Hat Research shared news of Daniel’s contribution of the Real-Time Linux Analysis toolset (RTLA) as of the Linux 5.17 release. 

Daniel’s research has been featured in RHRQ in October 2020, February 2021, and May 2021.

Runtime Verification (RV) is a rigorous method that complements classical exhaustive verification techniques (such as model checking and theorem proving) with a more practical approach for complex systems. RV works by analyzing the trace of the system’s actual execution, comparing it against a formal specification of the system behavior. The main advantage is that RV can give precise information on the runtime behavior of the monitored system without the pitfalls of developing models that require a re-implementation of the entire system in a modeling language. 

Moreover, given an efficient monitoring method, it is possible to execute an online verification of a system, enabling the reaction for unexpected events and avoiding, for example, the propagation of a failure on safety-critical systems. Such verification tools are becoming essential to the development of Linux for safety-critical systems, targeting, for example, automotive and industrial applications.

The initial support for RV includes online monitors in the Linux kernel, but RV was designed with extensibility in mind. It is expected to be extended with other theoretical analysis tools, serving as the starting point for researchers and practitioners to develop other verification methods. Red Hat Research’s Dr. Daniel is the maintainer of RV in the Linux kernel and actively participates in the academic community, helping to fill the gap between theory and practice with collaboration from both communities.

Watch the Red Hat Research website for more theoretical and practical developments on runtime verification-related topics.

About Daniel 

Daniel has a joint PhD in Automation Engineering from Universidade Federal de Santa Catarina (Brazil) and Embedded Real-Time systems from Scuola Superiore Sant’Anna (Italy). Currently, he is a Senior Principal Software Engineer at Red Hat, working on developing the real-time features of the Linux kernel. Daniel helps in the maintenance of real-time related tracers and toolings for the Linux kernel and the SCHED_DEADLINE. He is an affiliate researcher at the Retis Lab and researches real-time and formal methods. He is an active member of the real-time academic community, participating in the technical program committee of academic conferences, such as the Real-Time Systems Symposium, the Real-Time Technology and Applications Symposium, and the Euromicro Conference on Real-Time Systems.

Related Stories

OpenShift on elastic secure bare metal infrastructure

OpenShift on elastic secure bare metal infrastructure

The Red Hat Research team supports several cloud environments, such as MOC Alliance and CloudLab. We realized there is a need to increase the productivity of bare metal machines in these environments and to promote leasing unused infrastructure to trusted partners....

Call for Project Ideas (North America Research Interest Group)

Call for Project Ideas (North America Research Interest Group)

Are you a Red Hatter with a project idea that needs a little help getting started? Could your project benefit from some intern power?  Red Hat Research (RHR) may be able to help by providing intern and research support to get your idea off the ground or to the next...

DevConf.CZ Mini 2022 features Red Hat supported research projects

DevConf.CZ Mini 2022 features Red Hat supported research projects

Held on November 3, DevConf.CZ Mini featured talks themed around Cloud and Hyperscale, Edge Computing, and Future Tech and Open Research, including two research collaborations with Brno University of Technology and Czech Technical University in Prague supported by Red...

Open source values are the focus of Red Hat Summer Camp in Brno

Open source values are the focus of Red Hat Summer Camp in Brno

In summer 2022, a group of Red Hat volunteers organized the first in-office run of Red Hat Summer Camp Brno: an IT camp aimed at high school students, regardless of how much IT experience they had. The goal of the summer camp was to bring together people with...

PHYSICS 4th General Assembly held

PHYSICS 4th General Assembly held

Yiannis Georgiou, Ryax, discussing project outcomes The 4th PHYSICS project General Assembly meeting was held July 4-6, 2022, hosted by RYAX in Athens, Greece. During the meeting, partners analyzed the project’s growth and had the opportunity to participate in person...

DevConf.US 2022 recordings available

DevConf.US 2022 recordings available

Recordings from DevConf.US 2022, August 17-20, 2022 in Boston, MA are now available on the DevConf.US 2022 YouTube playlist. This year’s conference featured talks on topics integral to Red Hat Research projects, including hybrid cloud and cloud computing, edge...