Prerequisites
Download and unpack gfverif:
wget http://gfverif.cryptojedi.org/gfverif-20151230.tar.gz
gunzip gfverif-20151230.tar
tar -xf gfverif-20151230.tar
Install the pyparsing package: e.g., python-pyparsing under Ubuntu.
Install g++. After this typing g++ should produce g++: fatal error: no input files. If you don't have a recent version of g++ then you'll have to replace -std=c++11 with -std=c++0x in Makefile.
Install the Sage computer-algebra system. Under Fedora a recent version is nicely packaged:
yum install sagemath
Under Ubuntu it is better to install from source:
adduser --disabled-password --gecos 'Sage' sage
su - sage
time wget http://pari.math.u-bordeaux.fr/pub/pari/packages/seadata.tgz
openssl sha256 seadata.tgz
# c9282a525ea3f92c1f9c6c69e37ac5a87b48fb9ccd943cfd7c881a3851195833
time wget http://mirrors.mit.edu/sage/src/sage-6.8.tar.gz
openssl sha256 sage-6.8.tar.gz
# 49ca2885cce1ed1ea5e84f4954cee3f0e9d403289bbd5f6c0faf0411ffcf5580
ln -s sage-6.8/sage
time tar -xf sage-6.8.tar.gz
cd sage-6.8
time MAKE="make -j7" make
cd
tar -xf seadata.tgz
cp data/seadata/* sage-6.8/local/share/pari/seadata/
exit
ln -s /home/sage/sage /usr/local/bin/sage
After this typing echo print 2+2 | sage should print a Sage banner and sage: 4.
Example 1: modular exponentiation in GF(2127-1)
The following demo is meant as an introduction to what gfverif does.
Unpacking from wire format
Look at 127frombytes.cpp. The frombytes function is a typical input-conversion routine: it reads a 127-bit integer from bytes s[0], ..., s[15] and puts the same integer into unsigned 32-bit ints x[0], x[1], x[2], x[3], x[4] in radix 226. This function doesn't have any gfverif annotations.
main, via doit, calls frombytes with various gfverif annotations. Specifically:
- main allocates a 16-byte s array and calls inputunsignedchar() for each byte to declare that byte as an input integer between 0 and 255.
- doit allocates a verifier_bigint vs, and calls verifier_addlimb(&vs,s[i],i * 8) for each byte s[i]. This defines a ghost integer vs as the sum of s[i]*2(i*8).
- doit calls frombytes.
- doit defines another ghost integer vx as the sum of x[i]*2(i*26).
- doit calls verifier_assertequal(&vs,&vx) to assert that vs and vx are the same integer.
Type make 127frombytes.out and look at the resulting 127frombytes.out. After some preliminary lines you'll see
# v49 = v2 << 8 min 0 max 65280
# v50 = v1 + v49 min 0 max 65535
# v51 = v3 << 16 min 0 max 16711680
# v52 = v50 + v51 min 0 max 16777215
# v53 = v4 << 24 min 0 max 4278190080
# v54 = v52 + v53 min 0 max 4294967295
produced from one run through first few lines of the frombytes function:
x[0] = crypto_uint32(s[0]);
x[0] += crypto_uint32(s[1]) << 8;
x[0] += crypto_uint32(s[2]) << 16;
x[0] += crypto_uint32(s[3]) << 24;
v49 is the intermediate quantity s[1]<<8. The bounds min 0 and max 65280 are computed automatically by gfverif; they say that this intermediate quantity is definitely between 0 and 65280. (They don't say that 0 and 65280 are necessarily achievable, although obviously they are for this code.) v50 is the second value of x[0], guaranteed to be between 0 and 65535. This continues through v54, the final value of x[0], guaranteed to be between 0 and 4294967295, just barely fitting into a 32-bit unsigned int.
The previous quantity v48 is the ghost value vs for the frombytes input, between 0 and 340282366920938463463374607431768211455 (which you can check is 2128-1). The earlier lines are for intermediate quantities in the computation of v48.
Subsequent lines build up to v84, the ghost value vx for the frombytes output. The next line
# highlevel v48 = v84
translates the verifier_assertequal into a high-level language. The remaining lines of 127frombytes.out translate the same assertion into a polynomial equality expressed in the Sage computer-algebra language. Specifically, the line
R.<v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15,v16> = PolynomialRing(ZZ,16)
creates a polynomial ring with variables v1, ..., v16; subsequent lines such as
v49 = v2 * 2^8
v50 = v1 + v49
create polynomials in these variables, such as the polynomial v1 + v2 * 28, also known as v50; and the line
assert v48 - v84 in I
ends up asserting that the v48 and v84 polynomials are equal. To verify this assertion, type make 127frombytes.sage and then sage 127frombytes.sage, and check that there is no output from Sage.
Squaring
Now look at 127mul.cpp. The function frombytes is the same as in 127frombytes.cpp. The function mul is a typical modular-multiplication function, multiplying two inputs x and y modulo 2127-1 to obtain an output z; each input and output is a uint32[5] array in radix 226.
The function doit calls frombytes as before to convert s into x, and then calls mul to square x, producing z. It has three ghost variables: vs and vx as before, and a new vz. It has two assertions: verifier_assertequal(&vs,&vx) as before, and a new verifier_assertprodmod(&vz,&vx,&vx,vp), where vp is defined as "170141183460469231731687303715884105727" (which you can check is 2127-1).
Run
make 127mul.sage; sage 127mul.sage
to check both assertions. The new assertion fails:
File "127mul.py", line 192, in <module>
assert v165 - v166 in I
AssertionError
An assertion failure from gfverif is not necessarily a bug in the code being verified: maybe the code is correct but gfverif doesn't know enough to prove it. In this case, however, there is a bug in the code: a conflict between the implicit postconditions for frombytes and the implicit preconditions for mul. Specifically, mul computes various 64-bit sums of 64-bit products of its uint32 inputs, but it needs to assume that the inputs are considerably smaller than 232 to avoid overflow of these 64-bit sums, while frombytes can produce outputs almost as large as 232-1.
gfverif detects the bug in 127mul.cpp because it is tracking the range of each value, and using these ranges to control its inputs to the computer-algebra system. For example, if range analysis shows that two uint64 values a and b are both between 0 and 263-1, then uint64 c = a + b produces the sum c of the integers a and b, and gfverif says c = a + b to the computer-algebra system (translated into various v variables). However, if range analysis produces wider ranges for a and b, then c might be something different, so gfverif doesn't say c = a + b.
127mul2.cpp fixes the bug in 127mul.cpp by adding a few radix-226 carry steps to frombytes. This reduces the actual ranges of the uint32 output values from frombytes, and it also reduces the ranges computed by gfverif. To verify the 127mul2.cpp assertions:
make 127mul2.sage; sage 127mul2.sage
We comment that gfverif's range analysis for this simple load-and-multiply-mod-2127-1 example involves peephole optimization of ranges in the underlying computation graph. Consider, for example, the lines
c0 = x[0] >> 26; x[0] -= c0 << 26; x[1] += c0;
carrying from x[0] to x[1]. The peephole optimizer notices that the new x[0] is the old x[0] mod 226, and is therefore between 0 and 226-1. This particular optimization could have been expressed in the source code as x[0] &= ..., but then a different peephole analysis would have been required to see that these lines don't change x[0] + x[1]*226.
Are there any other tools that can handle this type of verification? We haven't found any.
Repeated squaring
127pow.cpp uses the corrected frombytes and mul from 127mul2.cpp, but now performs a chain of several squarings. Running
make 127mul2.sage; sage 127mul2.sage
again produces an assertion failure.
There is again a bug in the original code, this time in mul. Specifically, mul carries from z[0] to z[1] to z[2] to z[3] to z[4] and back around to z[0]. This is enough to guarantee that all of the results fit into uint32, but it can produce z[0] above 230, and then the next multiplication can overflow.
127pow2.cpp fixes this by adding another carry step. However, with 127pow2.cpp the time and memory for verification grow rapidly with the number of squarings, and are already unreasonable for a chain of 3 squarings. The problem here is that all results are being expressed as polynomials in terms of the original variables (along with a linearly increasing number of carry variables), and these polynomials have degree growing exponentially with the number of squarings.
127pow3.cpp fixes this by adding a "cut" after each squaring step: the new line
verifier_cutlimbs(z,5);
says that z[0], ..., z[4] are now treated as new variables, and the computations that produced them are forgotten. The verification cost then grows linearly with the number of squarings, and is just a few seconds for 200 squarings.
An inductive verification, finding a fixed point for the ranges, would have cost independent of the number of squarings, but straight-line verification is much simpler and is fast enough for full ECC verification.
Freezing
Each limb above such as x[0] is guaranteed to be not much larger than 226, and ghost integers such as vx are guaranteed to be not much larger than 2127. However, before an integer is output it must be reduced to a unique representative modulo 2127-1, which in turn must be represented as bytes in a unique way; otherwise the cryptanalysts would have to study how much other information is leaked.
127tobytes.cpp and 127tobytes2.cpp verify two different styles of "freezing" an integer into its least remainder modulo 2127-1. The line
verifier_assertrange(&Out,"0","170141183460469231731687303715884105726");
asserts that Out is between 0 and 170141183460469231731687303715884105726 (which you can check is 2127-2), and is checked by gfverif.
We briefly comment that verifier_isnegative and verifier_ispositive fork the verification into cases. There are several further points to document and improve here: in particular, 127tobytes.cpp and 127tobytes2.cpp need be adjusted to support the high-level language the same way that testsmult (below) does.
Example 2: X25519 scalar multiplication
testsmult.cpp is the ref10 implementation of X25519 scalar multiplication, plus some small tweaks, plus some annotations. Skim the code to see what the annotations look like, and pay particular attention to the following annotations:
verifier_bigint ninput;
for (int i = 0;i < 32;++i) verifier_addlimb(&ninput,n[i],i * 8);
verifier_input(&ninput);
You can see (by skimming earlier lines) that this directly uses the n input to crypto_scalarmult, and you can see that ninput is defined as the integer represented by the 32 bytes of n in radix 28. The verifier_input line defines ninput as an input in the high-level language.
There are similar annotations for the p input, and similar annotations for the q output, along with a line
verifier_assertrange(&vq,"0","57896044618658097711785492504343953926634992332820282019728792003956564819948")
asserting that this output is between 0 and 57... (which you can check is 2255-20).
Use gfverif to verify all assertions in the annotations:
make testsmult.sage; sage testsmult.sage
This takes two minutes on one core of a 3.5GHz Intel Xeon E3-1275 v2.
Next look at montaudit.in, a concise description of what crypto_scalarmult is supposed to do. This is human-auditable and easily checkable against cryptosystem specifications used by cryptanalysts.
Use gfverif to verify that the high-level computation carried out by testsmult matches this description:
time make equal.out
cat equal.out
This takes under two minutes and prints one line
57896044618658097711785492504343953926634992332820282019728792003956564819949
stating that the computations match modulo 57... (which you can check is 2255-19).
There's obviously more to be documented here about the high-level annotations, the high-level language, and what's actually being done by the equal script.