Fiat Cryptography: A Code-Generation Approach to Correct-by-Construction Cryptography
Duration: 28 mins 46 secs
Share this media item:
Embed this media item:
Embed this media item:
About this item
| Description: |
Chlipala, A
Thursday 13th May 2021 - 17:30 to 18:00 |
|---|
| Created: | 2021-05-18 13:41 |
|---|---|
| Collection: | Verified software: from theory to practice |
| Publisher: | Isaac Newton Institute for Mathematical Sciences |
| Copyright: | Chlipala, A |
| Language: | eng (English) |
| Abstract: | Big-integer modular arithmetic is at the heart of many cryptographic algorithms. Often the modulus is known in advance, in which case code can be quite specialized for performance reasons, and in fact experts have typically reimplemented classic algorithms from scratch in C or assembly, for each combination of modulus and hardware word size. Our Fiat Cryptography project showed a better way: a formally verified compiler that specializes implementations from algorithm libraries. Since our initial open-source release, Fiat Cryptography has been adopted for elliptic-curve operations in both Chrome and Firefox, the Linux kernel, and the Go standard library. I will sketch how we get world-performance-champion C code via partial evaluation of purely functional programs, with machine-checked proof via the Coq proof assistant. |
|---|---|
Available Formats
| Format | Quality | Bitrate | Size | |||
|---|---|---|---|---|---|---|
| MPEG-4 Video | 640x360 | 443.57 kbits/sec | 93.46 MB | View | Download | |
| WebM | 640x360 | 253.19 kbits/sec | 53.38 MB | View | Download | |
| iPod Video | 480x270 | 489.43 kbits/sec | 103.12 MB | View | Download | |
| MP3 | 44100 Hz | 249.86 kbits/sec | 52.68 MB | Listen | Download | |
| Auto * | (Allows browser to choose a format it supports) | |||||