Email: jgancher@andrew.cmu.edu
CV
I am a postdoc at Carnegie Mellon University, advised by Bryan Parno. I obtained my PhD from Cornell University, co-advised by Elaine Shi and Greg Morrisett.
My research is about using techniques from formal methods and program verification to certify cryptographic implementations and proofs.
I am on the job market this year! Please reach out if your
department is hiring. You can find my application materials
here.
Preprints/Publications:
WaveCert: Formal Compiler Validation for Asynchronous Dataflow
Programs.
In submission.
Zhengyao Lin, Joshua Gancher, and Bryan Parno.
Secure Synthesis of Distributed Cryptographic Applications.
To appear at CSF 2024.
Coşku Acay, Josua Gancher, Rolph Recto, and Andrew Myers.
Owl:
Compositional Verification of Security Protocols via an
Information-Flow Type System.
IEEE S&P 2023.
Joshua Gancher, Sydney Gibson, Pratap Singh, Samvid
Dharanikota, and Bryan Parno. Project link
here.
A Core Calculus for Equational Proofs of Cryptographic
Protocols.
POPL 2023.
Joshua Gancher, Kristina Sojakova, Xiong Fan, Elaine Shi, and
Greg Morrisett. Project link
here.
Viaduct: An Extensible, Optimizing Compiler for Secure
Distributed Programs.
PLDI 2021.
Coşku Acay, Rolph Recto, Joshua Gancher, Andrew Myers,
and Elaine Shi. Project link
here.
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.