2020 Summit
Third Annual Summit Technical Program
November 15-19, 2020
The third CoE Summit was held November 16-18, 2020, with an optional self-paced tutorial available to all participants on the Sunday just prior to the Summit start, on November 15th. Due to the COVID pandemic, this year’s Summit was a virtual event. The intensive four-day event provided registrants the opportunity to attend presentations by government, industry, and academia experts interact with discussion panels, and obtain an introductory, hands-on self-paced tutorial for the seL4® microkernel. Approximately 121 government, industry, and academia attendees attended the 2020 CoE Summit.
Once logged in, registrants were presented with the Summit Virtual Hub that was the center of all activity surrounding the event. Each day of the Summit was selectable at the top of the page and, when selected, the agenda for that day was presented. Each presentation title was a hyperlink to a page where the pre-recorded presentation was viewed, and a discussion board was available for attendees to ask questions and interact with the speaker and other attendees. Once presented in accordance with the agenda timing, the pre-recorded presentations were then available for viewing for the rest of the Summit and afterwards, allowing attendees to view at their convenience.
Based upon feedback from prior Summits, the number of presentations per day and the length of breaks were structured to facilitate more discussion and provide the opportunity for networking. A broad spectrum of topics related to seL4® technology were presented during the Summit, and those in attendance absorbed a wealth of seL4®-related information presented by experts representing government, industry, and academia.
The first day of the 2020 CoE Summit, Sunday November 15th, was an optional self-paced tutorial providing an introduction to seL4® and some hands-on exercises to step the user through some of the more useful concepts in understanding and using seL4®. The exercises provided a set of building blocks that culminated in the re-creation of one of the first ever video games, the game of Pong. The content was downloadable from the Summit Virtual Hub and consisted of the following:
- Introduction to seL4 (ppt) – a self-guided PowerPoint slide deck providing an introduction to seL4 along with guidance for the hands-on exercises.
- seL4-IAI.ova – a virtual machine pre-equipped with all the necessary environment setup needed to build seL4 projects within Docker containers.
- VM-Instructions (pdf) – details on the set up of the virtual machine (VM).
- Environment-setup (shell script) – to assist in configuring the attendee’s machine if they choose not to use the VM.
- Exercises (zip) – 11 different exercises to assist attendees in learning seL4 concepts and putting them in to practice. Most of the exercises contain a src folder and a solution folder. The src folder contains partially completed code with portions to be completed by the student. The solution folder contains the fully completed code.
- Exercises (ppt) – the exercise slides from the Introduction to seL4 slide deck, separated for your convenience.
2020 Summit Agenda
Sunday, Nov. 15 | Monday, Nov. 16 | Tuesday, Nov. 17 | Wednesday, Nov. 18
Monday, November 16, 2020
Chair & Time Session #1 – Introduction and Keynote Dr. Renato LevyOpening Remarks and Introduction to Keynote Speaker
(Dr. Renato Levy, Intelligent Automation Inc.; Dr. Jason Li, Siege Technologies) 09:00AM – 09:15AM
VideoKeynote 1: Targeted Formal Methods (Dr. Greg Shannon, CMU SEI) 09:15AM – 10:15AM
Presentation | Video: Keynote Intro | Video: Keynote | Chat Transcript
Break (15 Minutes) 10:15AM – 10:30AM
Session #2 – Government Efforts Douglas Schafer
- Army CCDC-GVSC Vision and Progress (Leonard Elliott, Army CCDC-GVSC) 10:30AM – 11:00AM
- CPS Security and Resilience: Viewpoint from ONR (Dr. Ryan Craven, ONR) 11:00AM – 11:30AM
- To ARM and Beyond: Embedding seL4 in the Air Force (Kyle Tillotson, AFRL) 11:30AM – 12:00PM
- Government Support of seL4 Ecosystem (Dr. Ray Richards, DARPA) 12:00PM – 12:30PM
Break (30 Minutes) 12:30PM – 13:00PM
Session #3 – Core Technologies Kyle Tillotson
- seL4 + TrustZone: Spanning both worlds (Nick Spinale, ARM Research) 13:00PM – 13:30PM
- Defense in Depth: Building 21st Century Secure Systems with PIPE 13:30PM – 14:00PM (Dr. Arun Thomas and Chris Casing, Draper Laboratory)
- VST+DeepSpec: connecting a program logic to a verified OS kernel 14:00PM – 14:30PM (Dr. Lennart Beringer, Princeton University)
- Strengthening Binary Software Verification with Certified Code Transforms 14:30PM – 15:00PM
Break (15 Minutes) 15:00PM – 15:15PM
Keynote 2: seL4 – State of the Union 15:15PM – 16:00PM
(Prof. Gernot Heiser, UNSW and Data61); Keynote introduction by Dr. Renato Levy
Presentation | Video: Keynote Intro | Video: Keynote | Chat Transcript
Break (15 Minutes) 16:00PM – 16:15PM
Session #4 – Panel Discussion: Techniques for Assurance 16:15PM – 17:15PM
(Moderator: Dr. Jason Li)
- Dr. Lennart Beringer, Princeton University
- Dr. Sergey Bratus, DARPA
- Prof. Kevin Hamlen, University of Texas at Dallas
- Prof. Gernot Heiser, UNSW and Data61
Closing Remarks (Dr. Lok Yan, Air Force Research Laboratory) 17:15PM – 17:30PM
Tuesday, November 17, 2020
Chair & Time Session #5 – Introduction and Keynote Dr. Ray RichardsIntroduction to Keynote Speaker (Dr. Raymond Richards, DARPA) 09:00AM – 09:15AM
Keynote 3: Formal Methods at Scale – Crossing a Threshold (Dr. Bill Scherlis, DARPA I2O) 09:15AM – 10:15AM
Video: Intro | Video: Keynote | Chat Transcript
Break (15 Minutes) 10:15AM – 10:30AM
Session #6 – Assured Systems – I Dr. Paul Pazandak
- seL4 Systems Development Made Easy (Sascha Kegreiß, HENSOLDT Cyber GmbH) 10:30AM – 11:00AM
- Challenges to the Industrial Adoption of seL4 (James Potts and Mark Bortz, Collins Aerospace) 11:00AM – 11:30AM
- Dishwashing with SeL4, or how to get seL4 working with nuclear weapons 11:30AM – 12:00PM (Randy Lober, Robert Armstrong and Noah Evans, Sandia Labs)
- The Need for Assured Execution – The Future of Code Has No Source (Matt Mickelson, MITRE) 12:00PM – 12:30PM
Break (30 Minutes) 12:30PM – 13:00PM
Session #7 – Assured Systems – II Dr. Eric Smith
- Time Enough for seL4 (Todd Carpenter, Adventium Labs) 13:00PM – 13:30PM
- Building a Commercial Virtualized Mobile Device with seL4 13:30PM – 14:00PM (Jason Sebranek and Yanyan Shen, Cog Systems, Inc.)
- Open Platform for Trustworthy Networked Autonomy 14:00PM – 14:30PM (Dr. Stuart Card, Tim Morin, and Nathan Studer; Critical Technologies Inc; Microchip Technology Inc; DornerWorks, Ltd)
Break (30 Minutes) 14:30PM – 15:00PM
Special Presentation: Introduction to the seL4 Proofs (Matthew Brecknell, Data61) 15:00PM – 16:00PM
Speaker introduction by Dr. Renato Levy
Video: Intro | Video: Special Presentation | Chat Transcript
Break (15 Minutes) 16:00PM – 16:15PM
Session #8 – Panel Discussion – Tales from the Crypt 16:15PM – 17:15PM
(Moderator: Todd Carpenter)
- Karl Hoech, Collins Aerospace
- Kent McLeod, Kry10 Limited
- Douglas Schafer, Cohere Technology LLC
Closing Remarks (Dr. Paul Ratazzi, Air Force Research Laboratory) 17:15PM – 17:30PM
Wednesday, November 18, 2020
Chair & Time Session #9 – Academia Research Dr. Lok Yan
- Securing Cloud Serverless Infrastructure with seL4 (Prof. Hui Lu, Binghamton University) 09:00AM – 09:30AM
- Building A Trusted Execution Environment for In-Storage Computing 09:30AM – 10:00AM (Prof. Jian Huang, University of Illinois at Urbana-Champaign)
- HAMR - High-Assurance Modeling & Rapid Engineering for seL4-based Embedded Systems Using AADL 10:00AM – 10:30AM (John Hatcliff and Robby, Kansas State University)
Break (30 Minutes) 10:30AM – 11:00AM
Session #10 – Assured Systems – III Dr. Stuart Card
- Formally Verified Network Stack Synthesis for seL4 (Dr. Eric Smith, Kestrel) 11:00AM – 11:30AM
- Virtualization and Customer Value (Carl L. Nerup, Cog Systems, Inc.) 11:30AM – 12:00PM
- A Secure Distributed Computing Middleware for the seL4 Ecosystem 12:00PM – 12:30PM (Dr. Paul Pazandak and Fabrizio Bertocci, RTI)
Break (30 Minutes) 12:30PM – 13:00PM
Session #11 – Thoughts, Challenges and Center of Excellence Todd Humiston
- Thoughts on Non-functional Challenges in seL4 13:00PM – 13:30PM (Prof. Gabe Parmer, The George Washington University)
- Building of the Training: the challenge and path to success (Ammar Salman, IAI) 13:30PM – 14:00PM
- Center of Excellence Progress and Way Forward (Jerry Dussault, Griffiss Institute) 14:00PM – 14:30PM
Break (30 Minutes) 14:30PM – 15:00PM
Session #12 – Updates from the Home Base Jerry Dussault
- The seL4 Foundation: update and why you should join (Prof. June Andronick, Data61 and UNSW) 15:00PM – 15:30PM
- Systems beyond POSIX (Curtis Millar, Data61) 15:30PM – 16:00PM
- The seL4 Core Platform (Ben Leslie, Breakaway Consulting; Gernot Heiser, Data61) 16:00PM – 16:30PM
- seL4 Device Driver Framework (Dr. Ihor Kuz, Data61) 16:30PM – 17:00PM
Closing Remarks (Dr. Ray Richards, DARPA) 17:00PM – 17:15PM
Video