Gernot:

thanks for the info. There are at least two reasons to try it within TZ:
(1) pure curiosity: can it be done? -- you answered that.
(2) can TZ be used as secure boot for seL4?

Back to your statement:
TZ gives you absolutely nothing you can’t get with just seL4 (eg in hyp mode) and some form of authenticated boot
so, what you refer to as "authenticated boot" has to have some hw support. Clearly, TZ is suitable for that.
TZ is also overkill as it provides many features beyond secure boot. If there is a
commercially available alternative that offers a smaller (minimal?) hw support for secure boot,
we'd like to hear about it.

Cheers,
Gene

======================
Gene Tsudik
Chancellor's Professor of Computer Science
University of California, Irvine
On 3/23/16 11:10 PM, Gernot Heiser wrote:
On 23 Mar 2016, at 6:22 , Norrathep Rattanavipanon <nrattana@uci.edu> wrote:

Is it possible to run sel4 as a secure world OS in TrustZone? 
Has anyone successfully done that before?

I believe we have done that in the past (with platforms where we could just ignore the secure/normal split and ran everything in secure mode). There is no reason why it wouldn’t work, it just comes down to initialising the platform correctly.

My question, though, is why bother? TZ gives you absolutely nothing you can’t get with just seL4 (eg in hyp mode) and some form of authenticated boot. TZ is for people who don’t trust their OS (rightly, because it’s unverified and thus buggy) and somehow believe that hardware is better.

I had this discussion quite a few times recently. On probing, it always came down to the other (a) side not really understanding their threat scenarios, or (b) not understanding what it means for software to be formally verified (or (c) someone understands all this but is working with people in (a), (b)).

Compare the two scenarios:

1) seL4 as the OS in the secure world presumably used to isolate different TEEs that get invoked from normal world. Obviously you also need a TZ monitor to do the switch between worlds securely.

2) Nothing runs in secure world, you (absolutely minimal) TZ monitor only does the minimal platform initialisation and then hands over to seL4 running in hyp mode, and never executes again.

Unless you formally verify your TZ monitor, scenario (1) has the much larger attack surface, i.e. your unverified TZ monitor. So this *reduces* security compared to scenario (2). Unless you verify your TZ monitor, but why bother?

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.