• Home
  • About
    • Bylaws
    • Organization Structure
    • Organizing Committee
    • Privacy Policy
  • Membership
    • Apply for Membership
    • Membership Info
    • Our Members
  • Summits
    • 2022 Summit
    • 2020 Summit
    • 2019 Summit
    • 2018 Summit
  • Resources
    • About seL4®
    • seL4® Foundation
    • TCCoE Repository
  • Training
  • Contact

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.
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
Sunday, Nov. 15 | Monday, Nov. 16 | Tuesday, Nov. 17 | Wednesday, Nov. 18
Sunday, November 15, 2020
Training Day Chat Transcript | Training- COMING SOON!
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
  • Video | Chat Transcript
  • CPS Security and Resilience: Viewpoint from ONR (Dr. Ryan Craven, ONR) 11:00AM – 11:30AM
  • Video | Chat Transcript
  • To ARM and Beyond: Embedding seL4 in the Air Force (Kyle Tillotson, AFRL) 11:30AM – 12:00PM
  • Presentation | Video 1 | Video 2 | Chat Transcript
  • Government Support of seL4 Ecosystem (Dr. Ray Richards, DARPA) 12:00PM – 12:30PM
  • Presentation | Video | Chat Transcript
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
  • Presentation | Video 1 | Video 2 | Chat Transcript
  • Defense in Depth: Building 21st Century Secure Systems with PIPE 13:30PM – 14:00PM (Dr. Arun Thomas and Chris Casing, Draper Laboratory)
  • Video | Chat Transcript
  • VST+DeepSpec: connecting a program logic to a verified OS kernel 14:00PM – 14:30PM (Dr. Lennart Beringer, Princeton University)
  • Video | Chat Transcript
  • Strengthening Binary Software Verification with Certified Code Transforms 14:30PM – 15:00PM
(Prof. Kevin Hamlen, University of Texas at Dallas)
  • Video | Chat Transcript
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
  • Video: Panel & Closing Remarks | Chat Transcript
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
  • Video | Chat Transcript
  • Challenges to the Industrial Adoption of seL4 (James Potts and Mark Bortz, Collins Aerospace) 11:00AM – 11:30AM
  • Video | Chat Transcript
  • 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)
  • Video | Chat Transcript
  • The Need for Assured Execution – The Future of Code Has No Source (Matt Mickelson, MITRE) 12:00PM – 12:30PM
  • Video | Chat Transcript
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
  • Presentation | Video | Chat Transcript
  • Building a Commercial Virtualized Mobile Device with seL4 13:30PM – 14:00PM (Jason Sebranek and Yanyan Shen, Cog Systems, Inc.)
  • Video | Chat Transcript
  • 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)
  • Presentation | Video 1 | Video 2 | Chat Transcript
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
  • Video: Panel & Closing Remarks | Chat Transcript
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
  • Video | Chat Transcript
  • Building A Trusted Execution Environment for In-Storage Computing 09:30AM – 10:00AM (Prof. Jian Huang, University of Illinois at Urbana-Champaign)
  • Video | Chat Transcript
  • HAMR - High-Assurance Modeling & Rapid Engineering for seL4-based Embedded Systems Using AADL 10:00AM – 10:30AM (John Hatcliff and Robby, Kansas State University)
  • Presentation | Video | Chat Transcript
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
  • Presentation | Video | Chat Transcript
  • Virtualization and Customer Value (Carl L. Nerup, Cog Systems, Inc.) 11:30AM – 12:00PM
  • Video | Chat Transcript
  • A Secure Distributed Computing Middleware for the seL4 Ecosystem 12:00PM – 12:30PM (Dr. Paul Pazandak and Fabrizio Bertocci, RTI)
  • Presentation | Video | Chat Transcript
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)
  • Presentation | Video | Chat Transcript
  • Building of the Training: the challenge and path to success (Ammar Salman, IAI) 13:30PM – 14:00PM
  • Presentation | Video | Chat Transcript
  • Center of Excellence Progress and Way Forward (Jerry Dussault, Griffiss Institute) 14:00PM – 14:30PM
  • Presentation | Video | Chat Transcript
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
  • Video | Chat Transcript
  • Systems beyond POSIX (Curtis Millar, Data61) 15:30PM – 16:00PM
  • Presentation | Video | Chat Transcript
  • The seL4 Core Platform (Ben Leslie, Breakaway Consulting; Gernot Heiser, Data61) 16:00PM – 16:30PM
  • Presentation | Video | Chat Transcript
  • seL4 Device Driver Framework (Dr. Ihor Kuz, Data61) 16:30PM – 17:00PM
  • Video | Chat Transcript
Closing Remarks (Dr. Ray Richards, DARPA) 17:00PM – 17:15PM Video
seL4 is a trademark of LF Projects, LLC. Trusted Computing Center of Excellence™ is a tradename of The Computing Center of Excellence, Inc. Copyright © 2022 The Computing Center of Excellence, Inc.

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.