Hi again :)
Is it possible to run sel4 as a secure world OS in TrustZone? Has anyone successfully done that before?
Thank you,
On 23 Mar 2016, at 6:22 , Norrathep Rattanavipanon <nrattana@uci.edumailto: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.
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA256
Hi Gernot,
thanks for sharing your thoughts. I am entering the thread here as I my thoughts go into a similar direction. We last year mentored Hesham's GSoC project of porting seL4 to the RISC-V architecture and think in the direction of TEEs for a GSoC this year. In my job I have worked a lot with GP-compliant TEEs the last year and it would be great if you could share your opinions on my thought process.
First of all, RISC-V has four execution levels that are more or less similar to ARM's EL0 to EL3. My starting point for a GP-compliant TEE would naturally be OP-TEE, and of course seL4.
These are the options and my thought process:
* Porting OP-TEE plainly to RISC-V: Would be a nice project, but I would prefer a portable solution. When porting directly, either OP-TEE can serve as SM or more preferably there should be a RISC-V equivalent of ARM-TF.
* Porting OP-TEE on top of seL4: That would be para-virtualizing OP-TEE os. The communication between secure world and non-secure world is mapped to seL4 communication.
* Porting OP-TEE functions as seL4 services: This is maybe actually the best way to handle it. All threading and separation is handled by seL4, Trusted Applications run as seL4 containers with the GP-API, and the services (encrypted storage, crypto functions etc.) are running as seL4 services, too.
* For the latter two, one thing that remains is similar to the original thread question: The non-secure operating systems need to be para-virtualized ideally, right? Or can seL4 currently work as a hypervisor? The question remains is then how the communication between non-secure and secure world is dispatched, or is there something like a lowest exception level secure monitor needed. Sorry, if I overlooked this part until now.
Thanks a lot for your input.
Best, Stefan
- -- Stefan Wallentowitz Staff Engineer
Simless GmbH, Zweigstelle/Branch München Adresse/Address: Freibadstr. 30, 81543 München, Germany Email: stefan@simless.com Web: www.simless.com
Simless GmbH Adresse/Address: Alaunstr. 85, 01099 Dresden, Germany Geschäftsführung/Managing Director: Karsten Ohme Handelsregister/Trage Register: Amtsgericht Dresden HRB 34482 Sitz der Gesellschaft/Head Office: Dresden
Hinweis: Der Inhalt dieser E-Mail ist vertraulich und ausschließlich für den bezeichneten Adressaten bestimmt. Wenn Sie nicht der vorgesehene Adressat dieser E-Mail sein sollten, setzen Sie sich bitte mit dem Absender der E-Mail oder unter der angegebenen Telefonnummer in Verbindung und vernichten Sie diese E-Mail auf Ihren Speichermedien.
Notice: The information contained in this e-mail is confidential. It is intended solely for the addressee named above. If you are not the intended recipient, please notify the sender immediately and destroy this message on any media of yours.
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 mailto: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:
- 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.
- 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.
Hello,
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.
that is a common misconception. TrustZone does not provide a secure-boot mechanism. It is merely a mechanism for running a "secure world" behind the back of the regular "normal-world" OS. The normal world is indeed bootstrapped from the secure world (at least in our TZ monitor implementation [1]). But the secure world must be securely booted as well. The mechanism for doing that depends the SoC vendor. For example, FreeScale i.MX uses a so-called high-assurance boot (HAB) mechanism.
[1] http://genode.org/documentation/articles/trustzone
Best regards Norman
Gernot,
I also had an opinion expressed to me that TZ could be leveraged to speed up some of context switching. No clue whether there is any truth to that.
Aleksey
From: Devel [mailto:devel-bounces@sel4.systems] On Behalf Of Gernot Heiser Sent: Wednesday, March 23, 2016 11:11 PM To: Norrathep Rattanavipanon nrattana@uci.edu Cc: GTS gts@ics.uci.edu; El Defrawy, Karim M kmeldefrawy@hrl.com; devel-request devel@sel4.systems Subject: Re: [seL4] sel4 in TrustZone
On 23 Mar 2016, at 6:22 , Norrathep Rattanavipanon <nrattana@uci.edumailto: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.
On 25 Mar 2016, at 5:44 , Nogin, Aleksey <anogin@hrl.commailto:anogin@hrl.com> wrote:
I also had an opinion expressed to me that TZ could be leveraged to speed up some of context switching. No clue whether there is any truth to that.
that’s complete bogus. Unless, of course, you’re talking in the context of some of the systems out there that take 10 times as long for a context switch as seL4.
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.
-
Gernot Heiser -
GTS -
Nogin, Aleksey -
Norman Feske -
Norrathep Rattanavipanon -
Stefan Wallentowitz