2019 seL4 Summit

Second seL4 Summit Technical Program

September 23-25, 2019
The first day of the event included nine presentations by government, industry, and academia experts discussing a variety of topics specifically related to the seL4® microkernel. Discussed were an overview of the seL4 microkernel, continued plans for the seL4 Center of Excellence and related seL4 ecosystem topics, an extended introduction to Formal Verification, and Government efforts related to seL4. On the second day of the event, the keynote speaker, Professor Edward Lee from the University of California at Berkeley spoke about Deterministic Concurrency and Its Role in Assurance. Other sessions on the second day included topics about Assured System, Formal Verification, and academia efforts related in the seL4 ecosystem. Todd Carpenter of Adventium Labs moderated a lively seL4 CoE Expert Panel Discussion that received much interested from attendees.
On the third day of the event, attendees had the option of continuing with the “General Session” track containing further presentations, or, attendees could choose the “Training Session” track, which provided a more “hands-on” approach. Both tracks conveyed a substantial amount of information regarding seL4. The hands-on portion of the training sessions occurred on the third and fourth days of the seL4 Summit event. The third day was the final day of the General Session track, and discussed that day were a second round of presentations regarding academia efforts related to seL4 technology. A second and third round of talks that were placed in the “Assured Systems” category were also presented. The General Session concluded with summaries about the “Center of Excellence” and planned directions forward in future years.
For the Training Session track, Nathan Studer, Chris Guikema, and Alex Pavey from DornerWorks Ltd. led a series of presentations with both lecture and labs components. Lecture presentation material began with a general background discussing microkernels, followed by advantages, disadvantages, and common characteristics of microkernels. After a seL4 kernel overview, the lecturers led the class into a deep dive about the seL4 user space and seL4 processes. Development environments were discussed, a CAmkES overview was provided and the lecturers covered the topic of porting and concluded with a discussion of using U-boot on the i.MX8. Instructors also provided students lab materials covering seL4 topics like:
  • Building an seL4 system
  • Adding a hardware resource to seL4
  • Debugging applications with GDB
  • Adding a network stack / Adding TCP to the network stack
  • Writing an HTTP Server Application
2019 Summit Agenda
Monday, September 23, 2019
Chair & Time
Session #1 – Overview Dr. Renato Levy
  • Opening Remarks and Introduction (Dr. Renato Levy, Intelligent Automation Inc.; Dr. Raymond Richards, DARPA) 08:45AM – 09:00AM
  • sel4 Research: What Is Next on the Horizon? (Prof. Gernot Heiser, Data 61) 09:00AM – 09:45AM
  • Developing Software to Leverage seL4’s Formal Correctness for Achieving 09:45AM – 10:30AM Security Guarantees (Prof. Trent Jaeger, Penn State University)
Break (30 Minutes) 10:30AM – 11:00AM
Session #2 – seL4 Center of Excellence and Ecosystem Douglas Schafer
  • seL4 CoE Progress and Plans (Dr. Renato Levy, IAI; Jerry Dussault, Griffiss Institute) 11:00AM – 11:30AM
  • Virtualization on seL4 – Expanding the CAmkES-ARM-VM (Chris Guikema, DornerWorks) 11:30AM – 12:00PM
  • seL4 Community and Contribution (Dr. Ihor Kuz, Data 61) 12:00PM – 12:30PM
Lunch 12:30PM – 13:30PM
Session #3 – Formal Verification – I Binoy Ravindran
  • Formal Verification: An Introduction (Prof. Taylor Johnson, Vanderbilt University) 13:30PM – 14:30PM
  • Presentation
  • Verified or not verified, that is the question (Prof. June Andronick, Data 61) 14:30PM – 15:00PM
Break (30 Minutes) 15:00PM – 15:30PM
Session #4 – Government Efforts Dr. Paul Ratazzi
  • Automated Rapid Certification of Software (Dr. Ray Richards, DARPA) 15:30PM – 16:00PM
  • Updates on ARES and AFRL Visions for Building Assured Systems 16:00PM – 16:30PM
(Douglas Schafer, Air Force Research Laboratory)
  • What We Are Looking for from seL4 CoE and What We Think We Can Contribute to the CoE 16:30PM – 17:00PM
(Jon Paulikonis, NavAir)
Closing Remarks (Dr. Lok Yan, Air Force Research Laboratory) 17:00PM – 17:15PM
Tuesday, September 24, 2019
Chair & Time
Keynote 3: Deterministic Concurrency and Its Role in Assurance 8:45AM – 09:30AM (Prof. Edward Lee, University of California at Berkeley)
Session #5 – Assured Systems – I Prof. Simon Ou
  • Cyber Assured Systems Engineering (Dr. Darren Cofer, Collins Aerospace) 09:30AM – 10:00AM
  • Model-Based Code Generation for seL4-Based Systems (Todd Carpenter, Adventium Labs) 10:00AM – 10:30AM
