New Verified ChaCha20-Poly1305 Paper

[Aleksa Sarai]

I just saw this paper[1] which claims to have an implementation of
ChaCha20-Poly1305 in vectorised assembly using a method which
"deliver[s] formally verified vectorized implementations which
outperform the fastest non-verified code"

Is there any interest in using this for Zinc (it's my understanding[2]
that the ChaCha20 and Poly1305 code in Zinc is *not* formally verified)?
The repo is [3]. It looks like they don't have verified generic C
implementations unfortunately, but aren't there verified C versions in
HACL*?

[1]: https://arxiv.org/abs/1904.04606
[2]: https://marc.info/?l=linux-kernel&m=155405777331772&w=2
[3]: https://github.com/tfaoliveira/libjc

-- 
Aleksa Sarai
Senior Software Engineer (Containers)
SUSE Linux GmbH
<https://www.cyphar.com/>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: not available
URL: <http://lists.zx2c4.com/pipermail/wireguard/attachments/20190506/5a4361aa/attachment.asc>