MadMode

Dan Connolly's tinkering lab notebook

Making Secure IoT: seL4 on my Raspberry Pi 3B

I got seL4 running on my Raspberry Pi 3B tonight.

Even though I worked with Dale Dougherty in the early '90s, I've been on the sidelines of the whole maker thing until September when Micro Center bundled a Google AIY VOICE KIT with Raspberry Pi 3B for $35.

AIY Kit

After I verified that it works as a voice device, I remembered the tantalizing seL4 on the Raspberry Pi 3 item from early this year. The build dependencies were greatly simplified by the seL4 dockerfiles. Building the seL4-Test project went without a hitch:

mkdir sel4test && cd sel4test
repo init --config-name -u git@github.com:seL4/sel4test-manifest.git
repo sync
make rpi3_debug_xml_defconfig && make
...
[GEN_IMAGE] sel4test-driver-image-arm-bcm2837

The only way to see the seL4 test project do its thing is via the serial console. Before I overwrote the working voice kit SD card, I wanted to test connectivity. I have plenty of experience with RS-232 serial cables (I even had a job in high school where I helped a tech by putting together serial terminal cables) but RS-232 vs. TTL serial is not just a matter of wires and connectors; the voltage levels are different. USB to TTL cables usually go for around $15, which is more than half of what I paid for the Pi!

Meanwhile, this summer Micro Center had a beaglebone green wireless, which usually goes for around $50, on clearance for $20, and I couldn't pass it up. The beaglebone uses the same TTL levels and works fine as an ssh server, so I put together a cable

IMG_20171106_212900488

After some config-pin tinkering, I confirmed that I could get UART1 and UART2 on the beaglebone to talk to each other (UART0 is debug outputonly), but I couldn't get any console output from the Pi to show up.

After discovering a JBtek Raspberry Pi USB to TTL Serial Cable on Amazon for $7, I ordered it and set the project aside.

That didn't work either until I connected an HDMI monitor and keyboard and used raspi-config to enable the serial console. I wonder if the beaglebone would have worked given that fix.

With serial console hardware issues in hand, I loaded the SD card as instructed. The first few boot stages worked, but I struggled to Hit any key to stop autoboot. Minicom (remember minicom?) showed "Offline" so I turned off hardware flow control. Bingo:

U-Boot> fatls mmc 0
    50248   bootcode.bin
  2818372   start.elf
       35   config.txt
   393408   u-boot.bin
  4064956   sel4test-driver-image-arm-bcm2837
U-Boot> fatload mmc 0 0x100000 sel4test-driver-image-arm-bcm2837
reading sel4test-driver-image-arm-bcm2837
4064956 bytes read in 328 ms (11.8 MiB/s)
U-Boot> bootelf 0x100000
...
Test suite passed. 119 tests passed. 42 tests disabled.
All is well in the universe