On 14 Jun 2017, at 13:54, Jonathan C Day <imipak@yahoo.commailto:imipak@yahoo.com> wrote:
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?
I use the term “trustworthiness” as defined by Verissimo et al, Intrusion-tolerant architectures: Concepts and design, 2003 (https://repositorio.ul.pt/bitstream/10451/14253/1/03-5.pdf):
“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 have absolutely no doubt SEL4 will retain all the provable integrity ever claimed (by anyone involved), but this experimental-proto-main branch confuses me on what fundamentally changes.
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.
Gernot