Is the L4-embedded microkernel here means seL4
Dear all, The web page http://ssrg.nicta.com.au/about/#achievements says: !$ All recent Apple iOS devices ship with a <http://www.apple.com/business/docs/iOS_Security_Guide.pdf> security processor controlled by a fork of our L4-embedded microkernel; I wonder whether the L4-embedded microkernel means seL4. thanks Xilong Pei Tongji University 2016/4/14
On Thu, Apr 14, 2016, at 18:23, XilongPei wrote:
I wonder whether the L4-embedded microkernel means seL4
My understanding is that it is a fork of OKL4. I look forward to Gernot writing about this topic on his blog 😉 -- cmr +610481782084 http://octayn.net/
On 14 Apr 2016, at 21:35 , Corey Richardson <corey@octayn.net<mailto:corey@octayn.net>> wrote: On Thu, Apr 14, 2016, at 18:23, XilongPei wrote:
I wonder whether the L4-embedded microkernel means seL4
My understanding is that it is a fork of OKL4. I look forward to Gernot writing about this topic on his blog 😉 There you go: https://microkerneldude.wordpress.com/ 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.
Hi, Google has release its Trusty OS for Android, · An operating system (the Trusty OS) that runs on a processor intended to provide a TEE https://source.android.com/security/trusty/index.html If I replace the Android's Trusty OS with seL4, what should I do, and what benefits can I get? Xilong Pei Tongji University 2016/4/18 发件人: Devel [mailto:devel-bounces@sel4.systems] 代表 Gernot Heiser 发送时间: 2016年4月14日 20:43 收件人: seL4 developers <devel@sel4.systems> 主题: Re: [seL4] Is the L4-embedded microkernel here means seL4 On 14 Apr 2016, at 21:35 , Corey Richardson <corey@octayn.net <mailto:corey@octayn.net> > wrote: On Thu, Apr 14, 2016, at 18:23, XilongPei wrote:
I wonder whether the L4-embedded microkernel means seL4
My understanding is that it is a fork of OKL4. I look forward to Gernot writing about this topic on his blog 😉 There you go: https://microkerneldude.wordpress.com/ 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 Mon, Apr 18, 2016 at 02:08:12PM +0800, XilongPei wrote:
Google has release its Trusty OS for Android,
An operating system (the Trusty OS) that runs on a processor intended to provide a TEE
https://source.android.com/security/trusty/index.html
If I replace the Android's Trusty OS with seL4, what should I do, and what benefits can I get?
You need to take a wider view of what Trusty is, how it fits into Android, and what it provides. Trusty is a "TEE", the OS that runs in the secure world on ARM TrustZone-compatible platforms. See the recent thread about TrustZone and seL4 in general: http://sel4.systems/pipermail/devel/2016-March/000746.html In particular, Trusty is an application on the LK kernel. seL4 here would replace LK, not Trusty. Trusty itself seemingly only provides IPC between "secure" apps and non-"secure" apps (including processes in Linux via virtio and SMCs). To replace Trusty you'd need to implement a Trusty-compatible ABI, convince a bootloader to load seL4 as the TEE OS, and do the appropriate initialization so that the existing Linux driver and apps work. The kernel might need modification to support handling SMCs. As for the benefits, see the FAQ: https://wiki.sel4.systems/FrequentlyAskedQuestions#What_is_formal_verificati... and make your own opinion after inspecting the existing Trusty apps and considering possible system designs. -- cmr +610481782084 http://octayn.net/
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA256 Hi guys, let me shortly note, that we currently evaluate a Google Summer of Code proposal in the lowRISC project where one possible path is to port OP-TEE on top of seL4. Please contact me if you are interested. Cheers, Stefan On 20.04.2016 00:50, Corey Richardson wrote:
On Mon, Apr 18, 2016 at 02:08:12PM +0800, XilongPei wrote:
Google has release its Trusty OS for Android,
An operating system (the Trusty OS) that runs on a processor intended to provide a TEE
https://source.android.com/security/trusty/index.html
If I replace the Android's Trusty OS with seL4, what should I do, and what benefits can I get?
You need to take a wider view of what Trusty is, how it fits into Android, and what it provides.
Trusty is a "TEE", the OS that runs in the secure world on ARM TrustZone-compatible platforms. See the recent thread about TrustZone and seL4 in general:
http://sel4.systems/pipermail/devel/2016-March/000746.html
In particular, Trusty is an application on the LK kernel. seL4 here would replace LK, not Trusty.
Trusty itself seemingly only provides IPC between "secure" apps and non-"secure" apps (including processes in Linux via virtio and SMCs).
To replace Trusty you'd need to implement a Trusty-compatible ABI, convince a bootloader to load seL4 as the TEE OS, and do the appropriate initialization so that the existing Linux driver and apps work. The kernel might need modification to support handling SMCs.
As for the benefits, see the FAQ:
https://wiki.sel4.systems/FrequentlyAskedQuestions#What_is_formal_veri fication.3F
and make your own opinion after inspecting the existing Trusty
apps and considering possible system designs.
-----BEGIN PGP SIGNATURE----- Version: GnuPG v2 iQEcBAEBCAAGBQJXFySeAAoJENZAHP84beGSNe4IAI6b5iwUujWWRgLbC1HcWYaU HBgC7xdz1DvklQhke1pJFPXEv2cdYk0RLDvAdck1d/8/46fC9IGrd4ZYBMf9PzsP RS21WQy+F3qQKSMj41/TcUEFQyc+47cwhYqPe+i6uadp7sJn/T9kYolSZ4ySOJPY 1H+nAseC1NQ4EZSSD+IDrNkcCZesnH6VUgHxsD4YyX85IXu9WiG+Y8igIzuBEsQT zu8880J9v/y7sKFTwy186LQMCj6XHHKiHrbWybwzpNv6nxJvsIErJXkaGbxm2wZQ xrGL8ZGfOhgYwNykmw3VgDnnwBioT4SK49MIKNrxPbdvwiQj93rCFmJC6l4li4o= =owvV -----END PGP SIGNATURE-----
participants (4)
-
Corey Richardson -
Gernot Heiser -
Stefan Wallentowitz -
XilongPei