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

Oct 17, 2022 | 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

Red Hat extends partnership with Masaryk University

Red Hat extends partnership with Masaryk University

Many years of successful partnership with the Faculty of Informatics at Masaryk University has led to an extraordinary five-year contract confirming Red Hat’s long-term intention to support and develop research cooperation in cybersecurity. Red Hat also plans to...

Red Hat welcomes BU prof Orran Krieger to lead AI platform initiative

Red Hat welcomes BU prof Orran Krieger to lead AI platform initiative

Red Hat Research has periodically been fortunate to have faculty from Boston-area universities spend their sabbaticals working with our team. We’re happy to announce that in June 2024 we took this relationship to the next level by welcoming Boston University professor...

MGHPCC receives $16 million to deploy neutral atom quantum computer

MGHPCC receives $16 million to deploy neutral atom quantum computer

The Massachusetts Green High Performance Computing Center (MGHPCC) has received nearly $5 million from the state of Massachusetts and $11 million from QuEra Computing to create a natural atom quantum computing complex. The MOC Alliance will make the quantum computer...

AI, LLMs, and hybrid cloud get the spotlight at DevConf.US

AI, LLMs, and hybrid cloud get the spotlight at DevConf.US

Members of the Red Hat Research team and several of our collaborators are presenting at DevConf.US at Boston University, held August 14-16, 2024. This is the sixth annual convening of this Red Hat-sponsored technology conference for community projects and professional...

How to find Red Hat Research and our partners at DevConf.CZ 2024

How to find Red Hat Research and our partners at DevConf.CZ 2024

DevConf.CZ 2024 , held June 13-15 in Brno, features a packed agenda with talks on AI and data science, IoT and edge computing, security and cryptography, DevOps, and much more. As usual, many presentations feature the work of Red Hat Research and our research...