[okl4-developer] OKL4 and timer service.

[Gernot Heiser]

>> There are a couple of reasons for OKL4 not externally exposing the timer it
>> uses:
>> 
>> a) Minimality: a guiding principle of microkernel design. Why should the
>> kernel provide a timer service when the same can be done at user level
>> (this assumes that platforms tend to have multiple timer sources, which
>> they generally do nowdays). Additionally, the functionality required by the
>> kernel of the timer is quite minimal: just a repeating hardcoded timeout;
>> for it to provide a useful external service the internal driver would need
>> to be significantly extended beyond the needs of the kernel, also violating
>> the minimality principle.

JD> OK, fair enough. Now OKL4 is capturing a full set of driver for a very minimal
JD> use preventing all cells to use this resource. It is not given that the
JD> platform has another set of timer available (even if this is generally the
JD> case) and beside as  OKL4 is doing the thread scheduling it sounds like it
JD> would be a good place to deal with sleeping threads and such.

A lot of things fall into the category of "it sounds like the kernel
would be a good place for this". That's the general design approach
for a monolithic kernel. The microkernel approach is: "if it doesn't
have to be in the kernel it shouldn't be in the kernel".

>> b) Security: if the kernel provides a time source, then you cannot
>> virtualize time.

JD> Not sure to see how this will be different from using another set of timer
JD> resource.

The difference is that if you put it into the kernel API, it is there
to use. As Josh explained, we don't stop you from adding this
functionality if you think it's useful in your system, but that
doesn't force it to be there in places where it would undermine security.

JD> A timer service is not a time service ...

Anything that gives you information of the passage of real time is a
time source.

>> This not only limits what you can do with virtualization,
>> it makes it much easier to exploit covert timing channels, and makes it
>> impossible to employ some standard approaches to reducing CTC bandwidth.

JD> OK, maybe I am missing something but I am not sure to see how the fact that
JD> OKL4 provides a timer service makes the CTC problem worst than if I manage
JD> another timer myself in an additional Cell. Maybe you could point me to some
JD> literature on the subject.

If you use your platform code to build an insecure system, that's your
choice. If our API makes the system insecure then that's no longer
your choice, and no workaround is possible for such insecurity-by-design.

Gernot