Break (30 Minutes) 10:30AM – 11:00AM
Session #6 – Formal Verification – II Dr. Jason Li
  • Verification of Modular and Effectful C Programs Using VST 11:00AM – 11:30AM
(Dr. Lennart Beringer, Prof. Andrew Appel, Princeton University)
  • Cerification Condition Generation for Formal Guarantees Against ROP Attacks 11:30AM – 12:00PM
(Dr. Freek Verbeek and Prof. Binoy Ravindran, Virginia Tech)
  • Bottom-Up Formal Validation of Binary-Specific Software Properties 12:00PM – 12:30PM (Prof. Kevin Hamlen, University of Texas at Dallas)
Lunch 12:30PM – 13:30PM
Session #7 – seL4 CoE Panel Discussion 13:30PM – 15:00PM (Moderator: Todd Carpenter, Adventium Labs)
  • Dr. Ray Richards, DARPA
  • Prof. Edward Lee, University of California at Berkeley
  • Dr. Paul Ratazzi, Air Force Research Laboratory
  • Dr. Darren Cofer, Collins Aerospace
Break (30 Minutes) 15:00PM – 15:30PM
Session #8 – Academia Efforts – I Prof. Cynthia Irvine
  • Quality-Time-As-An-Advantage Zero-Pre-Configuration Pairing Scheme for seL4 IoT Devices 15:30PM – 16:00PM
(Prof. Yong Guan, Iowa State University)
  • Performance Evaluation of ROS on an seL4-Based Raspberry Pi 16:00PM – 16:30PM (Prof. Daniel Limbrick, North Carolina A&T State University)
  • seL4 Transition Experience in Building Automation 16:30PM – 17:00PM (Prof. Simon Ou, University of South Florida; Dr. Raj Rajagopalan, Resideo)
Closing Remarks (Douglas Schafer, Air Force Research Laboratory) 17:00PM – 17:15PM
Wednesday, September 25, 2019
Chair & Time
Session #9 – Assured Systems – II Dr. Gabriela Ciocarlie
  • Building Secure Systems Using seL4 RISC-V and Tagged Hardware (Arun Thomas, Draper Labs) 09:00AM – 09:30AM
  • ACE: Assurance Composed and Explained (Dr. Arquimedes Canedo, Siemens) 09:30AM – 10:00AM
  • Hardware-Assisted Safety for seL4 (Dr. Gabriela Ciocarlie, SRI International) 10:00AM – 10:30AM
Break (30 Minutes) 10:30AM – 11:00AM
Session #10 – Academia Effort – II Dr. Lok Yan
  • Enabling seL4 Containers to Support Legacy Applications (Prof. Hui Lu, Binghamton University) 11:00AM – 11:30AM
  • Safer Enclaves with seL4 and Keystone on RISC-V 11:30AM – 12:00PM
(Dr. David Kohlbrenner, University of California at Berkeley)
  • Combining ROS with seL4 for Trustworthy Autonomous Systems 12:00PM – 12:30PM (Prof. Cynthia Irvine, Naval Postgraduate School)
Lunch 12:30PM – 13:30PM
Session #11 – Assured Systems – III Dr. Rick Skowyra
  • Correct-By-Construction Network Stack Synthesis for seL4 (Dr. Eric Smith, Kestrel) 13:30PM – 14:00PM
  • seL4 Drivers for Trustworthy Devices (Dr. Stuart Card, Critical Technologies) 14:00PM – 14:30PM
  • Assured Software for Advanced Manufacturing (Dr. Greg Shannon, CMU SEI) 14:30PM– 15:00PM
Break (30 Minutes) 15:00PM – 15:30PM
Session #12 – Center of Excellence and Way Forward Dr. Jason Li
  • Building Trustworthy Systems on seL4 (Dr. Ihor Kuz, Data61, CSIRO) 15:30PM – 16:00PM
  • seL4 COE and AFRL visions ((Dr. Paul Ratazzi, Air Force Research Laboratory) 16:00PM – 16:30PM
  • Summit Summary, Center of Excellence Way Forward (Jerry Dussault, Griffiss Institute) 16:30PM – 17:00PM
Closing Remarks (Dr. Ray Richards, DARPA) 17:00PM – 17:15PM
seL4® Used by permission. Copyright © 2021 Griffiss Institute. All rights reserved