Dear all,
The first of these terms has an... interesting history. In a nutshell, it's not always used appropriately. Clearly that's not going to be the case with SEL4, but what exactly is meant?
“Trustworthiness: the measure in which a component, subsystem or system, meets a set of properties (functional and/or non-functional).”
Mixed critical is another term that I'm cautious over. It's not completely clear to me if the mixing refers to relaxed constraints for utilisation reasons or something else.
Mixed-criticality is a well-established term, see
https://en.wikipedia.org/wiki/Mixed_criticality. In a nutshell, criticality refers to the severity of failure, an MCS is a system where
functions of different criticality are co-located and potentially interact, with a requirement that the correct operation of a highly-critical function must not depend on any assumptions on the behaviour of less-critical functions.
This is precisely what we mean with MCS support.
(Correct me if I'm mistaken, but I don't think SEL4 implements FLASK, which would be the obvious way to provide differing constraints, relaxed constraints within the trusted computing model. It's totally the wrong level.)
I assume you’re referring to FLASK = Flux Advanced Security Kernel, a model which was originally implemented in the Flux microkernel and later in SELinux. That is a particular security policy framework that is much higher-level than seL4 primitives, but you
can certainly implement it on top of seL4.
But note that neither the original FLASK, nor SELinux, is *trustworthy* in the above sense, as they are large, unverified code bases that you can safely assume to contain plenty of bugs.
I don’t think I understand. We made no claim that the MCS branch is “trustworthy”, in fact, the announcement explicitly pointed out that it may contain bugs. But I did indicate that it is undergoing verification, which will establish its trustworthiness.
Until then, our trustworthy kernel is the verified mainline seL4.
The MCS claim I certainly stand by.