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

Registration is now open for the 2019 seL4 Summit! It will be held September 23-26, 2019 at the Hyatt Regency Dulles Herndon, VA. We would like to thank the Summit 2018 attendees and speakers, and encourage them to attend the 2019 Summit and invite their colleagues. Register now in order to take advantage of special Early Bird pricing. Please also consider reserving a room at the Hyatt Regency Dulles during your stay at the Summit. Discounted rates are currently being offered.

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) 9:00AM - 9:45AM
• Developing Software to Leverage seL4’s Formal Correctness for Achieving Security Guarantees (Prof. Trent Jaeger, Penn State University) 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) 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 (1 hour) 12:30PM - 1:30PM
Session #3 Formal Verification – I Chair – Binoy Ravindran
• Formal Verification: An Introduction (Prof. Taylor Johnson, Vanderbilt University) 1:30PM - 2:30PM
• Verified or Not Verified, That Is the Question (Prof. June Andronick, Data 61) 2:30PM - 3:00PM
BREAK (30 minutes) 3:00PM - 3:30PM
Session #4 Government Efforts Chair – Dr. Paul Pazandak
• Automated Rapid Certification of Software (Dr. Ray Richards, DARPA) 3:30PM - 4:00PM
• seL4 & Agile and Resilient Embedded Systems (ARES) (Douglas Schafer, Air Force Research Laboratory) 4:00PM - 4:30PM
• What We Are Looking for from seL4 CoE and What We Think We Can Contribute to the CoE (Jon Paulikonis, NavAir) 4:30PM - 5:00PM
Closing Remarks (Dr. Lok Yan, Air Force Research Laboratory) 5:00PM - 5:15PM

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) 8:45AM - 9:30AM
Session #5 Assured Systems – I Chair – Prof. Simon Ou
• Cyber Assured Systems Engineering (Dr. Darren Cofer, Collins Aerospace) 9: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 Chair – Dr. Jason Li
• Verification of Modular and Effectful C Programs Using VST (Dr. Lennart Beringer, Prof. Andrew Appel, Princeton University) 11:00AM - 11:30AM
• Verification Condition Generation for Formal Guarantees Against ROP Attacks (Dr. Freek Verbeek and Prof. Binoy Ravindran, Virginia Tech) 11:30AM - 12:00PM
• Bottom-Up Formal Validation of Binary-Specific Software Properties (Prof. Kevin Hamlen, University of Texas at Dallas) 12:00PM - 12:30PM
LUNCH (1 hour) 12:30PM - 1:30PM
Session #7 seL4 CoE Panel Discussion (Moderator - Todd Carpenter, Adventium Labs) 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 (Prof. Yong Guan, Iowa State University) 3:30PM - 4:00PM
• Performance Evaluation of ROS on an seL4-Based Raspberry Pi (Prof. Daniel Limbrick, North Carolina A&T State University) 4:00PM - 4:30PM
• seL4 Transition Experience in Building Automation (Prof. Simon Ou, University of South Florida; Dr. Raj Rajagopalan, Resideo) 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
• Building Secure Systems Using seL4 RISC-V and Tagged Hardware (Arun Thomas, Draper Labs) 9:00AM - 9:30AM
• ACE: Assurance, Composed and Explained (Dr. Arquimedes Canedo, Siemens) 9:30AM - 10:00AM
• Hardware-Assisted Safety for seL4 (Dr. Gabriela Ciocarlie, Dr. Prashanth Mundkur, Dr. Peter G. Neumann, SRI International) 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) 11:00AM - 11:30AM
• Safer Enclaves with seL4 and Keystone on RISC-V (Dr. David Kohlbrenner, University of California at Berkeley) 11:30AM - 12:00PM
• Combining ROS with seL4 for Trustworthy Autonomous Systems (Prof. Cynthia Irvine, Naval Postgraduate School) 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) 1:30PM - 2:00PM
• seL4 Drivers for Trustworthy Devices (Dr. Stuart Card, Critical Technologies) 2:00PM - 2:30PM
• Assured Software for Advanced Manufacturing (Dr. Greg Shannon, CMU SEI) 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) 3:30PM - 4:00PM
• seL4: Can We "Cross the Chasm"? (Dr. Paul Ratazzi, Air Force Research Laboratory) 4:00PM - 4:30PM
• Summit Summary, Center of Excellence Way Forward (Jerry Dussault, Griffiss Institute) 4:30PM - 5:00PM
Closing Remarks (Dr. Ray Richards, DARPA) 5:00PM - 5:15PM


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

Please visit the special seL4 Summit hotel reservation website in order to obtain the best possible discounted rate.

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

hotel


Please note that the hotel provides complimentary airport shuttle service from Dulles Airport

The IAD Shuttle leaves from the hotel every 30 minutes beginning at 4:15 am through 12:15 am. The shuttle picks up at the airport every 30 minutes from 4:30 am ending at 12:30 am. The airport pick up location is curbs 2A and 2H, in lower baggage claim.

seL4 Summit Registration

Early Bird (before 8/4/19) Full Price
Registrant Full Conference Sessions Only Full Conference Sessions Only
Regular $950 $700 $1100 $800
Student $665 $490 $770 $560
Full Conference includes 4 days of speaker presentations and hands-on training sessions
Sessions Only includes 3 days of speaker presentations only

To register for the 2019 seL4 Summit, please visit the official Summit Registration Website


Attention Students! A limited number of Student Travel Grants are available.
(Applications are due by August 2, 2019)

Student Travel Grants

Travel grants are available to help partially cover the travel expenses of student attendees to the 2019 seL4 Summit.

Who Should Apply

We encourage applications from students from a wide variety of institutions, diverse backgrounds, and first time attendees. The travel grants will be given to students enrolled in U.S. institutions. Both undergraduate and graduate students will be considered for this award.

Award Criteria

We are unable to provide awards to all applicants. Awards will be determined by a committee of volunteers participating in the organization of the 2019 seL4 Summit. Preference will be given to students working on embedded systems security, students who can show evidence of financial need to attend the Summit, and students from diverse backgrounds. In order to ensure a diverse pool of awardees to the Summit, travel awards will be limited to at most one student per advisor, and at most two students from the same institution.

Award Description

We will reimburse registration costs and partial travel expenses (hotel, transportation, and meals) for a total of up to $1000.

How to Apply

Applications are due by August 2, 2019. Students will be notified by August 5, 2019 and will be expected to register before August 15, 2019. Please note that selected students not meeting the registration date deadline may forfeit their award. Applications should be submitted by filling out the form:

View the Application form

An application for a travel award will consist of a single PDF file with the student's resume, a statement from the student, and a letter from the student's research advisor with a justification of financial need. The student's statement should include a summary of research interests, and a statement of why the applicant will benefit from participating in the Summit.


If you would like to be notified about the 2019 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