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

Red Hat Research brings sustainability to the edge

Red Hat Research brings sustainability to the edge

A data-science-driven sustainability project supported by Red Hat Research was recognized as a FIWARE iHub at the 2023 FIWARE Summit in Vienna, Austria. Based on the SmartaByar smart village in Sweden, the project was a recipient of the Red Hat Collaboratory at Boston University Research Incubation Award in 2022 and 2023. FIWARE describes iHubs as centers for accelerated growth that support companies, cities, and developers in their innovation and digitalization journey by offering easy access to open source technologies, business development support, and community building.

Red Hat Collaboratory at Boston University announces Request for Proposals for 2024 Grants

Red Hat Collaboratory at Boston University announces Request for Proposals for 2024 Grants

The Red Hat Collaboratory at Boston University has announced details on the Request for Proposals (RFP) for 2024 Grants. The goal of the program is to enable collaborative research between Boston University researchers and Red Hat engineers. Projects must be open source and should generally focus on problems of distributed, operating, security, or network systems whose solution shows promise for advancing their field and impacting industry.

Watch recordings of the Mass Open Cloud Alliance Workshop

Watch recordings of the Mass Open Cloud Alliance Workshop

Over 30 Red Hatters attend the 2023 Mass Open Cloud (MOC) Alliance Workshop on March 20 - 21, 2023, at Boston University.  Recordings of each day of the event are available (see below with the schedule - currently unedited), and we will announce in the coming...

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