Extreme Security is Reachable.

If you need isolation or partitioning of software running on your computing platform and need to prove correctness with mathematical (formal methods) level of rigor, you should consider the open source seL4 microkernel.

seL4 has already been proven secure, so you don’t have to do the extreme math yourself.  DornerWorks will help you fill in the gaps to enhance your security story.
GET THE DATASHEET

US Support

DornerWorks is based in the United States.  Our engineers are all US persons.  We have worked on seL4 products (such as drivers, tools, system architecture) for government (DARPA) and commercial customers.

How do I get started?

1. seL4 is open source and free.  Start there!
2. Contact DornerWorks for a free initial consultation or jump right in with our seL4 Quick Start Package.
3. We will collaborate with you to extend the seL4 technology and make it work for your system and your design assurance needs.

Get a seL4 Quick Start Package

What is seL4?

• World’s first formal proof of correctness of a separation microkernel
  • Formal, machine-checked verification by NICTA provides proof that…
    • Source code satisfies specification (written in Haskell)
    • Object code conforms to source code
    • Security properties (e.g., kernel will never crash, nor hang)
  • http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf
• Very small footprint
  • 8,700 lines of C code and 600 lines of assembler
• Member of the L4 family of high-performance microkernels
• Hardware support: x86, ARMv6, ARMv7
• Virtualization mode
• Very limited features (purposely)
  • Many typical OS features delegated to user-mode applications (granted privilege via passed capabilities)
    • Device drivers, memory management, network protocol stack, file system

How do you pronounce seL4?

At first there was not a consensus.  Some people said it like it was a word: “sell four”.  Others said the individual letters: “s – e – L – 4”.  However, recently we learned from our friends at data61 that they are worried that saying the word sometimes confuses people into thinking of “cell”.  So they now prefer to say the individual letters.

DornerWorks Presentations and Projects on seL4

• Steven H. VanderLeest, “Is Formal Proof of seL4 Sufficient for Avionics Security?” IEEE Aerospace and Electronic Systems Magazine, Feb, 2018, pp. 16-21.
• Steven H. VanderLeest, “The Open Source, Formally-Proven seL4 Microkernel: Considerations for Use in Avionics,” Proceedings of the 35th Digital Avionics Systems Conference (DASC), Sacramento, CA, Sep 2016.
• Principal Investigator, United States Defense Advanced Research Projects Agency (DARPA) Small Business Innovation Research (SBIR) Phase I contract awarded to DornerWorks, Ltd., “Leveraging Assurance on an seL4-Enabled Safe & Secure Soldier Helmet Display,” Contract Number D16PC00107 , June 2016.
• Principal Investigator, United States Defense Advanced Research Projects Agency (DARPA) Small Business Innovation Research (SBIR) Phase I contract awarded to DornerWorks, Ltd., “An seL4 – Enabled Safe & Secure Soldier Helmet Display,” Contract Number D15PC00163, July 2015.
• Gregg Wildes and Steve VanderLeest, “Security Via Isolation Utilizing the seL4 Microkernel,” 2016 Government Cyber Security SBIR Workshop, Washington, DC, August 30-September 1, 2016.
• Steven H. VanderLeest,“SBIR Overview: Security via Isolation using the seL4 Microkernel,” High-Assurance Cyber Military Systems (HACMS) symposium, Pittsburgh, PA, Sep 7-9, 2016.
• Steven H. VanderLeest, “An seL4-Enabled Safe & Secure Soldier Helmet Display: Overview of the DornerWorks & Rockwell Collins SBIR,” seL4 Developers’ Day, 14 Aug 2015, Washington, DC.
• Steven H. VanderLeest, “Security via Isolation using the seL4 Microkernel,” TARDEC Innovation Talk, US Army Tank Automotive Research, Development and Engineering Center (TARDEC/Ground Vehicle Systems Center), Warren, Michigan, 23 May 2016.
• Chris Guikema, “Debugging seL4 with GDB,” First International seL4 Workshop, Malibu, CA, 15 Dec 2016.