The first day of the event included nine presentations by government, industry, and academia experts discussing a variety of topics specifically related to the seL4® microkernel. Discussed were an overview of the seL4 microkernel, continued plans for the seL4 Center of Excellence and related seL4 ecosystem topics, an extended introduction to Formal Verification, and Government efforts related to seL4. On the second day of the event, the keynote speaker, Professor Edward Lee from the University of California at Berkeley spoke about Deterministic Concurrency and Its Role in Assurance. Other sessions on the second day included topics about Assured System, Formal Verification, and academia efforts related in the seL4 ecosystem. Todd Carpenter of Adventium Labs moderated a lively seL4 CoE Expert Panel Discussion that received much interested from attendees.
On the third day of the event, attendees had the option of continuing with the “General Session” track containing further presentations, or, attendees could choose the “Training Session” track, which provided a more “hands-on” approach. Both tracks conveyed a substantial amount of information regarding seL4. The hands-on portion of the training sessions occurred on the third and fourth days of the seL4 Summit event. The third day was the final day of the General Session track, and discussed that day were a second round of presentations regarding academia efforts related to seL4 technology. A second and third round of talks that were placed in the “Assured Systems” category were also presented. The General Session concluded with summaries about the “Center of Excellence” and planned directions forward in future years.
For the Training Session track, Nathan Studer, Chris Guikema, and Alex Pavey from DornerWorks Ltd. led a series of presentations with both lecture and labs components. Lecture presentation material began with a general background discussing microkernels, followed by advantages, disadvantages, and common characteristics of microkernels. After a seL4 kernel overview, the lecturers led the class into a deep dive about the seL4 user space and seL4 processes. Development environments were discussed, a CAmkES overview was provided and the lecturers covered the topic of porting and concluded with a discussion of using U-boot on the i.MX8. Instructors also provided students lab materials covering seL4 topics like:
Building an seL4 system
Adding a hardware resource to seL4
Debugging applications with GDB
Adding a network stack / Adding TCP to the network stack