Third Annual Summit Technical Program
November 15-18, 2020
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.
2024 Summit Agenda
Sunday, Nov. 15 | Monday, Nov. 16 | Tuesday, Nov. 17 | Wednesday, Nov. 18