Modular Build and Binary Verification for seL4
Collaboration between individuals is standard practice for a vast majority of software projects; however, collaboration between companies can be more difficult.
What happens when one company wants to protect their intellectual property?
Achieving this goal can lead to complexities when the software build process produces a single, monolithic image. Independent Build, Link, and Load is the ability to create modular components that can be produced at different times by different developers, linked together, and loaded onto the target platform for execution.
DornerWorks has open-sourced code and instructions for this process using the seL4 microkernel. This clearly demonstrates that the only dependencies between applications are those that are expected; they are isolated at the source code level, allowing for collaboration between developers while protecting intellectual property.
Binary Verification of CAmkES applications helps aid in the overall security and safety story by ensuring the image built by the developers is the same image loaded onto the target platform. During the build process, a hash of the kernel and each application is stored and loaded into an archive. The root task unpacks the images and performs the same hash on each image before loading. The system aborts if the hashes do not match. This process ensures the applications built by the project developers are the same applications that get loaded on the target platform.
DornerWorks developed these capabilities by extending Data61’s seL4 tools repository (https://github.com/seL4/seL4_tools) as part of a Small Business Innovation Research project for the United States Defense Advanced Research Projects Agency (US DARPA). The source code for the secure build are located in the seL4_Tools mainline, since commit 0b34370. Instructions for use can be found here: https://github.com/seL4/seL4_tools/blob/master/elfloader-tool/src/arch-arm/README.md