Skip to main content

seL4 on the Raspberry Pi 3

Posted by: Kofi Doku Atuah

February 8, 2017

seL4 on the Raspberry Pi 3

The seL4 kernel is a burgeoning project that’s been creating a buzz in the security world for its uncompromising capability-based security model that comes with end-to-end proofs of conformance to its formal specification. It’s a microkernel, and it’s the fastest of its ilk. It says, “Security is no excuse for poor performance!”, and then backs it up. It’s open source. It’s free. It’s an increasingly relevant disruption in the Operating Systems monolith.

And now it’s on the Raspberry Pi 3. Do you have a Raspberry Pi 3? Then seL4 is now at your fingertips. Here’s how to get your hands on it.

Motivation:

Why was seL4 ported to the Raspberry Pi 3? Why now?

The team recognized that the Raspberry Pi 3 has a keen, intelligent userbase, and in order to promote security-conscious development and get folks practically involved in real world usage of a secure operating system, we decided to pilot a port that would appeal to a wide audience. From students to hardened embedded systems experts, to Linux hobbyists, the Raspberry Pi 3 presents a suitable platform for the growth of people who respect the fact that we live in a world where technology has an increasingly prevalent place in our lives.

That brings along with it both benefits and threats. The new generation of software engineers won’t be working on applications that are just bits and bytes in a computer. They will be writing the software that powers our cars, mobile phones, and machines that must be trusted with our very lives – pacemakers, robotic surgical aids, and nuclear power control systems.

It seems as a society, we haven’t yet fully understood the seriousness of the problem. Why is seL4 on the Raspberry Pi 3 now? Well: now is the critical time to get more developers invested in solid, realistic paradigms for software security. Could there be a better time?

A call to action.

A new, secure, connected world can’t be run without a fully-featured, mature platform. That’s where you come in. seL4 is still young. Can you do contribute? Yes: try seL4 on your Raspberry Pi 3. Tell a friend that it worked, and that they can get their hands on it too. Read our FAQ and understand the basics of our secure capability-based system. Join and follow our mailing list to clarify your understanding. Join our IRC channel and engage us. Ask us the tough questions. We don’t have all the answers, but you can jolt us into thinking about them.

Do you have an idea for a software project based on seL4? Drop us a question. Don’t be a stranger.

Prepare yourself:

The seL4 build dependencies.

There is no silver-tongued way to say, that seL4 has a fairly involved build-dependency set-up procedure. We know it’s tedious, and we’re working on it.

Here’s the simple description: you’ll need a compiler toolchain that can target your platform, and the “Repo” script, which is really just a script released by Google, that is a git submodule-management replacement. We use some Python scripts to generate some headers and our custom bitfield functions, so you’ll need some python modules. Slap on an XML parser which we use to generate our syscall invocation stubs, and ncurses for our “make menuconfig”, and you’re good to go.

Follow the seL4 build-dependencies guide, here. Make sure you don’t omit downloading Google’s “Repo” tool!

Building the seL4-Test project

The seL4 project maintains a unit test project which can be used as both a simple way to determine that you have a fully-functioning build, and to prototype new features in userspace. You can find the seL4-Test project publicly available here.

We’re going to check out a fresh copy of the source and build it. Run the following:

    mkdir sel4test && cd sel4test

    repo init --config-name -u git@github.com:seL4/sel4test-manifest.git

    repo sync

    make rpi3_debug_xml_defconfig && make

Concurrent “make” builds are supported. At the end of this, you should have a build of the seL4 kernel, with the sel4-test framework built as a CPIO payload. The built seL4 kernel image (unstripped) can be found and examined under /build/kernel/. The final images that are meant to be executed are placed in the /images subfolder. The generated seL4 bootable image will have the filename sel4test-driver-image-arm-bcm2837 by default.

Debug output:

You need to connect a serial cable to UART0 on your Raspberry Pi 3, because this is the line on which seL4 dumps its boot log and the line on which seL4-test also dumps the output from all of its tests. The settings should be 115200 baud, 8-N-1 signal bits.

Booting seL4 on your Raspberry Pi 3:

The Raspberry Pi 3 has two convenient ways to get a kernel image onto the board for booting. Using u-boot, you can TFTP-boot seL4, or copy seL4 onto an SD card and boot it from there.

Read through our Raspberry Pi 3 support wiki page. The Raspberry Pi 3 expects there to be an FAT32 partition on the SD card, and it expects certain files with specific filenames to be in the root directory of that partition. Our wiki page gives you links to all the binaries you need, except for the actual u-boot bootloader. Please use our prebuilt U-Boot image since the stock upstream U-Boot won’t boot seL4 out of the box. If you don’t trust prebuilt binaries, then the wiki page provides directions for how to generate the image we supplied from source as well.

You should now have all the following files:

  • bootcode.bin (This is provided via a link on the wiki page).

  • start.elf (This is provided via a link on the wiki page).

  • u-boot.bin (You can either build one of your own, or use our prebuilt image).

  • config.txt (This is provided via a link on the wiki page).

  • sel4test-driver-image-arm-bcm2837 (See Building the seL4-Test project, above).

Copy them all into the root-directory of your FAT32-formatted SD-card, attach your serial cable to see seL4’s output, and power your Raspberry Pi 3 on!

…So what exactly am I seeing here?

You’re seeing the seL4 microkernel booting, and preparing all of the various kernel objects that describe the running system. These objects include, IRQ Controllers, Untyped Memory objects,

RPi3 seL4test
seL4’s test suite (Click for full size)

Address Space ID pools, and so on. Each of these object types represents a resource that can be manipulated and “invoked” through a capability token. Invoking an object through a capability will cause the kernel to perform an action with that object.

 

You then see the seL4 microkernel examine the CPIO archive containing the seL4-test process,

and load it as its first userspace process – the “Root Task” TM. The root task is the parent of all other threads, and it contains the highest level of permissions to access all kernel objects. It can then decide which threads have access to which objects. It achieves this by making (or not making) capabilities to those objects available to those other threads.

To run the tests, the seL4-test parent process takes an “Untyped” object of a certain size, and sub-partitions it into a child-process. It then gives the remainder of that “Untyped” object to the same child process that it created dynamically. This child process will be repeatedly killed and re-created sequentially for each test.

The results of each test-run are sandboxed from the effects of the previous and subsequent test-runs because after each test is executed, the seL4-test parent-process performs a “Recycle” operation on the original “Untyped” object that was used to create the child-test process. This is done in one simple operation, and showcases the strength of the seL4 capability model for allowing strong capability-based security.

Ok, pretty cool: what next?

General:

Well, you now have a running seL4 image in your hands. Do you have a project that has real world consequences for human life? Do you want to move with a responsible choice that respects the criticality of your application, and the security of your users? Security is a difficult, and ever-evolving problem. Come talk to us.

While seL4 doesn’t promise to be the magic bullet, it does promise to be the solid, performant foundation upon which secure, Trustworthy Systems can be constructed, with careful planning, and adherence to good practice, and respect for the strong isolation guarantees that seL4 provides.

Writing applications?

Familiarize yourself with the seL4 capability system and then come ask us questions on IRC about the seL4 userspace libraries. The userspace libraries abstract away a lot of the work involved in creating a running seL4 application. Feel free to ask us questions about your design, and try to understand how to ensure that you extract the benefits of seL4’s security model in your new application.

Writing drivers?

As a microkernel, seL4 drivers are really just userspace threads. The thing that distinguishes a thread as a “driver” is that it handles one or more IRQ objects (because it has a capability to invoke operations on one or more IRQ objects), and it maps in and accesses device registers using some combination of Memory-Mapped I/O, Port-Mapped I/O and Direct Memory Access – all of these also being governed by capabilities.

You’ll need to learn to structure your system such that the correct capabilities are handed down to the correct driver threads. In general, it’s all about using the principle of least privilege: don’t give out capabilities to child threads that aren’t needed for them to accomplish their functional requirements!

19 comments on “seL4 on the Raspberry Pi 3

  1. DM says:

    Nice work!!

    Don’t forget to add a link to this article from the RPI hardware page on the wiki (or copy this there). https://wiki.sel4.systems/Hardware/Rpi3

    Great to see on RPi3. It’s probably the most common hobbyist & arm64 out there, apart from phones. Also one of the most affordable, which is important for students and many open source volunteers. (If only Broadcom would open source the boot too, it’d be even more broadly suitable for high assurance).

    Would be great if there was Genode support for armv8_64 too. 🙂 There’s a thread here if that’s your thing and you have the skills: https://sourceforge.net/p/genode/mailman/message/35566945/. With the road-map ahead for Genode (https://genode.org/about/road-map), it’d be a great way to get hobbyists using seL4 daily in a dynamic, general purpose OS scenario.

    1. Kofi Doku Atuah says:

      Wow — linking this post there is a really good idea that I would have missed: thanks

      EDIT: With regards to AArch64, you might find yourself pleasantly surprised by upcoming developments in the kernel. seL4 is a fast moving target 😉

      1. DM says:

        No worries! Thank you!!

      2. DM says:

        Fast moving indeed. I’ve seen the public road-map and that’s really exciting!

        It’s been a good month for aarch64. OpenBSD & HardenedBSD builds are recently out on RPi3 too. Maybe we’ll even see them running in an seL4 VM on a Genode desktop one day.

        I still dream of QubesOS-like end-user tooling on top of Genode+seL4. Would be great to have that transition path to support secure native components & domains, alongside compartmentalised legacy (mainstream) OSs on other cores. I could see someone porting Wireguard over (VPN in ~4000 loc) too. Maybe even doing things like virtualising CopperheadOS’s hardened Android for better security compartmentalisation with seL4 on mobiles.

        With Robigalia on seL4 and RISC-V processors coming too, there’s real hope on the horizon for the kind of trustworthy systems needed for safety, security assurance and real-world maintenance requirements. (A massive problem with the number of legacy & embedded devices that are buggy, uneconomical to maintain and becoming botnet WOMDs etc under current paradigms) .

        The great work seL4 team’s doing are going to open a lot of architectural options for safer systems.

        Well done to you and your team!

  2. Steve Soloski says:

    Interesting article – but my Pi3 doesn’t boot to seL4. I built the seL4test project, built U-Boot, copied the files to my SD card, powered up the Pi and… got the following:

    Hit any key to stop autoboot: 0
    switch to partitions #0, OK
    mmc0 is current device
    Scanning mmc 0:1…

    USB device 0: unknown device
    Waiting for Ethernet connection… unable to connect.
    missing environment variable: pxeuuid
    missing environment variable: bootfile
    Retrieving file: pxelinux.cfg/01-b8-27-eb-95-a5-5c
    Waiting for Ethernet connection… unable to connect.
    missing environment variable: bootfile
    Retrieving file: pxelinux.cfg/00000000
    Waiting for Ethernet connection… unable to connect.
    missing environment variable: bootfile
    Retrieving file: pxelinux.cfg/0000000
    Waiting for Ethernet connection…

    Any thoughts or things to look at would be most helpful!

    1. Steve Soloski says:

      For anyone else running into this issue – turns out u-boot v2017.3 (and later) hangs after printing out the “Starting application at 0x20000000 …” message. Instead, checkout v2017.1 (or v2016.11), build it and use it instead.
      When booting, press any key to get to the U-Boot prompt. Then manually load and run the sel4test binary:
      fatload mmc 0 ${loadaddr} sel4test-driver-image-arm-bcm2837
      bootelf ${loadaddr}

      You’ll get some CACHE Misaligned operation messages, but then all of the tests run and pass.

      Hope this helps someone!

      1. Kofi Doku Atuah says:

        Good looking out, Steve!

  3. Jesper Frickmann says:

    I cannot get the repo/github to work:

    $ repo init –config-name -u git@github.com:https://github.com/seL4/sel4test-manifest.git

    … A new repo command ( 1.23) is available.
    … You should upgrade soon:

    cp /home/jesper/sel4test/.repo/repo/repo /usr/bin/repo

    Permission denied (publickey).
    fatal: I don’t handle protocol ‘git@github.com:https’

    Please advice, if you have any suggestions – thanks! I am running Ubuntu 15.10 on a Thinkpad T61.

    Jesper

  4. Jesper Frickmann says:

    I got it fixed. I had to set up a SSH key on GitHub. I am a noob, sorry 🙂

  5. Mike says:

    What is the trick to getting seL4 to boot off of the SD card? I’ve followed your guide here and have my RPi3 up and running. After many iterations of “Waiting for Ethernet connection…” I get to a U-Boot prompt. I am not sure where to go from there.

    1. Mike says:

      I ended up following the instructions here: https://wiki.sel4.systems/Hardware/General-ARM#Booting_from_SD_card and made progress with that.

  6. Jesper Frickmann says:

    I need some help, please! I have followed the tips above with fatload and bootelf, and here is what I get:
    ———————————————————————————————————————
    CACHE: Misaligned operation at range [2030c000, 2031c820]
    ## Starting application at 0x20000000 …

    ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4
    paddr=[20000000..2031c81f]
    ELF-loading image ‘kernel’
    paddr=[0..36fff]
    vaddr=[e0000000..e0036fff]
    virt_entry=e0000000
    ELF-loading image ‘sel4test-driver’
    paddr=[37000..427fff]
    vaddr=[10000..400fff]
    virt_entry=1e968
    Enabling MMU and paging

    U-Boot 2017.05-00578-ga375ff8 (May 20 2017 – 08:29:32 -0400)

    DRAM: 944 MiB
    RPI 3 Model B (0xa02082)
    MMC: sdhci@7e300000: 0
    reading uboot.env
    In: serial
    Out: vidconsole
    Err: vidconsole
    Net: No ethernet found.
    starting USB…
    USB0: Core Release: 2.80a
    scanning bus 0 for devices… 3 USB Device(s) found
    scanning usb for storage devices… 0 Storage Device(s) found
    Hit any key to stop autoboot: 0
    switch to partitions #0, OK
    mmc0 is current device
    Scanning mmc 0:1…
    U-Boot>
    ——————————————————————————————————————
    It just restarts u-boot after loading the kernel? My ${loadaddr} is 0x00200000 – is that correct?

    Thanks!
    Jesper

    1. Jesper Frickmann says:

      OK, I may have made some progress. I had left the bootcode.bin and start.elf from Raspbian on the card. When I downloaded the ones that are linked from here, I got to the bug where it hangs after loading the ELF image, reported by Steve above. Tomorrow I will get the older version of u-boot and try again.

  7. Jesper Frickmann says:

    So I ran git reset –hard for the first commit of 2017 and recompiled u-boot. Tried again and got:


    Test suite passed. 218 tests passed.

    218/218 tests passed.
    All is well in the universe.

    Thanks, Steve!

  8. ig says:

    Hey just wanted to give you a quick heads up and let you know
    a few of the pictures aren’t loading properly. I’m not sure why but I think its a
    linking issue. I’ve tried it in two different web browsers and both show the same results.

    1. Kofi Doku Atuah says:

      Could you give some more details? What browser are you using? It seems fine to me

  9. Arthur says:

    Hello, despite I have tried all of the above solutions (U-Boot version and others) I can’t pass the “Starting application at 0x20000000” message error. Can someone helps me, by giving me his files for example? Thanks

    1. Kofi Doku Atuah says:

      Hi Arthur,

      We’ve updated the instructions on the wiki page and included a pre-built U-boot binary file which should successfully load seL4: could you try downloading the pre-built U-Boot binary on this page (https://wiki.sel4.systems/Hardware/Rpi3) and using that? Or if you are so inclined, I guess you could build your own from source using the instructions on the wiki page — either approach should work.

      Please let me know how things go~

      1. Arthur says:

        Hi,

        Sadly, I can’t make this work. I’ve recompiled my kernel, tried using the wiki’s u-boot and even building one following the instructions. Everytime I boot, it hangs at:

        CACHE: Misaligned operation at range [20000000, 20007860]
        CACHE: Misaligned operation at range [20007860, 203d8cc0]
        CACHE: Misaligned operation at range [203d8cc0, 203ec820]
        ## Starting application at 0x20000000 …

        I really want sel4 to work on my system, thanks in advance

Leave a Reply

Your email address will not be published. Required fields are marked with *


*
*