Re: [cap-talk] Public Release of seL4: a formally verified
Viswanathan, Kapaleeswaran (HP Labs India)
A microkernel is an OS kernel which is kept as small as possible, only providing the minimal mechanisms for securely managing hardware. They constitute an approach to minimising the trusted computing base (TCB) and microkernel-based OS design is really part and parcel of taking POLA seriously.
L4 microkernels are typically around 10 kLOC, and seL4 (9 kLOC) is no exception. This makes them three orders of magnitude smaller than mainstream OS kernels, and enables systems with a TCB of less than 20 kLOC.
<<
I am not an expert in the kernel land. I only have an intermediate exposure to it -- only theoretical knowledge. But, I have dabbled in the formal verification domain for a bit more than a year (Z and Possum tool for cryptography protocol verification).
With this background, I would like to comment on the above attempt at definition. I am a bit uncomfortable with it because from a formal verification point of view, which has a meta-language that includes words like objectives, states, functions, and state transitions. The above assumption tries to informally map the number of lines of code to the number of functions and states -- I am not sure how helpful this assumption may be with respect to formal verification.
The Wiki page for Mach OS has a nice pictorial depiction for microkernel: it does memory management, IPC, and task scheduling but nothing more. In the Mach OS language there is microkernel and applications (like browsers, file systems, device drivers, and so on). If we assume Intel's ring architecture for segregating instructions to the microprocessor (Level 0 contains Level 1 contains Level 2 contains Level 4 -- Level 0 functions have access to the entire instruction set supported by the microprocessor), we can say what is the smallest set of OS functions that must be in Level 0? That smallest set of functions should be called micro-kernel.
Would you agree with this alternative approach to formally defining micro-kernels?
Kapali Viswanathan
Research Scientist, HPL India
http://www.hpl.hp.com/people/kapali/
Knowledge may be some model of things that are visible to intellect. Wisdom may be something that includes even those that are invisible.
------------------------------
Message: 6
Date: Thu, 3 Mar 2011 21:10:04 +1100
From: Gernot Heiser <ger...@nicta.com.au>
Subject: Re: [cap-talk] Public Release of seL4: a formally verified
capability-based microkernel
To: "cap-...@mail.eros-os.org" <cap-...@mail.eros-os.org>
Message-ID: <D37C7205-651C-4DD8...@nicta.com.au>
Content-Type: text/plain; charset="us-ascii"
> I have always wanted to ask about a this strange thing: does NICTA distinguish between the terms:
> - microkernel
> - (OS) kernel
> - operating system
> ?
>
> This is strange carelessness compared to rigorousness required for formal verification.
>
> One thing is to verify a nice microkernel and completely another thing is to claim
> that you have a proved correctness of an operating system.
This and a couple other postings indicate some confusion about terminology. Let me try to explain...
High-level summary: a *kernel* is a part of an *operating system*, and *microkernel* is a subclass of *kernel*, and our use of terminology was accurate.
In detail:
An operating *system* is more than a kernel. In OS lingo, "kernel" usually refers to the part of the system which operates in the processor's privileged mode. The complete system contains additional services operating outside the kernel (i.e. un unprivileged, or "user" mode). This division exists in all OSes I know. In Linux, for example, the kernel binary is compiled from a code base of about 10 MLOC, but there are lots of other components which make up the OS, in particular various system "demons" (or "root servers").
A microkernel is an OS kernel which is kept as small as possible, only providing the minimal mechanisms for securely managing hardware. They constitute an approach to minimising the trusted computing base (TCB) and microkernel-based OS design is really part and parcel of taking POLA seriously.
L4 microkernels are typically around 10 kLOC, and seL4 (9 kLOC) is no exception. This makes them three orders of magnitude smaller than mainstream OS kernels, and enables systems with a TCB of less than 20 kLOC.
I (or to my knowledge anyone else in the NICTA ERTOS team) have never claimed we have "proved correctness of an operating system". We have proved functional correctness of an OS *kernel*, namely the seL4 microkernel.
An important aspect is that verification of the kernel cannot be subdivided: as it is running in privileged mode, any part of the code can potentially interfere with any other part, there is no way to enforce internal interfaces inside the kernel. However, once the kernel is verified, its (now trustworthy) mechanisms *can* be used to enforce interfaces between other (system or app) components. This makes it possible to verify user-level components (on top of the verified kernel) in isolation, and still obtaining guarantees about their behaviour. Which is what we are working on now.
I hope this helps to resolve any confusion.
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.
------------------------------
Message: 7
Date: Thu, 3 Mar 2011 21:22:53 +1100
From: Gernot Heiser <ger...@nicta.com.au>
Subject: Re: [cap-talk] Public Release of seL4: a formally verified
capability-based microkernel
To: "General discussions concerning capability systems."
<cap-...@mail.eros-os.org>
Message-ID: <F11F1CF9-1C22-414A...@nicta.com.au>
Content-Type: text/plain; charset="us-ascii"
Apologies for the (almost) duplicated posting. I wasn't subscribed when I posted the first mail. When after about 30h it didn't appear (and I hadn't received a "waiting for moderator approval" message), I assumed that the list quietly discards postings by non-members. So I subscribed and tried again, and then both versions appeared.
Looks like an interesting case of a protection system with memory. I don't think you can model this with caps ;-)
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.
------------------------------
_______________________________________________
cap-talk mailing list
cap-...@mail.eros-os.org
http://www.eros-os.org/mailman/listinfo/cap-talk
End of cap-talk Digest, Vol 84, Issue 5
***************************************
_______________________________________________
cap-talk mailing list
cap-...@mail.eros-os.org
http://www.eros-os.org/mailman/listinfo/cap-talk
Gernot Heiser
>>>>> Gernot Heiser wrote:
> A microkernel is an OS kernel which is kept as small as possible, only providing the minimal mechanisms for securely managing hardware. They constitute an approach to minimising the trusted computing base (TCB) and microkernel-based OS design is really part and parcel of taking POLA seriously.
>
> L4 microkernels are typically around 10 kLOC, and seL4 (9 kLOC) is no exception. This makes them three orders of magnitude smaller than mainstream OS kernels, and enables systems with a TCB of less than 20 kLOC.
>
> [...]
>
> With this background, I would like to comment on the above attempt at definition. I am a bit uncomfortable with it because from a formal verification point of view, which has a meta-language that includes words like objectives, states, functions, and state transitions. The above assumption tries to informally map the number of lines of code to the number of functions and states -- I am not sure how helpful this assumption may be with respect to formal verification.
The above was not meant to be a formal definition of a microkernel. It was meant to help OS non-experts to understand what we mean with those terms.
In fact, I don't think you can formally define the concept of a microkernel (not until people agree what's "minimal" in terms of kernel functionality). But there's no reason why you need a formal definition. We verified a kernel, which happened to be a microkernel (or rather had to be, in order to make the problem tractable, but it's also enough to use a component approach to verifying the rest of the TCB).
> The Wiki page for Mach OS has a nice pictorial depiction for microkernel: it does memory management, IPC, and task scheduling but nothing more.
Do you refer to wikipedia? The Mach wikipedia page doesn't have a picture. What you describe matches the picture on the Microkernel wikipedia page. (Which I did based on the one I have been using in teaching for 15 years, although it ended up slightly wrong when someone reformatted it, never bothered to fix it.)
> In the Mach OS language there is microkernel and applications (like browsers, file systems, device drivers, and so on). If we assume Intel's ring architecture for segregating instructions to the microprocessor (Level 0 contains Level 1 contains Level 2 contains Level 4 -- Level 0 functions have access to the entire instruction set supported by the microprocessor), we can say what is the smallest set of OS functions that must be in Level 0? That smallest set of functions should be called micro-kernel.
That isn't very formal, unless you formally define "smallest". Small with respect to function points, to LOC, to # instructions? Is it no longer a microkernel if I insert a bit of extra code to optimise a commonly-used path? Etc, etc. I don't think you'll get very far that way...
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.
_______________________________________________