Introduction to the Secure Microkernel, seL4
Security continues to be an ever-growing concern in more and more design spaces. There are daily articles about security breaches and there is a need for much higher security through the entire system stack. Thorough testing of systems can lead to stronger security in systems, but testing can only expose so many vulnerabilities. Formal methods is another solution that ensures specific behaviors will not occur. seL4 is the first formally proven microkernel and it is open-source. This makes it a great solution for systems that need strong security. The highest profile application of the seL4 Microkernel was in the DARPA High-Assurance Cyber Military Systems (HACMS) project where it was demonstrated that formal verification can scale to real-life systems to protect a wide range of cyber-physical systems from attacks. The biggest drawback of seL4 is that not many developers know about it or know how to utilize it.
This seminar will focus on providing attendees with an overview of seL4, its associated proof, and all of its software components. It will also focus on teaching participants how to use, build, and write applications for seL4. This knowledge will give designers another tool to combat vulnerabilities by having a secure foundation.
Students should bring their own laptops to the class to be able to participate in the hands-on exercises and labs and maximize their learning experience.
What Will You Learn
- Determine if seL4 is a good choice for your security solutions
- Develop and build basic seL4 applications
- Describe what the formal proof implies about seL4
- Identify capability-based systems
Is This Course For You
- seL4 Overview
- Userspace and processes
- Capabilities and Cspaces/Vspaces
- The Proof
- Formal Methods introduction
- Proof assumptions
- Proof implications
- Hands-on exercises and labs on:
- Building seL4 and an application
- Running seL4 systems on hardware
- Configuring seL4 applications
- Configuring CAmkES applications
- Debugging seL4 applications with GDB
- Writing an seL4 application that interacts with a hardware device