Program Committee

Lucy Fletcher is a Secure Kernel Engineer at Apple based in Sydney, Australia, working on L4 microkernels and the surrounding ecosystems. Before joining Apple, she studied Computer Science at UNSW and worked with the Trustworthy Systems group, where she focused on the design and development of the seL4 device driver framework. She is passionate about giving back to the seL4 community and supporting its continued growth.

Mostly have done work with separation technologies, especially Xen and seL4.

I work for the National Cyber Security Centre (NCSC) of the UK as lead of the Verification Research Team. We investigate tools, techniques and technologies based around formal methods and provable security that can be leveraged to make the UK the safest place to live and work online.

David is an early contributor to the seL4 microkernel, having contributed both the first C implementation and seminal formal-verification work. He holds a Ph.D. from the University of New South Wales where his research included probabilistic and non-functional properties of seL4 such as side channels. As a senior researcher at ETH Zurich, he also led the team that built the Enzian research computer.

Juliana Furgala is a technical staff member in the Secure Resilient Systems and Technology Group. Currently she is researching secure and recoverable satellite systems. Interested in the pursuit of technology built with security in mind, she aims to develop lasting technology that can stand the test of adversaries, not just the test of time. Her recent published research focuses on the needs of embedded and real-time systems.

Furgala received her MS degree in cybersecurity in 2024 from Georgia Institute of Technology and her BS degree in computer science in 2019 from Tufts University, where she also minored in history with a focus on global premodern women’s history. In 2018 she interned at MITRE, where she began her journey of studying satellites. There she developed technology to enable GPS receivers to directly communicate satellite information with each other without needing further satellite access, assuming that one receiver has prior data stored.

David S. Hardin has made contributions in the areas of formal methods, computer architecture for High Assurance systems, as well as memory-safe programming languages. He is currently Chief Technologist for Trusted Methods in the Applied Research and Technology organization at Collins Aerospace, where he has served as Principal Investigator or Researcher for several U.S. DoD Research and Development programs. He most recently contributed to the DARPA Cyber-Assured Systems Engineering program (CASE).

He is the editor of the book Design and Verification of Microprocessor Systems for High-Assurance Applications (Springer 2010), and a co-author of The Real-Time Specification for Java. He is author or co-author of more than 75 peer-reviewed publications, and is an inventor or co-inventor on 15 U.S. patents. In 1999, Dr. Hardin co-founded aJile Systems, a startup company focused on real-time and embedded Java technology, and served as aJile’s Chief Technical Officer from 1999 to 2003.

Dr. Hardin was selected as a Rockwell Engineer of the Year for 1997 for his contributions to the development of the world’s first Java microprocessor. His academic career includes BSEE and MSEE degrees from the University of Kentucky, and a Ph.D. in Electrical and Computer Engineering from Kansas State University, in 1989. Dr. Hardin is a proud native of the Commonwealth of Kentucky, and is a Kentucky Colonel.

Gernot leads the Trustworthy Systems group. He aims for principled, fundamental solutions to real-world problems, meaning his activities range from fundamental research to technology transfer and real-world deployment.

He sees research-driven teaching as a core part of this agenda, challenging students to grow, recruiting them into research and sending them out into the real world as ambassadors of TS and its technologies, and helping to advance the growth of industrial cybersecurity capabilities.

Most of his work is on seL4 and related technologies, and evangelising them is a significant part of his activities.

Corey was a senior proof engineer and the lead engineer for verifying multi-core seL4. During his time at TS he has been involved in a wide variety of projects to do with seL4. These include developing the original CapDL translation tools, helping complete the information flow proofs, and contributing to the verification of the seL4 MCS extensions. His research interests include formal methods, functional programming, and program verification. Corey now works at Proofcraft.

Computer engineer with an interest in operating systems, cybersecurity, microkernels, virtualisation, electronics, computer architecture and hardware design

I am an independent computer security researcher based in Portland, Oregon.

My interests include operating systems, formal methods, programming languages, and reverse engineering.

These days, most of my time at work is spent hacking on and around seL4, the formally verified microkernel. Right now I’m working on binary verification and seeding the seL4 userspace ecosystem with support for the Rust programming language.

I offer my consulting services through Colias Group, LLC.