PhD candidate in Computer Science at Princeton University
I study how we can use operating systems and programming languages to make software safer, more secure, and more reliable.
My work includes projects to facilitate safe interactions between Rust, foreign languages, and concurrent hardware. I am a core maintainer of the Tock operating system, which is used as a root of trust on tens of millions of devices.
I am advised by Amit Levy in the SNS Research Group and collaborate closely with Mae Milano.
Using foreign libraries shouldn’t mean giving up Rust’s safety guarantees. Omniglot combines memory isolation, type validation, and static checks to preserve those guarantees—even with unmodified, untrusted libraries, and without copying shared data. We demonstrate it in Linux applications and the Tock kernel.
OSDI ’25 · Best Paper Award
I am a core maintainer of Tock, a secure operating system for embedded devices. My contributions span the kernel’s application-memory interfaces, RISC-V memory protection, and sound abstractions for DMA—helping preserve Rust’s safety guarantees across interactions with untrusted applications and hardware.
SOSP ’25 · From research to deployed systems
Embedded software is difficult to test automatically, especially across chips and boards developers don’t have locally. I’m building Treadmill to make automated testing on real hardware accessible, with remote access for interactive development and debugging.
An introduction to Omniglot’s motivation and approach to safely using untrusted foreign libraries from Rust.
How Rust’s aliasing rules interact with mutexes, atomics, and interior mutability.
Keeping Phoenix streaming connections alive with heartbeats and per-request Cowboy timeouts.
Separating Emacs and its applications into systemd scopes to isolate memory pressure.
I implemented a 64-bit XGMII PHY for 10 Gb Ethernet, hardware packet timestamping, and GMII/XGMII simulation. I also ported the full XGMII adapter to Verilog.
I introduced declarative sudo rules and TPM2 integration.
I improved Verus’s support for Rust smart pointers and generic specification methods, fixed a coercion bug that disrupted proofs, and enabled running it without rustup.
I fixed an aliasing violation during thread-local storage teardown and a thread-exit race that could write into a replacement process’s memory.
I fixed an overflow in RISC-V memory-protection region calculations, uncovered through Tock’s simulation tests.
I fixed enabling experimental configuration-file includes from Cargo’s configuration itself.
At Princeton, I’ve served as a teaching assistant for COS316 (Fall ’23), COS518 (Spring ’24), and COS417 (Spring ’26), leading recitations, holding office hours, and advising undergraduate and graduate course projects. I’ve also had the opportunity to give guest lectures on:
I like tinkering with electronics, networking hardware, and servers. I volunteer at Selfnet e.V., a student-run internet service provider, where I administer a few services and servers.
Away from computers, I enjoy hiking and biking, and dabble in playing the bass guitar. A favorite hike was up Mt. Hallasan on Jeju Island.
I’m always happy to chat or collaborate on secure computer systems, networking, system administration, and embedded systems. Reach me at leon@is.currently.online.