Re: Fwd: Fwd: [Cryptography] seL4 going open source

On Sat, 2014-06-28 at 10:32 +1000, Gernot Heiser wrote:
> > On Thu, 2014-06-26 at 22:33 -0700, Bill Frantz wrote:
> >> ====== Forwarded Message ======
> >> Date: 6/24/14 6:43 PM
> >> Received: 6/24/14 1:56 PM -0400
> >> From: [email protected] (ianG)
> >> To: [email protected] (Cryptography Mailing List), 
> >> [email protected] (Crypto discussion list)
> >> 
> >> http://sel4.systems/
> >> 
> >> […]
> >> Finally, seL4 is the first (and still only) protected-mode OS kernel
> >> with a sound and complete timeliness analysis. Among others this means
> >> that it has provable upper bounds on interrupt latencies (as 
> >> well as
> >> latencies of any other kernel operations). It is therefore the only
> >> kernel with memory protection that can give you hard real-time guarantees.
> > 
> > I think it is not the only one kernel that can give hard real-time
> > guarantees.
> > 
> > please take a look here http://www.xtratum.org
> 
> I had a look at the XtratuM papers and could not find any indication of it having undergone a sound and complete worst-case execution-time (WCET) analysis. In fact, I have not seen any evidence of *any* protected kernel other than seL4 having undergone such an analysis. If anyone knows of any such system, and can point to any evidence, please let me know.
> 
> For those not familiar with sound WCET analysis, this is a static-analysis approach which examines all possible code paths from an entry point, uses a sound (i.e. conservative) micro-architectural model of the processor pipeline, caches etc to calculate an upper execution-time bound on each such code path, and identifies the longest of those as the WCET. Information on how this was done for seL4 can be found at http://ssrg.nicta.com.au/projects/TS/realtime.pml.
> 
> Having said that, even in the absence of a sound WCET analysis (and without having dug very deep), the claim that XtratuM is suitable for hard real time *in the domain it is designed for* is probably credible. But it needs to be understood that there are pretty fundamental differences between XtratuM and seL4. seL4 is a general-purpose microkernel, designed as a base for almost arbitrary systems. In particular, it provides very general, dynamic resource management. In contrast XtratuM is a simple separation-kernel style hypervisor, which supports only completely static partitioning of time and space. This obviously makes for a much simpler system (also much simpler to analyse, so a WCET analysis should not be hard), but also limits its applicability.
>
> Specifically, XstratuM does a simple round-robin schedule of partitions with a 10ms time slice. The obvious implication is that the worst-case interrupt latency is 10*((n-1)+w)) ms, where n is the number of partitions and w is the WCET of the kernel. Interrupt latencies of the 10s of milliseconds are not acceptable for the majority of hard real-time systems. In contrast, the WCET of seL4 is at least 2 orders of magnitude less (and can probably pushed lower by another OoM with some significant effort, mostly on the verification side).
> 
> Note that a similar “partition scheduler” has been implemented for seL4 as well, in order to produce a military-grade separation kernel configuration that can be argued to be free of covert channels (see the infoflow paper at last year’s S&P linked from http://ssrg.nicta.com.au/projects/TS/infoflow.pml). While standard practice, I consider this approach an expensive and inflexible hack, and we’re working on something better, even for this confidentiality-type separation.
> 
> Also, I don’t want to dodge the fact that seL4 is still quite imperfect as a real-time platform, particularly for mixed-criticality systems (where the “criticality” of a subsystem is orthogonal to its timeliness requirements). We’re working on API improvements that will solve this. These won’t be in the initial open-source release, as the model isn’t finalised yet, but I expect this to happen within the next 12 months.
> 
> Hope this helps to clarify things,
> Gernot


The paper characterizes xtratum as bare-metal hypervisor (not
microkernel or separation kernel). More precisely xtratum is a type 1
hypervisor that uses para-virtualization.

My understanding is that the application domain of xtratum is batch
processing of signals and similar embedded applications, not
general-purpose interative processing.

In such a domain, the round-robin scheduler sounds good.


_______________________________________________
cap-talk mailing list
[email protected]
http://www.eros-os.org/mailman/listinfo/cap-talk