Introducing HacSpec (“specification language for cryptographic primitives”)

Introducing HacSpec by Franziskus Kiefer.

From the post:

HacSpec is a proposal for a new specification language for cryptographic primitives that is succinct, that is easy to read and implement, and that lends itself to formal verification. It aims to formalise the pseudocode used in cryptographic standards by proposing a formal syntax that can be checked for simple errors. HacSpec specifications are further executable to test against test vectors specified in a common syntax.

The main focus of HacSpec is to allow specifications to be compiled to formal languages such as cryptol, coq, F*, and easycrypt and thus make it easier to formally verify implementations. This allows a specification using HacSpec to be the basis not only for implementations but also for formal proofs of functional correctness, cryptographic security, and side-channel resistance.

The idea of having a language like HacSpec stems from discussions at the recent HACS workshop in Zurich. The High-Assurance-Cryptographic-Software workshop (HACS) is an invite-only workshop co-located with the Real World Crypto symposium.

Anyone interested in moving this project forward should subscribe to the mailing list or file issues and pull requests against the Github repository.

Cryptography projects should be monitored like the NSA does NIST cryptography standards. If you see an error or weakness, you’re under no obligation to help. The NSA won’t.

Given security fails from software, users, etc., end-to-end encryption resembles transporting people from one homeless camp to another in an armored car.

Secure in transit but not secure at either end.

Leave a Reply

You must be logged in to post a comment.