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

EU-funded cybersecurity consortium kicks off in Brno, Czech Republic

EU-funded cybersecurity consortium kicks off in Brno, Czech Republic

Authors Jaroslav Řezník, Principal Program Manager—Technical at Red HatViktor Malík, Senior Software Engineer at Red Hat Cybersecurity has become a critical focus of research in today's interconnected world, especially with the rise of cyberattacks posing a threat to...

Meet the new 2023 Red Hat Collaboratory Research Incubation Award Recipients

Meet the new 2023 Red Hat Collaboratory Research Incubation Award Recipients

We are pleased to announce the recipients of the 2023 Red Hat Collaboratory Research Incubation Awards. The awards are part of a joint effort between Red Hat and Boston University (BU) aimed at recognizing, supporting and funding research in cloud computing, and to advance the state of the art in open source technologies such as distributed systems, security, operating systems, and networking.

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...