seL4 `

International seL4 Workshop

Given the growth in the community we are starting an annual international seL4 workshop where we can all come together to share and learn what is being done with seL4.

Unlike the previous developers days, the focus will be much more on what is happening with seL4 and what interesting things are being done using seL4 rather than a learning or tutorial event.

We'd like participants to join and:

First International seL4 Workshop


Where: HRL Laboratories 3011 Malibu Canyon Rd, Malibu, CA, USA
When: Thursday 15 December 2016
Who: People interested in talking or hearing about work being done with seL4
Cost: Free. Note: We may be able to provide students with financial assistance for travel. If you require such assistance, please let us know on the registration form.
Registration:    Closed

Notes and Slides

Corey Richardson has written up some notes about the workshop.

The slides form the workshop are linked below in the Agenda.


8:30 - 9:00 arrival and registration
9:00 - 9:15 opening and welcome
9:15 - 9:45 High-assurance software for autonomous ground systems. Aleksey Nogin, HRL
9:45 - 10:45 The seL4 Status Report.Gernot Heiser, Data61
10:45 - 11:15 break
11:15 - 12:00 Robigalia: Rust, seL4, and persistent capabilities. Corey Richardson, Clarkson University
12:00 - 13:00    lunch
13:00 - 13:45 Hybrid Design for Remote Attestation (Using a Formally Verified Microkernel). Norrathep Rattanavipanon, University of California, Irvine
13:45 - 14:30 Data Distribution for seL4. Andrea Sorbini, Real-Time Innovations Inc.
14:30 - 15:00 break
15:00 - 15:45 Debugging seL4 with GDB. Chris Guikema, DornerWorks
15:45 - 16:15 Virtualisation on seL4 Ihor Kuz, Data61
16:15 - 17:00 Discussion of seL4 'gaps'. Everyone
17:00 Close


HRL Travel Guide including accommodation around HRL.

Make sure to bring a government-issued id (for access to HRL).

Non-US people must bring a passport and should arrive at least 20 minutes in advance.


This workshop is sponsored by the Center for Secure and Resilient Systems at HRL Laboratories, LLC, and by Data61.