> On Sun, 8 Mar 2015 11:23 Tom Mitchell <[email protected]> wrote: >> >> On Sat, Mar 7, 2015 at 4:00 AM, Wolfgang Keller <[email protected]> >> wrote: >>> >>> On Sat, Mar 7, 2015 at 6:18 AM, Sebastian Lau <[email protected]> >>> 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 [email protected] https://sel4.systems/lists/listinfo/devel
