seL4-US
×

seL4 Summit
seL4 Summit
seL4 Summit

Air Force Research Laboratory
Defense Advanced Research Projects Agency
seL4
Air Force Research Laboratory
Defense Advanced Research Projects Agency
seL4
Air Force Research Laboratory
Defense Advanced Research Projects Agency
seL4

The 2019 seL4 Summit was held on September 23-26, 2019 at the Hyatt Regency Dulles Herndon, VA. We would like to thank the Summit attendees, and especially the Summit speakers, for making the Summit a great success! The CoE plans to use the feedback from attendee surveys to help make the 2020 seL4 Summit even better.

seL4 is the first formally verified microkernel, which offers fundamental software separation properties and provides new opportunities to build assured computer systems. The seL4 Summit is part of an effort to establish a Center of Excellence for seL4 ecosystems, aiming to further mature the seL4 technology, stabilize the software distribution, train and expand the user base, and develop much needed capabilities required by the Department of Defense, other government agencies, and commercial applications.

The development of seL4 was supported by the Defense Advanced Research Projects Agency (DARPA) under the High-Assurance Cyber Military Systems (HACMS) program, which aims to create technology for the construction of high-assurance cyber-physical systems, where high assurance is defined to mean functionally correct and satisfying appropriate safety and security properties.


For general information (Wiki, GitHub, etc.) about the seL4 Microkernel, please visit https://www.sel4-us.org

Agenda

Monday September 23, 2019 Luray Ballroom
Breakfast (Luray Foyer) 8:00AM - 8:45AM
Session #1 Overview Chair – Dr. Renato Levy
• Opening Remarks and Introduction (Dr. Renato Levy, Intelligent Automation Inc.; Dr. Raymond Richards, DARPA) 8:45AM - 9:00AM
• sel4 Research: What Is Next on the Horizon? (Prof. Gernot Heiser, Data 61) PDF 9:00AM - 9:45AM
• Developing Software to Leverage seL4’s Formal Correctness for Achieving Security Guarantees (Prof. Trent Jaeger, Penn State University) PowerPoint 9:45AM - 10:30AM
BREAK (30 minutes) 10:30AM - 11:00AM
Session #2 seL4 Center of Excellence and Ecosystem Chair – Douglas Schafer
• seL4 CoE Progress and Plans (Dr. Renato Levy, IAI; Jerry Dussault, Griffiss Institute) PDF 11:00AM - 11:30AM
• Virtualization on seL4 – Expanding the CAmkES-ARM-VM (Chris Guikema, DornerWorks) PDF 11:30AM - 12:00PM
• seL4: Community and Contribution (Dr. Ihor Kuz, Data 61) PDF 12:00PM - 12:30PM
LUNCH (1 hour) 12:30PM - 1:30PM
Session #3 Formal Verification – I Chair – Binoy Ravindran
• Formal Verification: An Introduction (Prof. Taylor Johnson, Vanderbilt University) PDF 1:30PM - 2:30PM
• Verified or Not Verified, That Is the Question (Prof. June Andronick, Data 61) PDF 2:30PM - 3:00PM
BREAK (30 minutes) 3:00PM - 3:30PM
Session #4 Government Efforts Chair – Dr. Stuart Card
• Automated Rapid Certification of Software (Dr. Ray Richards, DARPA) PDF 3:30PM - 4:00PM
• seL4 & Agile and Resilient Embedded Systems (ARES) (Douglas Schafer, Air Force Research Laboratory) PDF 4:00PM - 4:30PM
Closing Remarks (Dr. Lok Yan, Air Force Research Laboratory) 4:30PM - 4:45PM

