Add simple limb overflow checker for Poly1305

Monocypher now grabs at the graal of Formal Verification.

It is very crude, but it works for Poly1305.  Just transliterate the C
program into Python, add some preconditions and asserts, and execute the
result as Python to prove the absence of overflow (provided the
preconditions are correct).

ECC code might be more difficult, we'll see.

See #246

.gitignore

@@ -18,10 +18,11 @@
 *.includes
 *.su
 *.su.*
+*.gen.*
 tests/formal-analysis/*
 tests/formal-analysis
-**/__pycache__/**
 *.tar.gz
 monocypher-*/
+**/__pycache__/**
 doc/html/
-tests/vectors.h
+tests/vectors.h

dist_ignore

@@ -18,6 +18,7 @@
 *.includes
 *.su
 *.su.*
+*.gen.*
 tests/formal-analysis/*
 tests/formal-analysis
 *.tar.gz

src/monocypher.c

@@ -312,6 +312,27 @@ static void poly_block(crypto_poly1305_ctx *ctx, const u8 in[16], unsigned end)
 	u32 s[4];
 	load32_le_buf(s, in, 4);
 
+	//- PROOF Poly1305
+	//-
+	//- # Inputs & preconditions
+	//- ctx->h[0] = u32()
+	//- ctx->h[1] = u32()
+	//- ctx->h[2] = u32()
+	//- ctx->h[3] = u32()
+	//- ctx->h[4] = u32(limit = 4)
+	//-
+	//- ctx->r[0] = u32(limit = 0x0fffffff)
+	//- ctx->r[1] = u32(limit = 0x0ffffffc)
+	//- ctx->r[2] = u32(limit = 0x0ffffffc)
+	//- ctx->r[3] = u32(limit = 0x0ffffffc)
+	//-
+	//- s[0] = u32()
+	//- s[1] = u32()
+	//- s[2] = u32()
+	//- s[3] = u32()
+	//-
+	//- end = unsigned(limit = 1)
+
 	// s = h + c, without carry propagation
 	const u64 s0 = ctx->h[0] + (u64)s[0]; // s0 <= 1_fffffffe
 	const u64 s1 = ctx->h[1] + (u64)s[1]; // s1 <= 1_fffffffe
@@ -345,11 +366,15 @@ static void poly_block(crypto_poly1305_ctx *ctx, const u8 in[16], unsigned end)
 	const u64 u4 = (u3 >> 32)     + (u5 & 3);
 
 	// Update the hash
-	ctx->h[0] = (u32)u0; // u0 <= 1_9ffffff0
-	ctx->h[1] = (u32)u1; // u1 <= 1_97ffffe0
-	ctx->h[2] = (u32)u2; // u2 <= 1_8fffffe2
-	ctx->h[3] = (u32)u3; // u3 <= 1_87ffffe4
-	ctx->h[4] = (u32)u4; // u4 <=          4
+	ctx->h[0] = u0 & 0xffffffff; // u0 <= 1_9ffffff0
+	ctx->h[1] = u1 & 0xffffffff; // u1 <= 1_97ffffe0
+	ctx->h[2] = u2 & 0xffffffff; // u2 <= 1_8fffffe2
+	ctx->h[3] = u3 & 0xffffffff; // u3 <= 1_87ffffe4
+	ctx->h[4] = u4 & 0xffffffff; // u4 <=          4
+
+	//- # postconditions
+	//- ASSERT(ctx->h[4].limit() <= 4)
+	//- CQFD Poly1305
 }
 
 void crypto_poly1305_init(crypto_poly1305_ctx *ctx, const u8 key[32])

tests/proofs/filter.sh

@@ -0,0 +1,23 @@
+#! /bin/env sh
+
+echo "#! /bin/env python3"
+echo "from overflow import *"
+echo ""
+sed -n "/PROOF $1/,/CQFD $1/p"                                          |\
+    sed '1d;$d'                                                         |\
+    sed 's|	||'                                                         |\
+    sed 's|//- ||'                                                      |\
+    sed 's|^.*//-.*$||'                                                 |\
+    sed 's|  *//.*||'                                                   |\
+    sed 's|//|#|'                                                       |\
+    sed 's|const ||'                                                    |\
+    sed 's|;||'                                                         |\
+    sed 's|ctx->|ctx_|'                                                 |\
+    sed 's|\[|_|g'                                                      |\
+    sed 's|\]||g'                                                       |\
+    sed 's|(\([a-zA-Z0-9_]*\))\([a-zA-Z0-9_]*\)|\1(\2)|g'               |\
+    sed 's|^\([a-zA-Z0-9_]*\) \([a-zA-Z0-9_]*\) = \(.*\)$|\2 = \1(\3)|' |\
+    sed 's|\* \([0-9][0-9]*\)|\* cast(\1)|g'                            |\
+    sed 's|\+ \([0-9][0-9]*\)|\+ cast(\1)|g'                            |\
+    sed 's|\- \([0-9][0-9]*\)|\- cast(\1)|g'                            |\
+    cat

