A port to the Raspberry Pi 2?

older
docker compatible? (was Re: MySQL...

Sebastian Lau

7 Mar 2015 7 Mar '15

4:18 p.m.

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?

Attachments:

attachment.html (text/html — 151 bytes)

Show replies by date

Wolfgang Keller

7 Mar 7 Mar

11 p.m.

On Sat, Mar 7, 2015 at 6:18 AM, Sebastian Lau 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: On Raspberry Pi, it's not the ARM core that boots, but the GPU starts executing a bootloader that is stored in ROM. At that moment SDRAM and the ARM core is disabled. The first stage bootloader's only purpose is reading bootcode.bin from the SD card into the L2 cache. The 2nd stage bootloader (boot/bootcode.bin) also runs on the GPU. Its purpose is enabling the SDRAM and loading the GPU firmware (in most cases boot/start.elf). This is a OS in itself based on ThreadX running on the GPU and thus a large binary blob. It reads a few settings, enables the ARM core and starts it executing boot/kernel.img. Only from this point on, Linux starts booting. I hope I don't have to mention that the instruction set itself for start.elf is not documented... References: http://wiki.beyondlogic.org/index.php?title=Understanding_RaspberryPi_Boot_P... http://www.raspberrypi.org/forums/viewtopic.php?f=63&t=6685 http://raspberrypi.stackexchange.com/a/10595/9138 (a little outdated, now loader.bin is not used anymore) 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), I think porting seL4 to the RPi2 should be in principle doable. But please correct me, if I'm wrong.

Robert Kaiser

8 Mar 8 Mar

6:48 a.m.

Am 07.03.2015 um 13:00 schrieb Wolfgang Keller:

...

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

On Raspberry Pi, it's not the ARM core that boots, but the GPU starts executing a bootloader that is stored in ROM. At that moment SDRAM and the ARM core is disabled. The first stage bootloader's only purpose is reading bootcode.bin from the SD card into the L2 cache.

The 2nd stage bootloader (boot/bootcode.bin) also runs on the GPU. Its purpose is enabling the SDRAM and loading the GPU firmware (in most cases boot/start.elf). This is a OS in itself based on ThreadX running on the GPU and thus a large binary blob. It reads a few settings, enables the ARM core and starts it executing boot/kernel.img. Only from this point on, Linux starts booting. I don't think bootstrapping would be that much of a problem. The trick would be to provide a kernel.img that contains U-boot instead of Linux at this point. Once U-boot is in control, it should be possible to boot seL4 with it. AFAIK, there is support in mainline U-boot for the Raspberry Pi already.

...

I hope I don't have to mention that the instruction set itself for start.elf is not documented...

References:

http://wiki.beyondlogic.org/index.php?title=Understanding_RaspberryPi_Boot_P... http://www.raspberrypi.org/forums/viewtopic.php?f=63&t=6685 http://raspberrypi.stackexchange.com/a/10595/9138 (a little outdated, now loader.bin is not used anymore)

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), I think porting seL4 to the RPi2 should be in principle doable.

IMHO, the biggest problem with the Raspberry Pi is that most of its I/O (even the NIC) is connected through USB. A serial port is available (albeit without level shifters). So, running the seL4test should be possible without a USB stack, but as soon as you want to access a keyboard, network or filesystem, you'll need one. @Sebastian: I had a plan of porting seL4 to Rasperry Pi myself whenever I find the Time (TM), so I'd be more than happy if you could do this. My plan was to look at the Fiasco.OC kernel from Dresden: it does support the Raspi, so it may helpful to look at that code. Robert

...

But please correct me, if I'm wrong.

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

-- Robert Kaiser Computer Engineering RheinMain University of Applied Sciences

Tom Mitchell

9:20 a.m.

On Sat, Mar 7, 2015 at 4:00 AM, Wolfgang Keller wrote:

...

On Sat, Mar 7, 2015 at 6:18 AM, Sebastian Lau 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. 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. There is an old adage that to work on a car at home you need to have a second car available to go and get parts. With the R-Pi spare flash memory cards and USB memory give that spare vehicle to go and get parts.... Have fun. -- T o m M i t c h e l l

Sebastian Lau

9 Mar 9 Mar

5:25 p.m.

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? On Sun, 8 Mar 2015 11:23 Tom Mitchell wrote:

...

On Sat, Mar 7, 2015 at 4:00 AM, Wolfgang Keller wrote:

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

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.

There is an old adage that to work on a car at home you need to have a second car available to go and get parts. With the R-Pi spare flash memory cards and USB memory give that spare vehicle to go and get parts....

Have fun.

-- T o m M i t c h e l l _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Tom Mitchell

6:43 p.m.

The boot loader of choice on the Raspberry Pi is non trivial. https://thekandyancode.wordpress.com/2013/09/21/how-the-raspberry-pi-boots-u... http://elinux.org/RPi_U-Boot#Raspberry_Pi_Foundation_Tools So one strategy is to use the bootloader as it is now and replace the kernel (sel4) and friends that it loads. By building a working bootstrap chain you will have a handle for all the moving parts. Then decide what to change... On Sun, Mar 8, 2015 at 11:25 PM, Sebastian Lau wrote:

...

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?

On Sun, 8 Mar 2015 11:23 Tom Mitchell wrote:

...
On Sat, Mar 7, 2015 at 4:00 AM, Wolfgang Keller
...
wrote:

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

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.

There is an old adage that to work on a car at home you need to have a second car available to go and get parts. With the R-Pi spare flash memory cards and USB memory give that spare vehicle to go and get parts....

Have fun.

-- T o m M i t c h e l l _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

-- T o m M i t c h e l l

Robert Kaiser

10 Mar 10 Mar

8:10 a.m.

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

Wolfgang Keller

8:28 a.m.

...

On Sun, 8 Mar 2015 11:23 Tom Mitchell wrote:

...
On Sat, Mar 7, 2015 at 4:00 AM, Wolfgang Keller wrote:

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

Tim Newsham

9:43 a.m.

"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 wrote:

...

...
On Sun, 8 Mar 2015 11:23 Tom Mitchell wrote:

...
On Sat, Mar 7, 2015 at 4:00 AM, Wolfgang Keller wrote:

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

-- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com

Tom Mitchell

11:40 a.m.

On Mon, Mar 9, 2015 at 3:43 PM, Tim Newsham wrote:

...

"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 :)

This I like... GPU hardware is underutilized in many contexts. There is also the old school OS model where the operating system lived on an IO channel processor. Build the entire system Gentoo style and have at it. I mention Gentoo because nearly all the bits are in motion and handy to inspect and change. I may have to try "emerge world" and see how long it takes a Pi to bake a new set of bits. But that is not a sel4 topic.... -- T o m M i t c h e l l

3541

Age (days ago)

3544

Last active (days ago)

List overview

Download

9 comments

5 participants

participants (5)

Robert Kaiser
Sebastian Lau
Tim Newsham
Tom Mitchell
Wolfgang Keller