"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 <[email protected]> wrote: >> 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 -- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