tests/proofs/overflow.py

@@ -0,0 +1,49 @@
+
+def number(limit, overflow):
+    if limit > overflow:
+        raise AssertionError("limit exceeds overflow", limit, overflow)
+    return (limit, overflow)
+
+def add   (a, b): return number(a[0] + b[0], max(a[1], b[1]))
+def sub   (a, b): return number(a[0] + b[0], max(a[1], b[1])) # still +
+def mul   (a, b): return number(a[0] * b[0], max(a[1], b[1]))
+def rshift(a, n): return number(a[0] >> n, a[1])
+def lshift(a, n): return number(a[0] << n, a[1])
+def b_and (a, n): return number(a[0] & n, a[1])
+
+inttype = int #we're overriding int down the line
+def cast(n):
+    if type(n) is inttype:
+        return Number(number(n, 2**16-1))
+    return n
+
+class Number:
+    def __init__  (self, num  ): self.num = num
+    def limit     (self)       : return self.num[0]
+    def overflow  (self)       : return self.num[1]
+    def __add__   (self, other): return Number(add(self.num, cast(other.num)))
+    def __sub__   (self, other): return Number(sub(self.num, cast(other.num)))
+    def __mul__   (self, other): return Number(mul(self.num, cast(other.num)))
+    def __rshift__(self, n)    : return Number(rshift(self.num, n))
+    def __lshift__(self, n)    : return Number(lshift(self.num, n))
+    def __and__   (self, n)    : return Number(b_and (self.num, n))
+    def __str__(self): return "Number(" + str(self.num) + ")"
+
+def make(num, limit, overflow):
+    if num is not None:
+        limit = num.limit()
+    return Number(number(limit, overflow))
+
+def u16(num=None, limit = 2**16-1): return make(num, limit, 2**16-1)
+def u32(num=None, limit = 2**32-1): return make(num, limit, 2**32-1)
+def u64(num=None, limit = 2**64-1): return make(num, limit, 2**64-1)
+unsigned = u16
+
+def i16(num=None, limit = 2**15-1): return make(num, limit, 2**15-1)
+def i32(num=None, limit = 2**31-1): return make(num, limit, 2**31-1)
+def i64(num=None, limit = 2**63-1): return make(num, limit, 2**63-1)
+int = i16
+
+def ASSERT(truth):
+    if not truth:
+        raise AssertionError("ASSERT failed")

tests/proofs/test_carry.sh

@@ -0,0 +1,13 @@
+#! /bin/env sh
+
+set -e
+
+DIR=$(dirname "$0")
+
+POLY=$DIR/poly1305.gen.py
+
+echo "Check limb overflow: $POLY"
+$DIR/filter.sh Poly1305 <$DIR/../../src/monocypher.c >$POLY
+python3 $DIR/poly1305.gen.py
+
+echo "No limb overflow detected"