2020 seL4 Summit
Third seL4 Summit Technical Program
November 15-19, 2020
The third seL4® 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 seL4 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 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.
During the day and throughout the Summit, assistance was available via the discussion board for those attendees that ran into challenges with the tutorial. Overall, while some attendees found the tutorial to be challenging, the feedback was positive.
The Summit officially kicked off on Monday, November 16th and began with a keynote presentation entitled “Targeted Formal Methods” by Dr. Greg Shannon. He was followed by a series of four presentations that discussed government efforts related to seL4 in the Army Combat Capabilities Development Command, the Office of Naval Research, the Air Force Research Laboratory, and DARPA. The afternoon kicked off with four presentations focused on core technologies from ARM Research, Draper Laboratory, Princeton University, and the University of Texas at Dallas. The afternoon keynote address entitled “seL4 – State of the Union” was then given by Professor Gernot Heiser from UNSW and Data61. The day concluded with a live panel session discussing Techniques for Assurance.
The following day began with a keynote address from Dr. William Scherlis from DARPA entitled “Formal Methods at Scale – Crossing a Threshold”. The presentation was very well received and there is interest in the CoE community of giving it wider distribution, perhaps through a YouTube channel associated with the CoE. The bulk of the day focused on assured systems with morning presentations by HENSOLDT Cyber GmbH, Collins Aerospace, Sandia Labs, and MITRE. The afternoon resumed discussion of assured systems with presentations from Adventium Labs, Cog Systems, Inc., and a team from Critical Technologies, Inc., Microchip Technologies, Inc. and DornerWorks, Ltd. A special presentation entitled “Introduction to the seL4 Proofs” was given by Matthew Brecknell from Data61. This presentation directly addressed comments received in the 2019 Summit on the need to spend more time in this area. Finally, the day concluded with a live panel discussion focused on projects/programs using seL4.
The final day of the Summit kicked off with three presentations on academic research from Binghamton University, the University of Illinois at Urbana-Champaign, and Kansas State University. Rounding out the morning were three presentations that returned to the day two theme of assured systems from Kestrel, Cog Systems, Inc., and RTI. The afternoon began with some challenges in using seL4 followed by a discussion of the CoE progress and the way ahead. The Summit then concluded with four presentations from Data61 discussing the new formed seL4 Foundation and the latest updates in seL4 development.
2020 Summit Agenda
Monday, November 16, 2020
Chair & Time
Session #1 – Introduction and Keynote Dr. Renato Levy
Opening Remarks and Introduction to Keynote Speaker
(Dr. Renato Levy, Intelligent Automation Inc.; Dr. Jason Li, Siege Technologies) 09:00AM – 09:15AM
Video
Keynote 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
(Prof. Kevin Hamlen, University of Texas at Dallas)
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 Richards
Introduction 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
We use cookies to enable essential functionality on our website, and analyze website traffic. By clicking Accept you consent to our use of cookies. Read about how we use cookies.
Your Cookie Settings
We use cookies to enable essential functionality on our website, and analyze website traffic. Read about how we use cookies.
Cookie Categories
Essential
These cookies are strictly necessary to provide you with services available through our websites. You cannot refuse these cookies without impacting how our websites function. You can block or delete them by changing your browser settings, as described under the heading "Managing cookies" in the Privacy and Cookies Policy.
Analytics
These cookies collect information that is used in aggregate form to help us understand how our websites are being used or how effective our marketing campaigns are.