On 31 Aug 2015, at 19:33 , Jeroen Slim van Gelderen <
askslim@gmail.com> wrote:
In seL4, capabilities are used to refer to blocks of memory. You can delegate access to parts of your address space simply
by passing the capability to another process. You can also implement nested processes, by providing them with only the capabilities to talk to you. Memory in seL4 is typed. For example, some memory regions hold capabilities; to preserve the unforgeable guarantee,
they can only be modified by the microkernel. On boot, the kernel reserves some memory for itself and then delegates the remainder of the memory to a process as an untyped memory (UM) capability. -- http://www.informit.com/articles/article.aspx?p=1994798
Thanks for the pointer to this article, I hadn’t seen it.
It has a lot of informed content, but also some some confusion, so take it with a grain of salt.
Among the things I noticed:
- this is the first time I hear about doubling access-rights check in Mach being a major issue. Maybe it was, but it hasn’t figured in the literature or discussions with Jochen Liedtke. Other comments about Mach I can confirm.
- I have no idea where this factor 25 comes from: "The numbers produced by NICTA indicate that it costs around 25 times as much to develop a system this way as to develop one with no verification, testing, or QA.” OK, writing an OS with “cat >”
is going to be faster, but also utterly useless, so what’s the point? Our more detailed analysis paints a completely different picture: we’re a factor 2–3 *cheaper* than traditional "high-assurance” software (which still has no guarantee of correctness), and
a factor 2–4 more expensive than traditional low-assurance software (which doesn’t even pretend to make any claims of correctness). For details, check the peer-reviewed literature:
https://ssrg.nicta.com.au/publications/nictaabstracts/Klein_AEMSKH_14.abstract.pml
- the comments about preemtability (or not) miss the point. The continuation-passing style is a result of seL4 being an event-based design (as opposed to the traditional process-oriented L4 kernels), a decision which was made *before* any thought
of verification (to reduce memory usage) but turned out to be an enabler. The mechanism for achieving good interrupt latencies are preemption points, which aren’t new, the UNSW L4/MIPS kernel had them 18 years ago. See
ttps://ssrg.nicta.com.au/publications/nictaabstracts/Elphinstone_Heiser_13.abstract.pml for
details.
- TrustZone actually adds *nothing* that can’t be achieved with just seL4. Its continued existence is a result of established players not wanting to change their (broken) security model.
Gernot
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.