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

Hi, Am 09.03.2015 um 07:25 schrieb Sebastian Lau:

Well, I'll probably start one for a side project (being a student is busy... Not that working is any better). But wouldn't GRUB work as a bootloader as well or is it that sel4 only boots on uboot?

I was going to say that GRUB is x86 only, however googling for "grub bootloader ARM" reveals: https://wiki.linaro.org/LEG/Engineering/Kernel/GRUB so apparently GRUB now also exists for ARM architectures. (Not sure about the usefulness of the mentioned UEFI support in an ARM environment though..). I'd still expect U-boot to be less trouble. Also, U-boot is already being used to boot seL4 on other ARM platforms (e.g. the SabreLite), so it is proven to work.

On Sun, 8 Mar 2015 11:23 Tom Mitchell mailto:mitch@niftyegg.com> wrote:

On Sat, Mar 7, 2015 at 4:00 AM, Wolfgang Keller mailto:wolfgangkeller@gmail.com> wrote:

On Sat, Mar 7, 2015 at 6:18 AM, Sebastian Lau mailto: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.

The value of accepting some "Givens" is that other levels of work can move forward on a very inexpensive platform.

As a student platform the R-Pi is interesting because the student has a worthy (sufficiently interesting) platform to abuse for less than the price of a modern text book. Pop out the memory card reload it and start over. The students laptop has not crashed.

Yes, exactly: it is cheap and a its a worthy target. Robert -- Robert Kaiser Computer Engineering RheinMain University of Applied Sciences