Re: [PATCH net-next v9 00/19] WireGuard: Secure Network Tunnel

[Eric Biggers]

On Sun, Mar 31, 2019 at 08:18:13PM +0200, Jason A. Donenfeld wrote:
> On Sat, Mar 30, 2019 at 6:53 AM Eric Biggers <ebiggers@xxxxxxxxxx> wrote:
> > poly1305-simd is among the failing algorithms because it loses carry bits when
> > handling long "all 0xff bytes" inputs.  poly1305-avx2-x86_64.S is definitely
> > broken, and poly1305-sse2-x86_64.S *might* be too.  I am working on a patch...
> 
> Yea.... yikes. I'm kind of souring on this plan of having to deal with
> that code in Zinc, versus the extensively studied, fuzzed, and
> scrutinized code from Andy. Subtle carry bugs like that are kind of a
> testament to my overall plan of preferring formally verified or
> heavily used implementations to bespoke ones. This stuff is hard to
> get right.
> 
> Jason

I agree that Andy's Poly1305 code is better and we should probably switch to it,
but to be fair it's also longer and more complex, and I think you overestimate
the extent to which it's actually been "studied, fuzzed, and scrutinized".  Andy
previously made essentially the same mistake in three of his Poly1305
implementations as well, which he had to fix:
https://mta.openssl.org/pipermail/openssl-commits/2016-April/006639.html

Also OpenSSL's PowerPC implementation of AES-CTR that was incorporated into the
kernel was incorrect, as was recently fixed by

	commit dcf7b48212c0fab7df69e84fab22d6cb7c8c0fb9
	Author: Daniel Axtens <dja@xxxxxxxxxx>
	Date:   Fri Mar 15 13:09:01 2019 +1100

	    crypto: vmx - fix copy-paste error in CTR mode
	    
	    The original assembly imported from OpenSSL has two copy-paste
	    errors in handling CTR mode. When dealing with a 2 or 3 block tail,
	    the code branches to the CBC decryption exit path, rather than to
	    the CTR exit path.
	
and by https://github.com/openssl/openssl/pull/8510.  This took almost 5 years.

I also still think the extent that you keep emphasizing the phrase "formally
verified" when discussing Zinc is somewhat misleading, because the only
implementation that is actually formally verified is Curve25519 in C.  No other
algorithms or implementations are formally verified.  E.g. none of the Poly1305
implementations under discussion are formally verified.  That needs to be made
very clear, and as one consequence of that we really need good tests.

- Eric