From 9a49a3d3f9aee8cf87595bf498ed7021d947d5d6 Mon Sep 17 00:00:00 2001 From: Loup Vaillant Date: Sun, 22 Jan 2023 21:41:51 +0100 Subject: [PATCH] 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 | 5 ++-- dist_ignore | 1 + src/monocypher.c | 35 +++++++++++++++++++++++---- tests/proofs/filter.sh | 23 ++++++++++++++++++ tests/proofs/overflow.py | 49 ++++++++++++++++++++++++++++++++++++++ tests/proofs/test_carry.sh | 13 ++++++++++ 6 files changed, 119 insertions(+), 7 deletions(-) create mode 100755 tests/proofs/filter.sh create mode 100644 tests/proofs/overflow.py create mode 100755 tests/proofs/test_carry.sh diff --git a/.gitignore b/.gitignore index f4bcaa17..e3e1130d 100644 --- 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 4c6b623a..00b77b58 100644 --- 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 6787c83f..fafa169e 100644 --- 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 index 00000000..ca7bbcf3 --- /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 index 00000000..2008b5ac --- /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 index 00000000..a630eabb --- /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"