Introduction to the Secure Microkernel, seL4 C1874

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.

You must complete all course contact hours and successfully pass the learning assessment to obtain CEUs.

  • seL4 Overview
    • Kernel
    • Userspace and processes
    • Capabilities and Cspaces/Vspaces
    • CAmkES
  • 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
Nathan Studer and Robert VanVossen

Robbie is an embedded engineer at DornerWorks in Grand Rapids, MI. Robbie has a B.S.E in computer engineering from Grand Valley State University. Since working at DornerWorks, Robbie has been heavily involved in open-source separation technologies, specifically Xen and seL4. He has contributed patches to both of these projects, ranging from bug fixes to new features. Robbie has given multiple trainings on Virtuosity, which is DornerWorks’ Xen distribution. He has also spoken at the seL4 Summit, GVSETS, and the Xen Developers Summit.

Nathan is a senior engineer at DornerWorks in Grand Rapids, MI. Nathan has a B.S.E in Electrical Engineering from Calvin College and an M.S.E. in Computer Science from Michigan State University. Nathan has been working with virtualization and security technologies both at DornerWorks and as part of Delphi Automotive’s advanced infotainment group utilizing both open-source and commercial embedded operating systems, hypervisors, over-the-air update, and trusted boot software. He has contributed to both the seL4 and Xen open source projects and was the Xen arinc653 scheduler maintainer for several years. Nathan has given several training and conference presentations on Xen and holds a joint patent on deterministic interrupt scheduling.

Duration: 2 Days
CEUs: 1.3

Fees: $1299.00

This seminar is available for Private Delivery Corporate Learning Engagements only. Request Information »
Members save up to 10% off list price.
Log in to see discount.

If paying by any other method or if you have general questions, please contact SAE Customer Service.