14 Apr
2016
14 Apr
'16
10:23 a.m.
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
14 Apr
14 Apr
1:35 p.m.
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/
2:43 p.m.
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.
18 Apr
18 Apr
8:08 a.m.
New subject: 答复: Is the L4-embedded microkernel here means seL4
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(a)sel4.systems>
主题: Re: [seL4] Is the L4-embedded microkernel here means seL4
On 14 Apr 2016, at 21:35 , Corey Richardson <corey(a)octayn.net
<mailto:corey@octayn.net> > wrote:
On Thu, Apr 14, 2016, at 18:23, XilongPei wrote:
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.
I wonder whether the L4-embedded microkernel means
seL4
20 Apr
20 Apr
12:50 a.m.
New subject: Android TEE OS with seL4? (was: Is the L4-embedded microkernel here means seL4)
On Mon, Apr 18, 2016 at 02:08:12PM +0800, XilongPei wrote:
Google has release its Trusty OS for Android,
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_verificat…
and make your own opinion after inspecting the existing Trusty apps and
considering possible system designs.
--
cmr
+610481782084
http://octayn.net/
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? 
8:41 a.m.
New subject: Android TEE OS with seL4?
-----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:
and make your own opinion after inspecting the existing Trusty
On Mon, Apr 18, 2016 at 02:08:12PM +0800, XilongPei
wrote:
fication.3F
Google has release its Trusty OS for Android,
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 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? 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-----
2262
days inactive
2268
days old
5 comments
4 participants
participants (4)
-
Corey Richardson -
Gernot Heiser -
Stefan Wallentowitz -
XilongPei