A Verified Pipeline from a Specification Language to Optimized, Safe Rust
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.
Sat 22 JanDisplayed time zone: Eastern Time (US & Canada) change
14:30 - 14:50
|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 UniversityPre-print File Attached