New Verified ChaCha20-Poly1305 Paper

New Verified ChaCha20-Poly1305 Paper

[Aleksa Sarai]

[-- Attachment #1.1: Type: text/plain, Size: 783 bytes --]

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/>

[-- Attachment #1.2: signature.asc --]
[-- Type: application/pgp-signature, Size: 833 bytes --]

[-- Attachment #2: Type: text/plain, Size: 148 bytes --]

_______________________________________________
WireGuard mailing list
WireGuard@lists.zx2c4.com
https://lists.zx2c4.com/mailman/listinfo/wireguard