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 <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.



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