cancel
Showing results for 
Show  only  | Search instead for 
Did you mean: 

Partner: Port seL4 to Xilinx Zynq UltraScale+ MPSoC for Extreme Hardware Security

xtech-blogs
Xilinx Employee
Xilinx Employee
0 0 1,048

Editor’s Note: This content is contributed by Robert VanVossen, seL4 Technical Lead at DornerWorks

 

seL4 is a formally verified microkernel that was built with security and performance in mind. It is a very attractive software solution for projects that have rigorous security and/or safety requirements. While seL4 is a great option, one of the drawbacks is that there is less built around it than other, more mature solutions, such as a traditional OS. For example, seL4 doesn’t work on that many platforms, and it doesn’t have many drivers developed.

DornerWorks is trying to mitigate this by building up the ecosystem around seL4 and giving developers the tools they need to use seL4 for their systems. One way we are building up this ecosystem is by porting seL4 to more platforms that can really take advantage of its benefits.

 

Zynq UltraScale+ MPSoC

The Zynq® UltraScale+™ MPSoC has a quad-core Arm® Cortex®-A53 processor, a dual-core Cortex-R5F, a GPU, and programmable logic. This device is Xilinx’s most secure solution yet, with features like Secure Boot, Xilinx Memory Protection Unit (XMPU), and Xilinx Peripheral Protection Unit (XPPU). With these features, the Zynq UltraScale+ MPSoC is a great match for the seL4 microkernel. These secure hardware components provided by Xilinx and the formally verified seL4 microkernel pair together well by ensuring that the hardware and software collaborate in the overall security story. On top of that, it also provides the Arm virtualization extensions.

This support allows seL4 to be run as a hypervisor, which is another means to reinforce the budding seL4 ecosystem, by allowing guest operating systems to run on top of seL4.

 

Porting Effort

To port seL4 to a new platform, we needed to make modifications to the following repositories:

  • seL4 – The microkernel itself. Requires platform support of register map and interrupts.
  • seL4_tools – Provides tools to build and boot seL4 projects.
  • util_libs – OS independent utility libraries. The most important for our port was libplatsupport, which provides interfaces for interacting with drivers.
  • seL4_libs – Main Libraries for working with seL4. The most important piece for our port was libsel4platsupport, which is a wrapper around libplatsupport specificially for seL4.
  • sel4test – Test application that is used for regression testing. Defconfigs are implemented here for the various platforms.

 

seL4 already worked on the previous generation Zynq platform, the Zynq-7000 SoC. We used this platform as a starting point for our work on the Zynq UltraScale+ MPSoC. The Zynq-7000 SoC has some of the same peripherals as the Zynq UltraScale+ MPSoC, which made the porting effort a little easier.

seL4 structure, courtesy of Gernot Heiser, DATA61seL4 structure, courtesy of Gernot Heiser, DATA61

 

Some of the files that were originally in a platform folder for the Zynq-7000 SoC were moved to a machine folder for the common Zynq machine, a designation that houses a single copy of the drivers for peripherals common to both the Zynq 7000 and the Zynq UltraScale+ MPSoC.

But, we had to be very careful with this practice because there were some subtle differences, such as the TTC timers having a different register width between the two platforms. Also, some register base addresses and interrupt numbers differed between the platforms as well.

We started our work on the seL4_tools repository because that was needed to build our new platform and to boot the whole system. Next, we moved on to the kernel itself and added all of the register addresses and interrupts. After that, we added support for timers, the main clock, and two UARTs. Finally, we added a defconfig to sel4test to select our new platform for building.

Afterwards, we tested a simple CAmkES application to verify that CAmkES works on the platform.

 

Interesting Hurdles

A large portion of the porting effort was pretty straight forward, but there were a couple of interesting issues that we encountered. These issues were mostly due to elfloader, the tool that loads and runs the seL4 kernel.

For example, the elfloader calculated the physical to virtual offset as a 32-bit unsigned integer for all architectures. If the physical address was less than the virtual address then the offset would get truncated on 64-bit architectures. We fixed this by making the size of that variable dependent on the size of the architecture.

Another issue we ran into was that seL4 doesn’t want to enable the floating point coprocessor, but the elfloader was attempting to use floating point registers. This isn’t an issue when booting with U-Boot, which enables the floating point coprocessor by default, but there may be some configurations where you don’t want U-Boot. To fix this, we modified the compiler flags for both 64-bit and 32-bit Arm builds of the elfloader to not use floating point registers.

 

Other Improvements

We only scratched the surface of support for this porting effort. We only provided support for the bare minimum of devices needed for sel4test to run successfully. So, more devices can be mapped into the kernel and drivers for those devices can be provided to the util_libs and seL4_libs repositories. Also, camkes-arm-vm could be ported so that developers can run Linux on top of seL4 on the Zynq UltraScale+ MPSoC.

 

Trying It Out Yourself

The main goal of the Zynq UltraScale+ MPSoC port was to expand the seL4 ecosystem and give developers more options. So it is more useful if people are actually able to try out our work. Follow the instructions below to run it on your own ZCU102 evaluation kit.

These instructions assume you have Xilinx SDK and PetaLinux v2016.4 installed: Xilinx Downloads

 

Board Configuration

1. Set bootmode to JTAG
2. Plug in Power, UART (USB), and JTAG (USB)
3. Switch power on
4. Connect to the UART with a 115200 Baudrate

Setup Project

$ mkdir sel4test && cd sel4test
$ repo init \
-u https://github.com/seL4/sel4test-manifest \
-m default.xml
$ repo sync

64-Bit
Building
$ make zynqmp_aarch64_debug_xml_defconfig
$ make

Build FSBL, U-Boot, and ATF
1. Follow instructions here to build 64-bit boot images.
2. Copy generated u-boot.elf, zynqmp_fsbl.elf, and bl31.elf to seL4 project root folder.

Booting

These instructions are for JTAG, but we have also booted from an SD Card and QSPI.

1. Write a tcl script to load and run images over JTAG, boot-64.tcl:

proc run {fsbl uboot atf image_bin image_addr} {
  # Reset Processor
  targets -set -nocase -filter {name =~"*A53*0"}
  rst -processor

  # Download and run First Stage BootLoader
  dow $fsbl
  con
  after 5000
  stop

  dow $image_bin
  dow $uboot
  dow $atf
  con
}

# Set file locations
set uboot ./u-boot.elf
set fsbl ./zynqmp_fsbl.elf
set atf ./bl31.elf
set image_bin ./images/sel4test-driver-image-arm-zynqmp
set image_addr 0x10000000

connect -url tcp:127.0.0.1:3121
after 1000
run $fsbl $uboot $atf $image_bin $image_addr

* Make sure the input arguments point to the correct files on your system.

2. Run the script:

$ xsdb boot-64.tcl

3. In the UART terminal, stop U-Boot autoboot and start binary:

ZynqMP> go 0x10000000

You should see output from the tests and a final report that should say that all tests pass.
All is well in the universe.

 

32-bit

Since our boot method for 32-bit doesn’t use a full Xilinx software stack, it does exhibit some inconsistent behavior and may require updates to the platform’s FSBL to resolve, such as modifying the default clock value.

Building

$ make clean
$ make zynqmp_aarch32_debug_xml_defconfig
$ make
$ arm-linux-gnueabi-objcopy -O binary \
images/sel4test-driver-image-arm-zynqmp \
images/sel4test-driver-image-arm-zynqmp.bin

Generate First Stage Boot Loader
A bootloader is needed to configure the peripherals for the Zynq UltraScale+ MPSoC, especially to configure the DDR controller so seL4 has access to all of the RAM.
1. Run xsdk
2. Create 32-bit FSBL image
  i. File -> New… -> Application Project
    a. Project Name: seL4_FSBL
    b. Hardware Platform: ZCU102-ES2_HW_Platform
    c. Compiler: 32-bit
  ii. Click Next button
  iii. Select Zynq MP FSBL
  iv. Click Finish button
  v. XSDK will automatically build the image

Booting
These instructions are for JTAG, but we have also booted from an SD Card and QSPI.
1. Write a tcl script to load and run images over JTAG, boot.tcl:

proc run {fsbl utils image_bin image_addr} {
  # Set to 32-bit Mode
  source $utils
  targets -set -nocase -filter {name =~"APU*"}
  enable_a32_mode 0

  # Reset Processor
  targets -set -nocase -filter {name =~"*A53*0"}
  rst -processor

  # Download and run First Stage BootLoader
  dow $fsbl
  con
  after 5000
  stop

  # Download and run seL4Test
  dow -data $image_bin $image_addr
  con -addr $image_addr
}

# Set file locations
set utils /opt/Xilinx/SDK/2016.4/scripts/sdk/util/zynqmp_utils.tcl
set fsbl ./workspace/seL4_FSBL/Debug/seL4_FSBL.elf
set image_bin ./images/sel4test-driver-image-arm-zynqmp.bin
set image_addr 0x10000000
connect -url tcp:127.0.0.1:3121
after 1000
run $fsbl $utils $image_bin $image_addr

* Make sure the input arguments point to the correct files on your system.

2. Run the script:

xsdb boot.tcl

You should see output from the tests and a final report that should say that all tests pass.

All is well in the universe.

 

Conclusion

Security is a growing concern in all embedded markets. SeL4 running on the Zynq UltraScale+ MPSoC is a great solution due to the formal proof of seL4 and the security features provided by the Zynq UltraScale+ MPSoC.

DornerWorks is always looking to provide the best security solutions and will continue to look for ways to improve the seL4 ecosystem. We hope you get some use out of this port.

 

To learn more about the seL4 microkernel solutions, visit here.