reduce genode TCB

[Norman Feske]

Hello Riju,

> The current secure world has 27539 LOC. The baseline can be
> https://athena.smu.edu.sg/mobisys/backend/mobisys/assets/paper_list/pdf_version/paper_31.pdf,
> which also turned on/off peripherals, rewriting normal world device
> drivers from secure world. It has only about 4K LoC in TCB (section 6 para
> 2 and 3)> ...
> Looking at the .d files in hw_imx53 with sloc, we get the following
> break-down. The bulk of the code is coming from genode OS framework. The
> question I have is:  does the tz_vmm demo minimally use genode components?
> If yes, then maybe this is the best TCB size we can expect? If not, then
> what are some parts that can be cut down?

The number of 27 KLOC is plausible. It may be possible to shave off some
lines here and there. But this won't change the order of magnitude. As a
reference for the complexity of a modern stand-alone microkernel, please
consider the examples of seL4 or NOVA. Each has over 10 KLOC of code
without including any user-level infrastructure.

I'd rather question the value of having components in the first place in
your scenario. If your secure world consists of trusted components only
and has a static feature set, what is the value of componentization? If
there is no untrusted code in the secure world, the microkernel approach
adds costs but no benefits. If so, one way to significantly reduce the
complexity of your current implementation would be to co-locate the
tz_vmm, init, and other custom components with Genode's core. This
approach comes down to using Genode as a mere API, not as an OS. E.g.,
the interaction between components would become mere function calls.

The downside is two-fold: First, the forked implementation deviates from
the regular Genode OS Framework, which implies development effort and
ongoing maintenance costs. Second, it eliminates the modularity and
scalability that the Genode OS Framework gives you.

As soon as 3rd-party device drivers, parsing code, or other forms of
untrusted code enters the picture of the secure world, the microkernel
approach (e.g., the use of Genode) becomes beneficial. Here the static
TCB overhead of around 20 KLOC of the fundamental OS infrastructure
(microkernel and the low-level user-land code) must be accepted, or
alleviated by the means of formal verification as done by the seL4 project.

Cheers
Norman

-- 
Dr.-Ing. Norman Feske
Genode Labs

http://www.genode-labs.com · http://genode.org

Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden
Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth