seL4 on the Raspberry Pi 3
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.
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 or contact us some other way. 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.
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.
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 -u https://github.com/seL4/sel4test-manifest.git repo sync mkdir build-rpi && cd build-rpi ../init-build.sh -DPLATFORM=rpi3 -DBAMBOO=TRUE -DAARCH32=TRUE ninja
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-rpi/kernel/. The final images that are meant to be executed are placed in the build-rpi/images subfolder. The generated seL4 bootable image will have the filename sel4test-driver-image-arm-bcm2837 by default.
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 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 support 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 support page).
start.elf(This is provided via a link on the support 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 support 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,
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?
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.
Familiarize yourself with the seL4 capability system and then come ask us questions on Mattermost 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.
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!