Name: Where are we with Time Protection? Verification and Cross-domain Communication Update - Rob Sison, UNSW Sydney
Start: 2026-09-02T14:30:00-0700
End: 2026-09-02T15:00:00-0700

1 - 3 September | Vancouver, Canada BC
View More Details & Registration
The schedule is subject to change, so please check back before the event for the most up-to-date information.

Please note that all session times are listed below in Pacific Daylight Time (PDT), UTC-7.

Where are we with Time Protection? Verification and Cross-domain Communication Update - Rob Sison, UNSW Sydney

Wednesday September 2, 2026 14:30 - 15:00 PDT

Plaza A & B

This talk will give an update on the past two years’ advances at Trustworthy Systems in (1) our ongoing efforts to verify time protection for seL4, as well as (2) our implementation in seL4 of new time-protected cross-domain communication mechanisms on RISC-V Cheshire. On the formal verification front, I will present our results so far, thanks to a crucial rethink of our approach to verifying a key aspect of time protection for seL4 down to its C implementation, which has eliminated the main cause of the project’s previously large number of breakages to seL4’s existing correctness proofs. On the OS kernel design and development front, I will present both legacy and hardware-supported implementation options we evaluated for seL4 to support cross-domain shared memory and notification mechanisms that ensure one-way communications are truly one way, without permitting any timing channels in either (but most importantly, the backwards) direction. I will also remark on where we stand and next steps forward to formalise and verify that time protection is enforced by these new mechanisms.

Speakers

Rob Sison

Senior Research Associate, UNSW

Rob is a postdoc at UNSW Sydney who researches and develops formal methods, primarily for proving absences of information flow in systems for high-assurance use cases. In the past, their focus was on complications arising from concurrency and refinement to enable secure compilation... Read More →

Wednesday September 2, 2026 14:30 - 15:00 PDT
Plaza A & B

General Sessions, Advances in seL4 Security Verification and R&D

seL4 Summit 2026

Rob Sison

Get help with the event

seL4 Summit 2026

Rob Sison

Sign up or log in to save this to your schedule, view media, leave feedback and see who's attending!

Get help with the event