I am a PhD candidate in Computer Science at Cornell University, co-advised by Elaine Shi
and Greg Morrisett
My research is about using techniques from formal methods and program verification to certify proofs in cryptography.
Viaduct: An Extensible, Optimizing Compiler for Secure
To appear at PLDI 2021.
Coşku Acay, Rolph Recto, Joshua Gancher, Andrew Myers, and Elaine Shi.
IPDL: A Simple Framework for Formally Verifying Distributed Cryptographic Protocols.
In submission to USENIX 2021.
Greg Morrisett, Elaine Shi, Kristina Sojakova, Xiong Fan, and Joshua Gancher. 1
Symbolic Proofs for Lattice-Based Cryptography. CCS 2018.
Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grégoire, Charlie Jacomme and Elaine Shi.
- Externally Verifiable Oblivious RAM. PETS 2017.
Joshua Gancher, Adam Groce, and Alex Ledger.