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_verificat…
and make your own opinion after inspecting the existing Trusty apps and
considering possible system designs.
--
cmr
+610481782084
http://octayn.net/