University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Verified Software Toolchains: Fiat-Cryptography

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Verified Software Toolchains: Fiat-Cryptography

Download to your calendar using vCal

If you have a question about this talk, please contact nobody.

VSO2 - Verified software

Big-integer modular arithmetic is surprisingly tricky to implement efficiently in cryptographic software.  Ten years ago, all such implementations for elliptic-curve crypto were coded by hand from scratch for each new prime modulus.  Our Fiat Cryptography project showed how to automate that process with a Coq-verified compiler, which has since been adopted for small but important parts of all major web browsers.  I will introduce the different techniques: a mix of data-structure verification, partial evaluation, and classic verified-compiler phases.

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Lecture Theatre 6, Department of Engineering Senior Parlour, Gonville & Caius College Room FW11, Computer Laboratory, William Gates Building Zoom Link: https://cl-cam-ac-uk.zoom.us/j/4361570789?pwd=Nkl2T3ZLaTZwRm05bzRTOUUxY3Q4QT09&from=addon.

Other talks

Title to be confirmed title abstract tba Group Work Kirk Public Lecture | A proxy window into the beautiful and challenging world of causal attribution The uplift and erosion history of the Gamburtsev Subglacial Mountains and their role in the formation of the East Antarctic Ice Sheet Scientific Steering Committee meeting
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity