NEW Initiative Proposal: Extending Runtime Verification (RV) Monitors with More Languages

[minyu66]

Title: Extending Runtime Verification (RV) Monitors with More Languages

Proposal: "The Linux kernel's runtime verification (RV) subsystem validates at runtime
that the system follows specified properties. These properties can currently
be written in two languages: deterministic automata (DA) and linear temporal
logic (LTL).

Deterministic automata are primitive: properties written as automata tend to
be large, complicated, and hard to review. LTL was introduced to ameliorate
this, but it still lacks the constructs to describe complex properties
elegantly. Additionally, LTL does not support timing, which is
crucial for some cases (e.g. verification of the deadline scheduler).

This project explores other potential languages for runtime
verification. Candidates include:

• Property Specification Language (PSL),which is standardized by IEEE, enhances the expressiveness power of of Linear Temporal Logic
• Signal Temporal Logic (STL) which extend LTL with timing properties"

How it supports ELISA: Runtime verification is a key building block for safety arguments about
Linux: instead of (or in addition to) arguing that the kernel is correct by
construction, RV monitors detect violations of safety properties at runtime.
Today, timing-related safety properties — such as deadline scheduler
guarantees or watchdog deadlines relevant to the Automotive and Medical
Devices working groups — cannot be expressed in the kernel's RV languages at
all. This initiative closes that gap and makes complex properties readable
enough to be reviewed as part of a safety case, directly supporting the
work on kernel safety claims and evidence.

Tangible Deliverables: (Months 1–3): A documented study evaluating different potential property
specification languages.

(Months 4–9): A kernel patch series implementing the promising languages
in Linux runtime verification.

(Months 10-12): A kernel patch series converting the existing RV
monitors (written in deterministic automata and linear temporal logic)
into better languages.

What's preventing progress: Lack of funding

Being worked on by other project/community: The RV subsystem already exists in the mainline Linux kernel with
support for deterministic automata and linear temporal logic as
specification languages. This initiative enhances RV with more advanced
languages.

Funding: around 11 months of work, details can be deliverd if this proceeds

If not pursued, what opportunities/benefits/capabilities will be lost The RV monitors would only support limited specification languages.

[matthew-l-weber]

NASA has some projects going with adding the copilot monitors to linux via eBPF and there was discussion on bringing this up to LFSCS. fyi @ivanperez-keera

[pahmann]

Comments from TSC meeting:

• This is more explorative compared to the concrete proposal in NEW Initiative Proposal: User-Defined Runtime Verification (RV) Monitors in the Linux Kernel #95
• Need to check, if there is already some ground work conducted (e.g. demo) to show where this could lead to.
• Has a good fit to ELISA mission and work.

[igor-stoppa]

I think my comment still stands, though.
Problems are the same.

https://github.com/elisa-tech/tsc/issues?q=state%3Aopen%20label%3A%22proposed%20initiative%22

[ivanperez-keera]

I would love to help with this.

[covanam]

I think my comment still stands, though. Problems are the same.

https://github.com/elisa-tech/tsc/issues?q=state%3Aopen%20label%3A%22proposed%20initiative%22

Hi, I am the proposal's author. I was not in the meeting. Do you mind explaining what problems are you referring to?

[covanam]

Comments from TSC meeting:

* This is more explorative compared to the concrete proposal in [NEW Initiative Proposal: User-Defined Runtime Verification (RV) Monitors in the Linux Kernel #95](https://github.com/elisa-tech/tsc/issues/95)

Yes, this is explorative.

* Need to check, if there is already some ground work conducted (e.g. demo) to show where this could lead to.

There is nothing yet. I intend the exploration phase to be part of the initiative, afterward we can decide whether to pursue it further.

[igor-stoppa]

I think my comment still stands, though. Problems are the same.
https://github.com/elisa-tech/tsc/issues?q=state%3Aopen%20label%3A%22proposed%20initiative%22

Hi, I am the proposal's author. I was not in the meeting. Do you mind explaining what problems are you referring to?

It seems I used the wrong link in my previosu comment.
Apologies. This should work: elisa-tech/Safety_Architecture_WG#14 (comment)

In a nutshell: any monitor is as weak as its dependencies. At least in principle. E.G. a monitor that is exposed to the interference it attepts to detect can be disabled by that same interference. What happens then?

[covanam]

In a nutshell: any monitor is as weak as its dependencies. At least in principle. E.G. a monitor that is exposed to the interference it attepts to detect can be disabled by that same interference. What happens then?

I acknowledge that RVM, just like any other software, is susceptible to errors. But that does not mean RVM cannot be useful. Similar to traditional testing, it is not proof of correctness, but it has been very helpful so far at pointing out problems.

For instance, we have monitors which detect incorrect real-time design patterns. We tried it on pipewire (real-time multimedia framework) and detected couple of issues, which we discussed with the pipewire's maintainer and fixed some of them. We also accidentally discovered a previously-unknown real-time issue with Linux vDSO thanks to RVM.

I mainly work with monitors which validate user-space processes. To ensure that RV monitors work, I have a bunch of sample user programs with issues. The monitors themselves are validated that they point out those exact issues.

We also have monitors which validate the kernel, which is developed by another person. I am not sure how he validates his monitors. But the same idea can apply, we can use faulty kernel modules or we can patch the kernel with issues, and validate that the monitors point out those exact issues.

I agree with you that the monitors would be questionable to validate their own dependencies, which is mainly the tracing subsystem (which includes kernel patching as you mentioned). But we can still monitor user-space processes. We can also monitor other parts of the kernel (e.g. we have some monitors for the scheduler); of course they are still the kernel and cannot be completely independent, but the issue is not that concerning.

There is no doubt that RVM is imperfect. It is possible that an issue manifest in a way that silences its detector (that sounds rare, however). But that does not mean we cannot get values out of it.

[igor-stoppa]

My point is that before trying to retrofit something existing that was created with different purposes and constraints, it would be better to first assess the chances it has to reach the end goal.

Safety is not a matter of "best effort" or "can get values out of it".

There are standards that specify what is expected to be able to achieve compliance.
What is the intention? To go for any compliance?
If yes, does the work have a way forward to that? How?

If not, then why would someone care about it, since - realistically - those who care about safety are making products and very often they need that compliance.

I'm just saying that without a clear self assessment, any activity remains an academic exercise.

Nothing wrong with that, but it would be better to say upfront what is the intended outcome.
And if the conclusion is that the intended outcome is not known, that is also a valid answer, but it should be communicated transparently, I think.

Exploratory activities are fine, as long as they are correctly declared as such.
Just beware that the point I mentioned needs to be addressed, if there is any wish to go beyond the academic exercise.