Introduce Runtime Verification Monitors#13
Conversation
In the Safety Architecture working group we are investigating the adoption of runtime verification monitors as a possibity to qualify the Kernel against specific safety claims. This commit: - create a new working area for runtime verification monitors - introduce the initial study performed by the working group Signed-off-by: Gabriele Paoloni <gpaoloni@redhat.com>
|
|
||
|
|
||
| 1. The kernel code implementing the requirement is correct; | ||
| 2. There is no unintended functionality in the current implementation; |
There was a problem hiding this comment.
I would replace "implementation" with module(s) or subsystem(s)
Or perhaps "implementation of subsystems involved"
Same for the rest.
There was a problem hiding this comment.
I'll propose a rewording to disambiguate between the whole active Kernel code AND the actual Kernel code implementing the ioctl syscall
|
|
||
| 1. Kernel code that functionally contributes to the allocated safety requirement | ||
| 2. Kernel code potentially invoked as part of the implementation but not contributing to the safety requirement (e.g. printk). | ||
|
|
There was a problem hiding this comment.
- Kernel code which might occasionally contribute to the allocated safety requirements. (e.g. the allocation of a certain quantity of memory can take very different paths, depending on the overall state of the system, without being directly affected by the use case at hand.
There was a problem hiding this comment.
IMO code that can "occasionally" contribute shall go under point 1. The reason for distinguishing between 1. and 2. is that code classified as 1. is the actual code to be modelled and monitored. The model has no notion of the probability associated with a specific state (and hence with a specific code path to be invoked), so I do not see why adding a class 3. as proposed here
There was a problem hiding this comment.
To better clarify that category one covers code that may contribute to the safety requirement but that it is not always guaranteed to be invoked at every invocation of the ioctl, replace "functionally contribute" with "functionally may contribute"
There was a problem hiding this comment.
Let me try to be more explicit (numbering will now be different):
- Kernel code that functionally contributes to the allocated safety requirement, since it has been designed to fulfill a specific purpose. E.g. a device driver that implements functionality associated to a FuSa requirement.
- Kernel code that incidentally contributes to the allocated safety requirement, since it has been designed to fulfill a system-level functionality that receives cascaded requirements from the code described in the previous point. E.g. scheduler, memory management, list primitives, locking primitives, etc.
- Kernel code potentially invoked as part of the implementation but not contributing to the safety requirement (e.g. printk).
I think this is the minimum differentiation needed, because even from the perspective of the RVM, it means that most likely all the aspects (or a great deal of them) of point 1 will have to be addressed, while point 2 is far more conditional, but still must be somehow addressedd. It cannot be ignored silently.
There was a problem hiding this comment.
Ok I like your classification.
I will update the doc accordingly.
| 1. Kernel code that functionally contributes to the allocated safety requirement | ||
| 2. Kernel code potentially invoked as part of the implementation but not contributing to the safety requirement (e.g. printk). | ||
|
|
||
| With respect to point 3. above we can have: |
There was a problem hiding this comment.
UHHH there was a problem with the conversion where letters got transposed into numbers :( . I'll fix it
There was a problem hiding this comment.
I meant that I had inserted a new point before your previous point number 3, which had become 4 -and it's still true, my previous comment is shifting your old numbers from 3 onward
There was a problem hiding this comment.
Got it. I will fix, thanks
| 3. Unintended functionalities due to interferences from Kernel code outside the implementation associated with classes A. and B. above. | ||
|
|
||
|
|
||
| When it comes to claim that code as in A. and B. are able to meet point 1 and point 2, for a complex SW component we need to hierarchically break it down into SW units, for each of these do a safety analysis and derive CoUs and Derived Safety Requirements; this regardless of code being classified as A. or B above. This process already proved to be very intensive even considering an entire subsystem like a single SW Unit (e.g. [STPA(-like) inside the Kernel ](https://docs.google.com/document/u/0/d/1K_cQSS2KYDnJQ0B91Zvlxq9-35Cx8ntbXwVMQJ51rvY/edit)). |
There was a problem hiding this comment.
A & B, 1& 2 tend to be confusing, why not quickly referring to them, instead?
There was a problem hiding this comment.
because I do not want to overwhelm the sentences expanding numbers and letters...
There was a problem hiding this comment.
Perhaps beak it down? Currently it feels like a Math book. :-) Or some regulation :-P
There was a problem hiding this comment.
what do you mean by "break it down" ?
There was a problem hiding this comment.
"break it down" as in: "unpack more the concepts, in a bit more verbose way, that is easier to assimilate"
There was a problem hiding this comment.
ok I'll try to propose something more natural language friendly in the next version
|
|
||
| When it comes to claim that code as in A. and B. are able to meet point 1 and point 2, for a complex SW component we need to hierarchically break it down into SW units, for each of these do a safety analysis and derive CoUs and Derived Safety Requirements; this regardless of code being classified as A. or B above. This process already proved to be very intensive even considering an entire subsystem like a single SW Unit (e.g. [STPA(-like) inside the Kernel ](https://docs.google.com/document/u/0/d/1K_cQSS2KYDnJQ0B91Zvlxq9-35Cx8ntbXwVMQJ51rvY/edit)). | ||
|
|
||
| Finally with respect to failure modes as in C it is well known that, as of today, there are no comprehensive architectural measures that can isolate Kernel implementing the allocated safety requirement from code outside the implementation associated with A. and B. |
There was a problem hiding this comment.
I would remove "well know", as it might give the impression that it's not factual.
There was a problem hiding this comment.
agreed. I'll rewrite as "with respect to failure modes as in C, as of today, there are"
|
|
||
| [Runtime Verification Monitors](https://docs.kernel.org/trace/rv/index.html) are mechanisms inside the Kernel that allow monitoring the Kernel itself to behave according to a predefined machine state diagram. \ | ||
| So if the Kernel misbehaves leading to a violation of points 1 or 2 above, the runtime verification monitor detects that the monitored Kernel code has violated the associated machine state diagram and accordingly raises an exception halting the execution or doing other custom remedial actions. \ | ||
| In this regard RV Monitors could be used not only to do control flow monitoring but also data integrity monitoring. In fact it may be possible to associate states with corresponding valid data sets that could be stored internally as part of the monitor specific data structures and, upon incoming events, it may be possible to check the correctness of the event specific data against the current state and associated data set. |
There was a problem hiding this comment.
*corresponding constraints or conditions
There was a problem hiding this comment.
Ok I can reword as "[...] with corresponding constraints and conditions; data sets could be stored internally as part of the monitor specific data [...]"
|
|
||
|
|
||
| * The hierarchical safety analysis of the Kernel and associated safety requirements definitions can be limited to code functionally contributing to the allocated safety reqs (class A above). | ||
| * The Runtime Verification Monitor provides an architectural protection mechanisms against Kernel interferences following a safety analysis of the resources to be monitored against interference failure modes |
There was a problem hiding this comment.
If I understand corectly, this point says that it ensures that what stated in the prvious one is sufficient. I'd say it more directly
There was a problem hiding this comment.
I am trying to say that we can limit the safety analysis to the functional code, since any unintended behavior triggered by non-functional code would be detected by the RVM monitoring the functional one....
| So if the Kernel misbehaves leading to a violation of points 1 or 2 above, the runtime verification monitor detects that the monitored Kernel code has violated the associated machine state diagram and accordingly raises an exception halting the execution or doing other custom remedial actions. \ | ||
| In this regard RV Monitors could be used not only to do control flow monitoring but also data integrity monitoring. In fact it may be possible to associate states with corresponding valid data sets that could be stored internally as part of the monitor specific data structures and, upon incoming events, it may be possible to check the correctness of the event specific data against the current state and associated data set. | ||
|
|
||
| So assuming that it is possible to prove FFI between RV Monitors and the rest of the Kernel code (see section below), adopting the RV Monitor solution would lead to the following advantages: |
There was a problem hiding this comment.
Somewhere there should be a clear statement that explicitly says this won't help if there are availability requirements to be met.
There was a problem hiding this comment.
I can add a section under "Limitations and Improvements" stating that if we are using RVM to make safety claims we do not have any advantage in terms of quality of the monitored code. This imply that a monitored code coming with low quality would directly impact availability requirements
|
|
||
| * The complexity of the Automata model is significantly lower than the code being monitored (i.e. when the code is capable of providing many functionalities under many different condition and states but only a specific subset of its potentials are used in a safety context); this implies that from a FuSa qualification effort perspective and continuous certification perspective dealing with a significantly smaller code baseline is cheaper and faster and hence it is better to make a systematic capability claim on the RV Monitor code instead of spending effort on proving the same for the monitored code. | ||
| * The expected behavior of the monitored code is comprehensively analyzed in how it would meet the allocated safety requirements. This is needed to guarantee that the monitor is monitoring all the critical states and data for safety reasons and to avoid the monitor triggering due to valid states and data not being analyzed. | ||
| * The specific use case being evaluated is compatible with ex-post-facto treatment of the failure: by design the RVM will be able to detect the failure only after it has taken place and it cannot avoid it (it works as detection measure, not as prevention one) . |
There was a problem hiding this comment.
Therefore, if availability is a requirement, the RVM is not sufficient.
There was a problem hiding this comment.
and it is not meant to be...
There was a problem hiding this comment.
yes, I did not mean to say that you implied otherwise, but I would like to make this document more accessible to people with less FuSa experience, and rather risk to state the obious, than optimistically expect the reader to draw autonomously the correct conclusions.
There was a problem hiding this comment.
Ok I can rephrase as "The specific use case being evaluated is compatible with ex-post-facto treatment of the failure: by design the RVM will be able to detect the failure only after it has taken place and it cannot avoid it (it works as detection measure, not as prevention one). Therefore, for events associated to unrecoverable failures, the RVM cannot provide assurance on the availability of the monitored functionalities"....WDYT ?
|
|
||
| A monitor is the central part of the runtime verification of a system. The monitor stands in between the formal specification of the desired (or undesired) behavior, and the trace of the actual system. | ||
|
|
||
| In Linux terms, the runtime verification monitors are encapsulated inside the RV monitor abstraction. A RV monitor includes a reference model of the system, a set of instances of the monitor defined at development time (e.g. per-cpu monitor, per-task monitor, and so on), and the helper functions that glue the monitor to the system. Depending on both the parameters being monitored and the specific hardware features available, different approaches can provide flexibility in managing the need of monitoring vs the overhead that it might introduce. More on this later. |
There was a problem hiding this comment.
If they are supported, I would add also device drivers, since they can be the hardest to qualify, when it comes to detecting interference.
There was a problem hiding this comment.
Add where? .... RVM can be designed to monitor any custom portion of Kernel code ranging from few files of a driver or subsystem, to an entire driver or subsystem and even to a group of drivers and subsystems (like in the example we made for the WTD...)
There was a problem hiding this comment.
wher you have the per-cpu, per-task list, it might seem that the RVM covers only system level features, but not peripherals. For the principle of least surprise (in the reader) I'd rather mention also device drvers.
There was a problem hiding this comment.
I can rephrase as <<A RV monitor includes a reference model of the system or of a subset of the system (e.g. a model of a specific subsystem or of a device driver), a set of instances of the monitor defined at development time (e.g. per-cpu monitor, per-task monitor, and so on) ... >> ...WDYt ?
|
|
||
| In Linux terms, the runtime verification monitors are encapsulated inside the RV monitor abstraction. A RV monitor includes a reference model of the system, a set of instances of the monitor defined at development time (e.g. per-cpu monitor, per-task monitor, and so on), and the helper functions that glue the monitor to the system. Depending on both the parameters being monitored and the specific hardware features available, different approaches can provide flexibility in managing the need of monitoring vs the overhead that it might introduce. More on this later. | ||
|
|
||
| Callbacks must be introduced in a way that is compatible with safety requirements allocated to the functionality they support (i.e. adding tracepoint by patching the code rather than by compiler could be more cost-effective from a FuSa effort point of view). |
There was a problem hiding this comment.
... more cost-effective, but less reliable, from a FuSa ...
There was a problem hiding this comment.
why less reliable ?
There was a problem hiding this comment.
because it adds one extra step which involves the kernel modifying itself.
It can have a level of reliability at most on par, but more likely lower, than the compiler time option.
I think this is beyond any debate. Self modifying code is inherently less safe, because it has a higher exposure to the risk of bugs.
There was a problem hiding this comment.
Ok I can rephrase as "(i.e. adding tracepoint by patching the code rather than by compiler could be more cost-effective from a FuSa effort point of view, but possibly more error-prone)"
There was a problem hiding this comment.
The part that really bothers me is to associate higher cost effectiveness to FuSa perspective.
FuSa is about making judgement calls that are specific to certain situations, so it is very misleading, IMO, to make such generalisation. I would leave FuSa out of this.
And even cost effectiveness, that is highly subjective. If I get sued because it turns out that I saved few developers-month by not doing the less-error prone thing. It means that I had the wrong FuSa perspective and also I was possibly not cost effective.
I think there are only 2 facts:
- doing runtime patching is riskier and error prone
- doing runtime patching here has only one potential advantage: to not invest into implementing a safer way for the RVM to connect to the rest.
I think we agree on the 1st.
WRT the second, I can only point out that this is the most objective view on it.
Then of course, if there is no budget, one tries to make ends meet, but I do not really see any advantage in retrofitting a mechanism that was designed with very different requirements in mind.
And then there's to answer the question: "Is it safe enough?"
There was a problem hiding this comment.
What about "[...]. I.e. adding tracepoint by patching the code rather than by compiler would avoid the effort of qualifying the compiler mechanism, however it would be more error-prone. So for example if the number of tracepoints if very less then the direct code patching could be a viable solution, whereas for a monitor with a significant number of tracepoints the compiler tracepoints solution would be more appropriate"
I think the tradeoff above reflects the reality .....
There was a problem hiding this comment.
Then, I would just leave out these considerations.
They are still bound to an evaluation of feasibility based on arbitrary assumptions.
There was a problem hiding this comment.
Ok let's just have "Callbacks must be introduced in a way that is compatible with safety requirements allocated to the functionality they support" without further specifications
|
|
||
| From a **temporal interference** point of view we can assume the safety relevant code (including the Kernel code) to be monitored by an external watchdog. So if such code slows down beyond the allocated max FDTI portion, the external watchdog will trigger. \ | ||
| Now the monitored code by definition is safety relevant code, and, as explained above, the associated RV monitor executes in the same context directly invoked by the trace interfaces added in the monitored code. \ | ||
| So if the monitored code slows down, the RV Monitor code equally slows down and as a result the external watchdog is not pet on time, with a safe state driven physically by the watchdog. |
There was a problem hiding this comment.
This is true only if the monitor is executed as part of the same queue matching the priority of the least prioritised task/event that is still relevant to safety. Unless that was the meaning of "same context". But then perhaps it might be more explicit.
There was a problem hiding this comment.
the RVM code is executed sequentially like a functiol call departing from the monitored code.....
There was a problem hiding this comment.
ok, then it falls within the "Unless ..." part of my previous comment, and I'd suggest to incorporate in the text what you just answered to me
There was a problem hiding this comment.
I can rephrase
<<Now the monitored code by definition is safety relevant code, and, as explained above, the associated RV monitor executes in the same context directly invoked by the trace interfaces added in the monitored code>>
AS
<<Now the monitored code by definition is safety relevant code, and, as explained above, the associated RV monitor executes sequentially in the same context of the code being monitored, since it is directly invoked by the trace interfaces added in the monitored code>>
If it clarifies better....
|
|
||
|
|
||
|
|
||
| 1. The Safety Application invokes the open syscall passing the input path from the filesystem associated with the watchdog to be opened. |
There was a problem hiding this comment.
This part is somewhat inconsistent: The kernel is not per-se safe, nor is the application, therefore they can fail before configuring and activating the WD.
We could say that there needs to be a further external safety element which is qualified to detect this event.
Or we could say that the WD is wired (some can be configured so) to start in a predefined mode, at power on.
Either way, all that matters is the fact that this one must be either properly correctly configured by a safe element, or it must be self-configuring.
But safety bootstrapping of the WD through kernel and pplication alone, is not a valid proposition.
There was a problem hiding this comment.
the application is assumed to be ASIL B, hence safe...
There was a problem hiding this comment.
The application can be implemented to be ASILB, however that doesn't preclude that the running application has been corrupted somehow, during loading, and therefore what is effectively being executed is not safe at all.
There was a problem hiding this comment.
Somewhere we can say that
a) We assume the safety app to be qualified at least up to the same ASIL that we target for the monitored Kernel code
b) We assume the Kernel code supporting the creation of the safety app address space and maintaining the integrity of the same to be already qualified at least up to the same ASIL as the safety app
Would that work?
There was a problem hiding this comment.
Without giving further justifications, it's an impossible-to-prove assumption :-D
How can that work?
There was a problem hiding this comment.
So WRT to a) it is a fair assumption since it is out of the scope of the operating system. Now WRT to b) we can say
"b) We assume the Kernel code supporting the creation of the safety app address space and maintaining the integrity of the same to be already qualified at least up to the same ASIL as the safety app. Such claims are in the scope of ELISA activities but not covered as part of this document"
There was a problem hiding this comment.
a) agreed
b) "If my grandmother had a wheel, she would have been a wheelbarrow" (Apologies, I coulnd't help it :-D )
In general I would not disagree, but here the assumption seems to overlap the scope of the document, which is about integrity (violations) in kenrel space.
There was a problem hiding this comment.
I was going to reply with a sentence about grandads and flippers but then I changed my mind... :)
This doc is explaining how we qualify the Kernel against the claims allocated to it by the safety app. Now you're saying "Hey look, we haven't proved that the Kernel is qualified against the claims of creating the app address space and maintaining its integrity", that is true, however it is not in the scope of the claims that I am analysing (hence the AoUs of the Kernel being qualified, somehow, against such claims).
The idea is that at some stage (I hope sooner, rather than later) we can also analyze what would take to qualify the Kernel against such claims, that are indeed also way more interesting than the one we are looking at.
So my ask is "please let's write this AoU for now and later we can address this"; actually I can add a note explaining that such a claim has to be considered as part of the future ELISA activities...
There was a problem hiding this comment.
Following the last WG discussion I will add a clear disclaimer at the top of the doc as in:
Disclaimer
This document only focuses on the qualification of the Kernel functionalities supporting the following requirements:
KSR_0003: the watchdog subsystem shall ensure the opened WD device to be the one specified as input argument;
KSR_0004: The watchdog subsystem shall ensure the WD timeout to be set according to the ioctl input parameter;
KSR_0005: The operating system shall ensure the WD timeout to be not wrongly re-set to a different timeout value;
KSR_0012: Writing the Watchdog shall reset it with a timeout equal to the one specified in the IOCTL. No other timeout value shall be used / reconfigured
All other Kernel Safety Requirements defined in Telltale_Safe are not in the scope of this document.
Therefore the solution proposed in this document is NOT sufficient to qualify the Kernel against all the allocated safety requirements; only a subset of them is covered.
| 12. Write the same shifted value to `ESB_TIMER2_REG;` | ||
| 13. Unlocks the watchdog registers for write access; | ||
| 14. Reloads the external watchdog (stops any previous counting) | ||
| 6. If successful the Kernels returns 0 to the Safety Application, else -1 is returned. |
There was a problem hiding this comment.
So, basically, till here, this might work for re-configuring the WD, but strictly speaking, it is not part of the safe initialisation and it could be omitted, I think, because per-se it is not sufficient to claim that the WD was initialised safel.
There was a problem hiding this comment.
I don't understand....here the Kernel programs the WTD with the timeout passed by the safety app and restart the WTD timer. If it doesn't program the WTD with the right value OR it does not kick off the WTD timer our safety mechanism (the WTD) will not work as expected and the safety app will continue un-monitored....
There was a problem hiding this comment.
Exactly!
My point is that the WD needs to have been initialised by whatever started the safe app, not the safe app itself.
The safe app should be allowed - possiby - to reprogram the WD ONLY after it has been proven that the allegedly safe app is indeed safe, in this specific round of execution. But in a simpler scenario the safe app doesn't program the WD, which gets setup by the safe component that spawned the safe app.
There was a problem hiding this comment.
But by definition, considering how the program is structured, the safety APP does not start the actual safe operations till the ioctl returns success, so if, for any reason, the App never comes to the point of ioctl returning success, there would be no harm involved
There was a problem hiding this comment.
I am trying to describe how a more generic system should be designed.
What we have here is a corner case. It can be described as a corner case, taking advantage of its corner-casyness, of course.
But how useful is it? To a reader who probably needs to adapt this to something else?
I'd rather have the corner case to still be implemented in a generic way and take advantage of being "special" only as the last resort, to get out of a problem that could otherwise not be solved.
This is definitely not the case.
There was a problem hiding this comment.
From a use case perspective, the arch wg relies on domain WGs to define a safety concept and allocate requirements on the OS.
Now if you roll back in history you will realise that telltale was the only completed TSC from the automotive WG. What I always said in every forum is that the Arch WG will keep investigating methodologies to analyse and qualify the Kernel given a set of safety requirements and then, when a more realistic use case is available, the WG will re-align to it.
So from my perspective you are stating the obvious. What you are missing instead is that, even under assumptions of claims to be demonstrated, the methodology we are working on is still useful and scalable later to other more realistic use cases.
There was a problem hiding this comment.
eh, initially I did not arue against this because it looked like this might be made to work ...
but it seems now clear that it will not reach a real conclusion, because of lack of documentation
sure, one can argue that the documentation can be enhanced, but even doing that, the claims will then rest on a variety of avoidable burdens
so, I wonder, why not just fixing this?
but hey, these are just my thoughts and the arguments supporting them
if you think they are wrong or inconsistent, feel free to ignore them, you don't have to convince me :)
There was a problem hiding this comment.
Igor AFAIK the Automotive WG tried to revisit the telltale use case to match something more "realistic", but in the end the work was not completed while now the automotive WG focus is shifting.
Realistically, IMO, what we can do is to:
a) complete this RVM excercise e refine the Kernel analysis methodology with the OSEP wg
b) we could discuss internally in our WG what modification we could do (with the HW we have) and eventually propose to revisit the Telltale v1 completed TSC (however this should be double checked with Phillipp)
c) Nothing prevents us from analysing different aspects of Linux against different safety claims eirther in the LFSCS, OSEP WG and Arch WG. Respectively from
- technical and code enhancement perspective
- methodological perspective
- safety analysis perspective
There was a problem hiding this comment.
As discussed in the previous WG meeting we will complete this document covering only a subset of the Kernel Safety requirements defined from the Telltale Automotive WG use case. Now a DISCLAIMER will be proposed (as per comment here) to avoid misleading the audience. Then later we can revisit the doc once we have a more realistic or better use case.
|
|
||
| ## Tracepoints | ||
|
|
||
| **TODO**: evaluate if it is safer OR easier (in terms of FuSa effort) to resolve monitoring points at compile time instead of using runtime tracepoints. |
There was a problem hiding this comment.
compile-time can be verified statically - hard to beat that :-D
There was a problem hiding this comment.
noted....but is it OK to leave the TODO as written above or you want to propose a modification in the text ?
There was a problem hiding this comment.
I would prefer to say it explicitly that compile time is the preferred approach, because the other option is not equally safe (and good luck proving that it is sufficiently safe)
There was a problem hiding this comment.
Ok I think we can remove the TODO and just state:
<<Relying on runtime tracepoints implies allocating safety requirements to a mechanisms that is more complex than relying on compile time resolution of monitoring points hooks; therefore it may be preferable to use compile time ones. However each user can make his own analysis in this regard>>. Ok ?
|
|
||
| ## Monitored Data access | ||
|
|
||
| **TODO**: evaluate if, for failure avoidance purposes and hence availability purposes, it is doable to directly read the data to be monitored from the monitored code heap or stack instead of passing it as parameters on the stack. The rationale is that passing critical data through function parameters would increase the surface of possible corruption. |
There was a problem hiding this comment.
... corruption. Which is not relevant from integrity perspective, but it is from availability perspective.
There was a problem hiding this comment.
right, it is written on top "and hence availability purposes" ....
|
|
||
| The effect of the interference is not easy to generalise, because it strongly depends on which type of peripheral and registers are involved and what values might be written there. | ||
|
|
||
| * Especially on 64 bit systems which are capable of addressing a very large address space, it is also possible that nothing is associated with a specific address; in such a case, a write operation will fail with a bus error and it will trigger an exception. This scenario can be considered as safe, because the exception will be noticed by the system and it can be acted upon (usually an MMU translation error). |
There was a problem hiding this comment.
Note: exceptions can be disabled, in a logic way, even if not through hardware. For example, the verification that confirms the rodata memory is effectively write protected does just that. It attempts a write over protected memory, but without the kernel treating it as a terminal event. It should be confirmed that there are no chances for exceptions to be disabled, to rely on this assumption.
There was a problem hiding this comment.
Add a note about care being taken on making sure no drivers disable the safety critical exceptions
|
Superseded by #14 |
In the Safety Architecture working group we are investigating the adoption of runtime verification monitors as a possibity to qualify the Kernel against specific safety claims. This commit: