Introduction to the Secure Microkernel, seL4


July 16-February 17, 2019 VA, Herndon SAE International Classroom Seminar

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.

Learning Objectives

By attending this seminar, you will be able to:

  • 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

Who Should Attend

This course will benefit software, computer or systems engineers, security specialists, or embedded developers that focus on security.


An undergraduate engineering or computer science degree or a strong technical background is highly recommended. A basic knowledge of operating systems is required. Students should know how to program in C.

Note: See related course, Formal Methods for Functional Safety and Security in Cyber-Physical Systems, for more in-depth training.

Register Now