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