Re: [seL4] A port to the Raspberry Pi 2?

On Sun, 8 Mar 2015 11:23 Tom Mitchell wrote:

...

On Sat, Mar 7, 2015 at 4:00 AM, Wolfgang Keller wrote:

...

On Sat, Mar 7, 2015 at 6:18 AM, Sebastian Lau wrote:

...

Would a port of seL4 to the raspberry pi 2 be welcome because I'm interested in buying a raspberry pi 2 and building sel4 for it?

I have not much knowledge about seL4, but the boot process of the RPi (all versions) is rather special:

Thanks for the R-Pi summary!

Some layers may be difficult to prove but that should not make it impossible to do good work.

Something along the lines... If Given: uboot is trusted. If Given: USB IO is trusted to devices ...UVW, XYZ.

Obviously, it will not be possible to establish a chain of trust using uboot and USB. If a proof of correctness is the goal, don't even dream of doing it with the Raspberry Pi.

As I already told above: Even if we could trust uboot and some kind of USB stack (IMHO complicated, but perhaps even doable), on RasPi, it's the GPU that controls the CPU (as I told earlier). Thus you also have to trust the firmware blob that contains an own OS running on the GPU that is based on ThreadX. That's why I wrote

Since the ARM core is just a slave to the GPU core which runs a binary blob based on ThreadX, this makes it IMHO very difficult to apply the correctness proof and guarantees of seL4 to the RPi version. If you can relinquish the correctness guarantees of seL4 (the thing that makes seL4 interesting) [...]