Jonathan Protzenko的肖像

Jonathan Protzenko

Principal Researcher

关于

See my personal web page (opens in new tab) for an up-to-date list of publications, and more information about my current projects.

I am a Principal Researcher in the RiSE group, which I joined in Fall 2014. Previously, I was at INRIA Paris (opens in new tab) from 2010 to 2014.

Learn more about my work in the press: Quanta Magazine (opens in new tab), IEEE Explore! (opens in new tab), CACM (opens in new tab)

Projects:

  • Computational Law (Catala): bringing the rigor of formal methods to the legal world, specifically statutory law.
  • Verified Protocol Stacks (Noise*, Signal*, MLS*): low-level, efficient, verified implementations of popular cryptographic protocols.
  • Low-Level Programming in F* (a.k.a. Low*): I wrote KaRaMeL (née KReMLin) (opens in new tab), a compiler from Low* to C (opens in new tab), and co-lead several high-profile projects written in Low*, such as: HACL*, EverCrypt, EverQUIC, parts of which have been integrated into Windows, Linux, Firefox, Tezos, mbedTLS, and many more.

On my free time, I maintain several open-source projects, including a Thunderbird addon (opens in new tab) that now has 200,000 users.

 

精选内容

Scaling the Everest of software security with Dr. Jonathan Protzenko

Scaling the Everest of software security with Dr. Jonathan Protzenko

Episode 58, January 9, 2019 - Dr. Protzenko talks about what’s wrong with software (and why it’s vitally important to get it right), explains why there are so many programming languages (and tells us about a few he’s been working on), and finally, acts as our digital Sherpa for Project Everest, an assault on software integrity and confidentiality that aims to build and deploy a verified HTTPS stack.