Sydney Gibson

sydgibs [at] gmail [dot] com

Blog | CV

Hello! I'm Sydney Gibson. I am a software engineer at Aurora.

I was previously a Ph.D. student in the Computer Science Department at Carnegie Mellon, advised by Bryan Parno. My research focused on formal methods for verifying safety and security properties of low-level, high-performance systems, and on developing new ways of doing so at scale.

During my time in academia I was a doctoral researcher at Google, where I formally verified cryptographic security routines for the OpenTitan chip. I was also a member of the Everest Project.

I received my B.S. and M.Eng. from the Electrical Engineering and Computer Science Department at MIT. While I was there, I worked with the Parallel and Distributed Operating Systems group.

Feel free to email me, follow me and/or message me on Twitter, or see what I'm up to on Github.

Galápagos: Developing Verified Low Level Cryptography on Heterogeneous Hardwares
Yi Zhou, Sydney Gibson, Sarah Cai, Menucha Winchell, Bryan Parno
ACM CCS 2023 | November 2023 | To Appear

Owl: Compositional Verification of Security Protocols via an Information-Flow Type System
Joshua Gancher, Sydney Gibson, Pratap Singh, Samvid Dharanikota, and Bryan Parno
IEEE S&P 2023| May 2023 | Preprint

Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic
Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido MartĂ­nez, Denis Merigoux, and Tahina Ramananandro
ICFP 2021 | August 2021 | Paper

Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language
Jay Bosamiya, Sydney Gibson, Yao Li, Bryan Parno, and Chris Hawblitzel
VSTTE 2020 | July 2020 | Paper