packnback

Rust HACL

Having chosen rust as the language to implement packnback with, I needed a high quality implementation of the Nacl cryptographic api.

Luckily, I had previously read about the High-Assurance Cryptographic Library which uses the F* language and formal verification to produce a C library and thought I could use this as an opportunity to learn about the Rust C ffi.

Here is the first bit of code. After finishing this, I found someone else had the same idea, but for now I want to maintain control over this dependency and it’s wrapper.

I made some small additions to the C api while playing with rust:

  • Rust naming conventions for types.
  • Boxing (unique pointers) secret keys to minimize accidental possible copies in memory.
  • Wiping secret keys on drop.
  • Misuse resistant type wrappers around Secret/Public keys.
  • Assertions around api preconditions.

This project relies on sponsors and donations to survive, consider donating.