search

GaloisInc / cryptol-specs

A central repository for specifications of cryptographic algorithms in Cryptol
BSD 3-Clause "New" or "Revised" License
34 stars 7 forks source link

very few specs include properties #32

Open kiniry opened 3 years ago

kiniry commented 3 years ago

We have tons of non-trivial properties specified for various algorithms. Sharing specs with properties permits us to easily demonstrate the power and utility of stating and having assurance about theorems in order to ensure that a specification is validated, as well as to help drive an assurance case of an implementation of the algorithm. We should endeavor to include these properties in our public specs.

weaversa commented 3 years ago

At the very least, each spec should come with test vectors. Also, remember that the :safe command adds assurance to any Cryptol function by showing it is total (defined for all inputs).

On Fri, Nov 13, 2020 at 4:07 PM Joseph Kiniry notifications@github.com wrote:

We have tons of non-trivial properties specified for various algorithms. Sharing specs with properties permits us to easily demonstrate the power and utility of stating and having assurance about theorems in order to ensure that a specification is validated, as well as to help drive an assurance case of an implementation of the algorithm. We should endeavor to include these properties in our public specs.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/GaloisInc/cryptol-specs/issues/32, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABYQSOWDH3IL5OMBMF7LVNLSPWNXJANCNFSM4TVBRAAQ .

robdockins commented 3 years ago

Indeed; test vectors should be an absolute minimum. For AES, SHA-2 and ECDSA, I spent a fair amount of time munging some of the public NIST test vectors into Cryptol syntax to validate the new primitive implementations. They could pretty easily be reused here, I think.

https://github.com/GaloisInc/cryptol/tree/master/tests/suiteb