Interesting article. I’d add one more point to Gernot’s:
- seL4 does have a test suite, and the verifiers are very happy about that. :-)
Even though it is proved correct, the proof does have assumptions and you can can validate
those by test. For maintenance, finding simple obvious mistakes can be quick in a
regression test suite, saving you time in verification. The problem with test is just that
you don't know when you have tested enough. That’s what the proof is good at.
Cheers,
Gerwin
On 31.08.2015, at 21:46, Gernot Heiser
<gernot@nicta.com.au<mailto:gernot@nicta.com.au>> wrote:
On 31 Aug 2015, at 19:33 , Jeroen Slim van Gelderen
<askslim@gmail.com<mailto: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.abstr…
- 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<https://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.
_______________________________________________
Devel mailing list
Devel@sel4.systems<mailto:Devel@sel4.systems>
https://sel4.systems/lists/listinfo/devel