Third Annual Summit Technical Program
November 15-19, 2020
- 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
Monday, November 16, 2020
- 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
- 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
- Dr. Lennart Beringer, Princeton University
- Dr. Sergey Bratus, DARPA
- Prof. Kevin Hamlen, University of Texas at Dallas
- Prof. Gernot Heiser, UNSW and Data61
Tuesday, November 17, 2020
- 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
- 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)
Wednesday, November 18, 2020
- 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)
- 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)
- 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
- 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