"Thus you also have to trust the firmware blob that contains an own OS running on the GPU that is based on ThreadX. "
A more advanced and fun project might be to port seL4 to the GPU :)
On Mon, Mar 9, 2015 at 11:28 AM, Wolfgang Keller wolfgangkeller@gmail.com wrote:
On Sun, 8 Mar 2015 11:23 Tom Mitchell mitch@niftyegg.com wrote:
On Sat, Mar 7, 2015 at 4:00 AM, Wolfgang Keller wolfgangkeller@gmail.com wrote:
On Sat, Mar 7, 2015 at 6:18 AM, Sebastian Lau sebastianlau25@gmail.com 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) [...]
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel