Formal verification

[tarcieri]

It would be nice to formally verify Miscreant's implementations of algorithms (e.g. CMAC, PMAC), and in particular verify the Rust version.

Galois Cryptol may be useful here:

https://cryptol.net/

My understanding is given a Cryptol description of an algorithm, Galois' Software Analysis Workbench tool could potentially formally prove equivalence to e.g. the Rust implementation:

https://saw.galois.com/

[ranweiler]

Hi! FYI, I'm currently looking into this, and starting a conversation with my former coworkers about the state of Rust verification via SAW/Cryptol.

[tarcieri]

@ranweiler great news! I'd probably suggest starting with the cmac and pmac crates from the RustCrypto project:

https://github.com/RustCrypto/MACs