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

diff --git a/.gitignore b/.gitignore
index f4bcaa17ecd9e4f3a4483a49d2b86caa31508c40..e3e1130d0c2471c389c7eea915c0107cb11ae01a 100644 (file)
--- a/.gitignore
+++ b/.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
\ No newline at end of file
+tests/vectors.h

diff --git a/dist_ignore b/dist_ignore
index 4c6b623a563326918f0dc623d40736a8ea9405da..00b77b58b52d08b121b052c53a812458701a68f5 100644 (file)
--- a/dist_ignore
+++ b/dist_ignore
@@ -18,6 +18,7 @@
 *.includes
 *.su
 *.su.*
+*.gen.*
 tests/formal-analysis/*
 tests/formal-analysis
 *.tar.gz

diff --git a/src/monocypher.c b/src/monocypher.c
index 6787c83f19bf3fe2dab49431da3afb87821e1314..fafa169e72bff00c26734234c80473f46345a6d8 100644 (file)
--- a/src/monocypher.c
+++ b/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])

diff --git a/tests/proofs/filter.sh b/tests/proofs/filter.sh
new file mode 100755 (executable)
index 0000000..ca7bbcf
--- /dev/null
+++ b/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

diff --git a/tests/proofs/overflow.py b/tests/proofs/overflow.py
new file mode 100644 (file)
index 0000000..2008b5a
--- /dev/null
+++ b/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")

diff --git a/tests/proofs/test_carry.sh b/tests/proofs/test_carry.sh
new file mode 100755 (executable)
index 0000000..a630eab
--- /dev/null
+++ b/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"