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:
|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.|
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|
Directions to HRL. HRL encourages people to carpool where possible.
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.