1432431 - Land Cryptol/SAW specs for Poly1305

Status: RESOLVED FIXED

(NSS :: Test, enhancement)

Description

[Tim Taubert [:ttaubert] (inactive)]

I wrote Cryptol and SAW specs for Poly1305 that are able to verify our implementations for a single input/key pair. The 128-bit multiplication isn't verifiable as-is. It takes forever, probably literally. We would need to take the HACL* approach and gently guide Z3 to link the mathematical spec to the optimized spec.

Let's not do this now, let's just land the specs so we have them in the repo.

Comment 1

[Tim Taubert [:ttaubert] (inactive)]

https://treeherder.mozilla.org/#/jobs?repo=nss-try&revision=0dd223772b19928d4bc4889de275b4ed610a43d6

Comment 2

[Phabricator Automation]

Comment on attachment 8944672 [details]
Bug 1432431 - Land Cryptol/SAW specs for Poly1305 r=franziskus

Franziskus Kiefer [:fkiefer or :franziskus] has approved the revision.

https://phabricator.services.mozilla.com/D430

Comment 3

[Phabricator Automation]

Comment on attachment 8944672 [details]
Bug 1432431 - Land Cryptol/SAW specs for Poly1305 r=franziskus

Franziskus Kiefer [:fkiefer or :franziskus] has approved the revision.

https://phabricator.services.mozilla.com/D430#10707

Comment 4

[Tim Taubert [:ttaubert] (inactive)]

https://hg.mozilla.org/projects/nss/rev/28bc767eccd1

Comment 5

[Martin Thomson [:mt:]]

Hey Tim, do you think that there is any value in providing a tool for building and running these?

Comment 6

[Tim Taubert [:ttaubert] (inactive)]

(In reply to Martin Thomson [:mt:] from comment #5)
> Hey Tim, do you think that there is any value in providing a tool for
> building and running these?

We actually have a tool, or rather a Docker image called "docker-saw" that runs ChaCha20 and bmul verification already:

https://phabricator.services.mozilla.com/D388

I wrote the Poly1305 specs to test whether we can (re-)verify that code too, although I was quite sure it wouldn't work as-is. We need to help z3 along here, and I haven't found the time to do that yet. I tried with bmul64() but wasn't very successful thus far.