## 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(2^{127}-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 2^{26}.
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 4294967295produced 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 2^{128}-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 * 2 ^{8}`, 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 2^{127}-1 to obtain an output `z`;
each input and output is a uint32[5] array in radix 2^{26}.

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 2^{127}-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 2^{32}
to avoid overflow of these 64-bit sums,
while `frombytes` can produce outputs almost as large as 2^{32}-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 2^{63}-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-2^{26} 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-2^{127}-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 2^{26},
and is therefore between 0 and 2^{26}-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]*2 ^{26}`.

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 2^{30},
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 2^{26},
and ghost integers such as `vx`
are guaranteed to be not much larger than 2^{127}.
However,
before an integer is output it must be reduced to a *unique*
representative modulo 2^{127}-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 2^{127}-1.
The line

verifier_assertrange(&Out,"0","170141183460469231731687303715884105726");

asserts that `Out` is between 0 and 170141183460469231731687303715884105726
(which you can check is 2^{127}-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 2^{8}.
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 2^{255}-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 2^{255}-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.