sel4 in TrustZone - Devel - lists.sel4.systems

newer
Porting Qubes OS to seL4 project

sel4 in TrustZone

older
(simple?) build error?

Norrathep Rattanavipanon

23 Mar 2016 23 Mar '16

6:22 a.m.

Hi again :) Is it possible to run sel4 as a secure world OS in TrustZone? Has anyone successfully done that before? Thank you, -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

Attachments:

attachment.html (text/html — 413 bytes)

Reply

Sign in to reply online Use email software

Show replies by date

Gernot Heiser

24 Mar 24 Mar

5:10 p.m.

On 23 Mar 2016, at 6:22 , Norrathep Rattanavipanon 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: 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.

Reply

Sign in to reply online Use email software

Stefan Wallentowitz

9:20 p.m.

New subject: TEE and seL4, was: sel4 in TrustZone

-----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. -----BEGIN PGP SIGNATURE----- Version: GnuPG v2 iQEcBAEBCAAGBQJW879wAAoJENZAHP84beGSn44H/ipV3sA1uqLd7hLQcHcqmMW6 9d1VE77DkKl319s3pkmKPkZQG1OdyvmBS9WT2FNEbelKlREkW24aN5kpK8pY+C8l /15moC4PVA3f03K3iUWfFyvLysx4P2t8BrF6gnaV7n7LjaiUAkd5z3hSS9oO3HSI fkuGtKuNI4AtbhIkvJcDERtPWJUV6uvV7HBFaEBCjhWGpyqMhzTzfP8mI7R5VzcS JvZmlUcPTZoDEZpXxtVYMTl60IEzdDPTwby3HEw8rBezJrkZ6PsICnGEq1x96p1F 3GGC+sasfWpMiYwBi7AFwXgpXQyC7qmdoLtjYAH6DcigxJZFsil1XqfXq96uYvQ= =QIEM -----END PGP SIGNATURE-----

Reply

Sign in to reply online Use email software

GTS

25 Mar 25 Mar

2:20 a.m.

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

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: 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 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:

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.

Reply

Sign in to reply online Use email software

Norman Feske

27 Mar 27 Mar

6:40 p.m.

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 -- 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

Reply

Sign in to reply online Use email software

Nogin, Aleksey

25 Mar 25 Mar

5:44 a.m.

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 Cc: GTS ; El Defrawy, Karim M ; devel-request Subject: Re: [seL4] sel4 in TrustZone On 23 Mar 2016, at 6:22 , Norrathep Rattanavipanon 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: 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.

Reply

Sign in to reply online Use email software

Gernot Heiser

26 Mar 26 Mar

5:52 p.m.

On 25 Mar 2016, at 5:44 , Nogin, Aleksey mailto: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.

Reply

Sign in to reply online Use email software

3189

Age (days ago)

3194

Last active (days ago)

Download

6 comments

6 participants

tags

participants (6)

Gernot Heiser
GTS
Nogin, Aleksey
Norman Feske
Norrathep Rattanavipanon
Stefan Wallentowitz