Sat 22 Jan 2022 14:30 - 14:50 at Salon I - Contributed Talk (Afternoon) Chair(s): Amin Timany

Currently, the IETF standardizes cryptographic primitives using pseudo-code. The correctness of an implementation of such a standard is safe-guarded by unit tests and reference implementations. Hacspec improves on this by replacing pseudo-code by a subset of rust with a precise operational semantics. Similarly, the Fiat Cryptogrphy library allows one to synthesize efficient correct-by-construction implementations. We contribute a Coq-backend for hacspec and connect the two projects using bedrock2, as well as a printer from the bedrock’s C-like language to Rust. Thus we provide a pipeline from hacspec to optimized, safe Rust. As a feasibility study, we apply the pipeline to the BLS elliptic curve, used for signatures.

Abstract (coqpl22-final61.pdf)157KiB

Sat 22 Jan

Displayed time zone: Eastern Time (US & Canada) change

14:30 - 14:50
Contributed Talk (Afternoon)CoqPL at Salon I
Chair(s): Amin Timany Aarhus University
A Verified Pipeline from a Specification Language to Optimized, Safe RustRemote
S: Rasmus Holdsbjerg-Larsen Aarhus University, Bas Spitters Aarhus University, Mikkel Milo Concordium Blockchain Research Center, Aarhus University
Pre-print File Attached