Tuesday September 24, 2019 Luray Ballroom
Breakfast (Luray Foyer) 8:00AM - 8:45AM
Keynote: Deterministic Concurrency and Its Role in Assurance (Prof. Edward Lee, University of California at Berkeley) PowerPoint 8:45AM - 9:30AM
Session #5 Assured Systems – I Chair – Prof. Simon Ou
• Cyber Assured Systems Engineering (Dr. Darren Cofer, Collins Aerospace) PDF 9:30AM - 10:00AM
• Model-Based Code Generation for seL4-Based Systems (Todd Carpenter, Adventium Labs) PDF 10:00AM - 10:30AM
BREAK (30 minutes) 10:30AM - 11:00AM
Session #6 Formal Verification – II Chair – Dr. Jason Li
• VST & DeepSpec: Program Verification in a Verified System Stack (Dr. Lennart Beringer, Prof. Andrew Appel, Princeton University) PDF 11:00AM - 11:30AM
• Formal Proofs of Return Address Integrity (Dr. Freek Verbeek and Prof. Binoy Ravindran, Virginia Tech) PDF 11:30AM - 12:00PM
• Bottom-Up Formal Validation of Binary-Specific Software Properties (Prof. Kevin Hamlen, University of Texas at Dallas) PowerPoint 12:00PM - 12:30PM
LUNCH (1 hour) 12:30PM - 1:30PM
Session #7 seL4 CoE Panel Discussion (Moderator - Todd Carpenter, Adventium Labs) PDF 1:30PM - 3:00PM
• Dr. Ray Richards, DARPA  
• Prof. Edward Lee, University of California at Berkeley  
• Dr. Paul Ratazzi, Air Force Research Laboratory  
• Dr. Darren Cofer, Collins Aerospace  
• Dr. Raj Rajagopalan, Resideo  
BREAK (30 minutes) 3:00PM - 3:30PM
Session #8 Academia Efforts – I Chair – Prof. Cynthia Irvine
• Quality-Time-As-An-Advantage Zero-Pre-Configuration Pairing Scheme for seL4 IoT Devices/Networks (Prof. Yong Guan, Iowa State University) PDF 3:30PM - 4:00PM
• Performance Evaluation of ROS on an seL4-Based Raspberry Pi (Prof. Daniel Limbrick, North Carolina A&T State University) PDF 4:00PM - 4:30PM
• Selling seL4 to Commercial Sectors - Opportunities and Challenges (Prof. Simon Ou, University of South Florida; Dr. Raj Rajagopalan, Resideo) PowerPoint 4:30PM - 5:00PM
Closing Remarks (Dr. Paul Ratazzi, Air Force Research Laboratory) 5:00PM - 5:15PM

Wednesday September 25, 2019 Luray Ballroom
Breakfast (Luray Foyer) 8:00AM - 9:00AM
Session #9 Assured Systems – II Chair – Dr. Gabriela Ciocarlie
• PIPE: Hardware Acceleration for Efficient Enforcement of Software-defined Security Policies (Arun Thomas, Draper Labs) PowerPoint 9:00AM - 9:30AM
• ACE: Assurance, Composed and Explained (Dr. Arquimedes Canedo, Siemens) PowerPoint 9:30AM - 10:00AM
• Hardware-Assisted Safety for seL4 (Dr. Gabriela Ciocarlie, Dr. Prashanth Mundkur, Dr. Peter G. Neumann, SRI International) PDF 10:00AM - 10:30AM
BREAK (30 minutes) 10:30AM - 11:00AM
Session #10 Academia Effort – II Chair – Dr. Lok Yan
• Enabling seL4 Containers to Support Legacy Applications (Prof. Hui Lu, Binghamton University) PowerPoint 11:00AM - 11:30AM
• Safer Enclaves with seL4 and Keystone on RISC-V (Dr. David Kohlbrenner, University of California at Berkeley) PDF 11:30AM - 12:00PM
• Combining ROS with seL4 for Trustworthy Autonomous Systems (Prof. Cynthia Irvine, Naval Postgraduate School) PDF 12:00PM - 12:30PM
LUNCH (1 hour) 12:30PM - 1:30PM
Session #11 Assured Systems – III Chair – Dan Fayette
• Correct-By-Construction Network Stack Synthesis for seL4 (Dr. Eric Smith, Kestrel) PowerPoint 1:30PM - 2:00PM
• seL4 Drivers for Trustworthy Devices (Dr. Stuart Card, Critical Technologies) PDF Web Link 2:00PM - 2:30PM
• Assured Software for Intelligent Manufacturing (Dr. Greg Shannon, CMU SEI) PowerPoint 2:30PM - 3:00PM
BREAK (30 minutes) 3:00PM - 3:30PM
Session #12 Center of Excellence and Way Forward Chair – Dr. Jason Li
• Building Trustworthy Systems on seL4 (Dr. Ihor Kuz, Data61, CSIRO) PDF 3:30PM - 4:00PM
• seL4: Can We "Cross the Chasm"? (Dr. Paul Ratazzi, Air Force Research Laboratory) PDF 4:00PM - 4:30PM
• Summit Summary, Center of Excellence Way Forward (Jerry Dussault, Griffiss Institute) PDF 4:30PM - 5:00PM
Closing Remarks (Dr. Ray Richards, DARPA) 5:00PM - 5:15PM

PDFPowerPoint   Download all the presentations in one large zip file.



Training Session Track (Wednesday and Thursday)

Wednesday, September 25, 2019 Luray Ballroom
Breakfast (Luray Foyer) 8:00AM - 9:00AM
Laptop Setup (Luray Ballroom) 8:30AM - 9:30AM
Presentation Session #1     (Nathan Studer and Chris Guikema, DornerWorks, Ltd.)  
• Kernel 9:30AM - 10:30AM
BREAK (30 minutes) 10:30AM - 11:00AM
• Userspace and processes 11:00AM - 11:45AM
• Capabilities and CSpaces/VSpaces 11:45AM - 12:30PM
LUNCH (1 hour) 12:30PM - 1:30PM
• CAmkES (Component Architecture for MicroKernel-based Embedded Systems) 1:30PM - 2:00PM
Lab Session #1     (Nathan Studer and Chris Guikema, DornerWorks, Ltd.)  
• Building seL4 2:00PM - 3:00PM
BREAK (30 minutes) 3:00PM - 3:30PM
• Adding a hardware resource 3:30PM - 5:00PM


Thursday, September 26, 2019 Luray Ballroom
Breakfast (Luray Foyer) 8:00AM - 9:00AM
Presentation Session #2     (Nathan Studer and Chris Guikema, DornerWorks, Ltd.)  
• Formal Methods Overview 9:00AM - 9:30AM
• Proof Assumptions 9:30AM - 10:00AM
• Proof Implications 10:00AM - 10:30AM
BREAK (30 minutes) 10:30AM - 11:00AM
Lab Session #2     (Nathan Studer and Chris Guikema, DornerWorks, Ltd.)  
• Debugging applications with GDB 11:00AM - 11:45AM
• Adding a Network Stack 11:45AM - 12:30PM
LUNCH (1 hour) 12:30PM - 1:30PM
• Adding TCP to the Network Stack 1:30PM - 2:15PM
• Writing an HTTP Server Application 2:15PM - 3:00PM
BREAK (30 minutes) 3:00PM - 3:30PM
Open Discussion     (Nathan Studer and Chris Guikema, DornerWorks, Ltd.) 3:30PM - 5:00PM

Venue

The 2019 seL4 Summit was held September 23-26, 2019 at:

Hyatt Regency Dulles
2300 Dulles Corner Blvd.
Herndon, VA 20171

hotel


seL4 Summit Registration

If you would like to be notified about the 2020 seL4 Summit and other major seL4 events, please consider emailing any contact information that you feel comfortable sharing to: summit@sel4-us.org

We respect your privacy, so please be assured that we will only use your email address to contact you about significant seL4-related events.

Contact

Do you have additional questions about the seL4 Summit?

summit@sel4-us.org