[okl4-developer] OKL4 structure questions

[Gernot Heiser]

>>>>> On Fri, 29 May 2009 16:03:04 +0200, Xavier.LANGELLIER at fr.thalesgroup.com said:
XL> Hi,
XL> I have (again) some questions about OKL4 structure:

XL> I asked in a previous mail the difference between cells and address spaces.
XL> Josh answered that in the case off a Linux cell there is one address space
XL> for each program and I don't understand if those address spaces are OKL4
XL> address spaces or Linux address spaces.

Both. Linux address spaces get mapped onto OKL4 address spaces. OKL4
(kernel) address spaces are essentially an abstraction for page tables.

XL> In this mail Josh also said that an address space is associated with exactly
XL> one clist but in the pdf "OKL4 Programming Overview of the OKL4 3.0 API" at
XL> page 54 the diagram shows 3 address spaces in 2 cells and 4 clists. What is
XL> the rule about that point?

That diagram is misleading, apologies.

XL> How to decide between address space and cell isolation for a given
XL> application?

a Secure HyperCell is a high-level abstraction, which is implemented
by using low-level kernel abstractions, including Clists and address
spaces. The system designer should think in terms of the higher-level
constructs. Cells define isolation domains. If multiple processes
exist in such a domain (as is the case in the example of a virtual
machine) then they each get mapped onto a kernel address space, all
typically sharing the same Clist (although sub-domains with further
restricted rights can be set up -- there is much more support for this
in future releases).

XL> I would like to know the status of the kernel proof of correctness.

About a month away from completion.

Gernot