Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Benoit Viguier
coqveriftweetnacl
Commits
64002ca6
Commit
64002ca6
authored
Oct 01, 2019
by
Benoit Viguier
Browse files
WIP
parent
cbec0bd8
Changes
4
Hide whitespace changes
Inline
Sidebyside
paper/2_preliminaries.tex
View file @
64002ca6
...
...
@@ 107,7 +107,7 @@ Note that $n' \in 2^{254} + 8\{0,1,\ldots,2^{251}1\}$.
X25519 then computes the
\xcoord
of
$
n'
\cdot
P
$
.
RFC~7748~
\cite
{
rfc7748
}
standardized the X25519 Diffie–Hellman keyexchange algorithm.
Given the base point
$
B
$
where
$
X
_
B
=
9
$
, each party generate a secret random number
Given the base point
$
B
$
where
$
X
_
B
=
9
$
, each party generate
s
a secret random number
$
s
_
a
$
(respectively
$
s
_
b
$
), and computes
$
X
_{
P
_
a
}$
(respectively
$
X
_{
P
_
b
}$
), the
\xcoord
of
$
P
_
A
=
s
_
a
\cdot
B
$
(respectively
$
P
_
B
=
s
_
b
\cdot
B
$
).
The parties exchange
$
X
_{
P
_
a
}$
and
$
X
_{
P
_
b
}$
and compute their shared secret with
...
...
@@ 118,7 +118,7 @@ X25519 on $s_a$ and $X_{P_b}$ (respectively $s_b$ and $X_{P_a}$).
As its name suggests, TweetNaCl aims for code compactness (
\emph
{
``a crypto library in 100 tweets''
}
).
As a result it uses a few defines and typedefs to gain precious bytes while
still remaining readable.
still remaining
human
readable.
\begin{lstlisting}
[language=Ctweetnacl]
#define FOR(i,n) for (i = 0;i < n;++i)
#define sv static void
...
...
@@ 129,7 +129,7 @@ typedef long long i64;
TweetNaCl functions take pointers as arguments. By convention the first one
points to the output array. It is then followed by the input arguments.
Due to some limitations of VST, indexes used in
\TNaCle
{
for
}
loops have to be
Due to some limitations of
the
VST, indexes used in
\TNaCle
{
for
}
loops have to be
of type
\TNaCle
{
int
}
instead of
\TNaCle
{
i64
}
. We change the code to allow our
proofs to carry through. We believe this does not affect the correctness of the
original code. A complete diff of our modifications to TweetNaCl can be found in
...
...
@@ 341,7 +341,7 @@ int crypto_scalarmult(u8 *q,
% the pseudocode description
\subsection
{
Coq, separation logic, and VST
}
\subsection
{
Coq, separation logic, and
the
VST
}
\label
{
subsec:CoqVST
}
Coq~
\cite
{
coqfaq
}
is an interactive theorem prover based on type theory. It
...
...
@@ 382,6 +382,6 @@ The first step consists of translating the source code into Clight,
an intermediate representation used by CompCert.
For such purpose one uses the parser of CompCert called
\texttt
{
clightgen
}
.
In a second step one defines the Hoare triple representing the specification of
the piece of software one wants to prove. Then using VST, one uses a strongest
the piece of software one wants to prove. Then using
the
VST, one uses a strongest
postcondition approach to prove the correctness of the triple.
This approach can be seen as a forward symbolic execution of the program.
paper/4_lowlevel.tex
View file @
64002ca6
...
...
@@ 26,7 +26,7 @@ Theorem body_crypto_scalarmult:
% We first describe the global structure of our proof (\ref{subsec:proofstructure}).
Using our formalization of RFC~7748 (
\sref
{
sec:CoqRFC
}
) we specify the Hoare
triple before proving its correctness with VST (
\ref
{
subsec:withVST
}
).
triple before proving its correctness with
the
VST (
\ref
{
subsec:withVST
}
).
We provide an example of equivalence of operations over different number
representations (
\ref
{
subsec:numreprrfc
}
). Then, we describe efficient techniques
used in some of our more complex proofs (
\ref
{
subsec:inversionsreflections
}
).
...
...
@@ 153,7 +153,7 @@ point to nonoverlapping space in memory.
When called with three memory fragments (
\texttt
{
o, a, b
}
),
the three of them will be consumed. However assuming this naive specification
when
\texttt
{
M(o,a,a)
}
is called (squaring), the first two memory areas (
\texttt
{
o, a
}
)
are consumed and VST will expect a third memory section (
\texttt
{
a
}
) which does not
\emph
{
exist
}
anymore.
are consumed and
the
VST will expect a third memory section (
\texttt
{
a
}
) which does not
\emph
{
exist
}
anymore.
Examples of such cases are illustrated in
\fref
{
tikz:MemSame
}
.
\begin{figure}
[h]
%
\centering
%
...
...
@@ 246,7 +246,7 @@ Later in \sref{subsec:Zmodp}, we formally define $\Ffield$.
Equivalence between operations in
$
\Zfield
$
(
\ie
under
\coqe
{
:GF
}
) and in
$
\Ffield
$
are easily proven.
Using these two definitions, we prove intermediate lemmas such as the correctness of the
multiplication
\Coqe
{
Low.M
}
where
\Coqe
{
Low.M
}
replicate the computations and steps done in C.
multiplication
\Coqe
{
Low.M
}
where
\Coqe
{
Low.M
}
replicate
s
the computations and steps done in C.
\begin{lemma}
\label
{
lemma:mult
_
correct
}
\Coqe
{
Low.M
}
correctly implements the multiplication over
$
\Zfield
$
.
...
...
@@ 392,7 +392,7 @@ The idea is to \emph{reflect} the goal into a decidable environment.
We show that for a property
$
P
$
, we can define a decidable Boolean property
$
P
_{
bool
}$
such that if
$
P
_{
bool
}$
is
\Coqe
{
true
}
then
$
P
$
holds.
$$
\text
{
\textit
{
reify
\_
P
}}
: P
_{
bool
}
=
\text
{
\textit
{
true
}}
\implies
P
$$
By applying
\textit
{
reify
\_
P
}
on
$
P
$
our goal become
$
P
_{
bool
}
=
true
$
.
By applying
\textit
{
reify
\_
P
}
on
$
P
$
our goal become
s
$
P
_{
bool
}
=
true
$
.
We then compute the result of
$
P
_{
bool
}$
. If the decision goes well we are
left with the tautology
$
\text
{
\textit
{
true
}}
=
\text
{
\textit
{
true
}}$
.
...
...
paper/5_highlevel.tex
View file @
64002ca6
...
...
@@ 41,27 +41,28 @@ an elliptic curve $E$
is a plane cubic algebraic curve defined by an equation
$
E
(
x,y
)
$
of the form:
$$
E : y
^
2
+
a
_
1
xy
+
a
_
3
y
=
x
^
3
+
a
_
2
x
^
2
+
a
_
4
x
+
a
_
6
$$
where the
$
a
_
i
$
's are in
\K\
and the curve has no singular point (
\ie
no cusps
or selfintersections). The set of points, written
$
E
(
\K
)
$
, is formed by the
solutions
$
(
x,y
)
$
of
$
E
$
augmented by
a distinguished point
$
\Oinf
$
(
called point at infinity
)
:
$$
E
(
\K
)
=
\{
(
x,y
)
\in
\K
\times
\K
 E
(
x,y
)
\}
\cup
\{\Oinf\}
$$
or selfintersections). The set of points
defined over
\K
, written
$
E
(
\K
)
$
, is formed by the
solutions
$
(
x,y
)
$
of
$
E
$
together with
a distinguished point
$
\Oinf
$
called point at infinity:
$$
E
(
\K
)
=
\{
E
(
x,y
)
~~
(
x,y
)
\in
\K
\times
\K\}
\cup
\{\Oinf\}
$$
\end{dfn}
\subsubsection
{
Weierstra
{
\ss
}
curves
}
\subsubsection
{
Short
Weierstra
{
\ss
}
curves
}
\label
{
subsec:ECCWeierstrass
}
This equation
$
E
(
x,y
)
$
can be reduced into its short Weierstra
{
\ss
}
form.
\begin{dfn}
Let
$
a
\in
\K
$
, and
$
b
\in
\K
$
such that
$$
\Delta
(
a,b
)
=

16
(
4
a
^
3
+
27
b
^
2
)
\neq
0
.
$$
The
\textit
{
elliptic curve
}
$
E
_{
a,b
}
(
\K
)
$
is the set of all points
$
(
x,y
)
\in
\K
^
2
$
satisfying the equation:
$$
y
^
2
=
x
^
3
+
ax
+
b,
$$
Let
$
a
\in
\K
$
and
$
b
\in
\K
$
such that
$$
\Delta
(
a,b
)
=

16
(
4
a
^
3
+
27
b
^
2
)
\neq
0
.
$$
The
\textit
{
elliptic curve
}
$
E
_{
a,b
}$
is defined by the equation:
$$
y
^
2
=
x
^
3
+
ax
+
b.
$$
$
E
_{
a,b
}
(
\K
)
$
is the set of all points
$
(
x,y
)
\in
\K
^
2
$
satisfying the
$
E
_{
a,b
}$
along with an additional formal point
$
\Oinf
$
, ``at infinity''. Such a curve does not have any singularity.
\end{dfn}
In this setting, Bartzia and Strub defined the parametric type
\texttt
{
ec
}
which
represent the points on a specific curve. It is parameterized by
a
\texttt
{
K : ecuFieldType
}
 the type of fields which characteristic is not 2 or 3 
and
\texttt
{
E : ecuType
}
 a record that packs the curve parameters
$
a
$
and
$
b
$
a
\texttt
{
K : ecuFieldType
}


the type of fields which characteristic is not 2 or 3 

and
\texttt
{
E : ecuType
}


a record that packs the curve parameters
$
a
$
and
$
b
$
along with the proof that
$
\Delta
(
a,b
)
\neq
0
$
.
\begin{lstlisting}
[language=Coq]
Inductive point := EC
_
Inf  EC
_
In of K * K.
...
...
@@ 77,11 +78,11 @@ Definition oncurve (p : point) :=
Inductive ec : Type := EC p of oncurve p.
\end{lstlisting}
Points o
f
an elliptic curve are equipped with the structure of an abelian group.
Points o
n
an elliptic curve are equipped with the structure of an abelian group.
\begin{itemize}
\item
The negation of a point
$
P
=
(
x,y
)
$
is defined by reflecti
ng in
the
$
x
$
axis
$

P
=
(
x,

y
)
$
.
\item
The negation of a point
$
P
=
(
x,y
)
$
is defined by reflecti
on over
the
$
x
$
axis
$

P
=
(
x,

y
)
$
.
\item
The addition of two points
$
P
$
and
$
Q
$
is defined as the negation of the third intersection point
of the line passing through
$
P
$
and
$
Q
$
or tangent to
$
P
$
if
$
P
=
Q
$
.
of the line passing through
$
P
$
and
$
Q
$
,
or tangent to
$
P
$
if
$
P
=
Q
$
.
\item
$
\Oinf
$
is the neutral element under this law: if 3 points are collinear, their sum is equal to
$
\Oinf
$
.
\end{itemize}
These operations are defined in Coq as follows (where we omit the code for the tangent case):
...
...
@@ 124,9 +125,9 @@ than the Weierstra{\ss} form. We consider the Montgomery form \cite{MontgomerySp
Similar to the definition of
\texttt
{
ec
}
, we defined the parametric type
\texttt
{
mc
}
which
represents the points on a specific Montgomery curve.
It is parameterized by
a
\texttt
{
K : ecuFieldType
}
 the type of fields which characteristic is not
2 or 3 
and
\texttt
{
M : mcuType
}
 a record that packs the curve
parameters
$
a
$
and
$
b
$
along with the proofs that
$
b
\neq
0
$
and
$
a
^
2
\neq
4
$
.
a
\texttt
{
K : ecuFieldType
}


the type of fields which characteristic is not
2 or 3 
and
\texttt
{
M : mcuType
}


a record that packs the curve
parameters
$
a
$
and
$
b
$
along with the proofs that
$
b
\neq
0
$
and
$
a
^
2
\neq
4
$
.
\begin{lstlisting}
[language=Coq]
Record mcuType :=
{
cA : K; cB : K;
_
: cB != 0;
_
: cA
^
2 != 4
}
.
...
...
@@ 139,7 +140,6 @@ Inductive mc : Type := MC p of oncurve p.
Lemma oncurve
_
mc: forall p : mc, oncurve p.
\end{lstlisting}
We define the addition on Montgomery curves in the similar way as in the Weierstra
{
\ss
}
form.
%, however the actual computations will be slightly different.
\begin{lstlisting}
[language=Coq]
Definition add (p1 p2 : point K) :=
match p1, p2 with
...
...
@@ 162,7 +162,7 @@ Definition addmc (p1 p2 : mc) : mc :=
MC p1 p2 (addO p1 p2)
\end{lstlisting}
We then define a bijection between a Montgomery curve and its Weierstra
{
\ss
}
form.
We then define a bijection between a Montgomery curve and its
short
Weierstra
{
\ss
}
form.
In this way we get associativity of addition on Montgomery curves from the
corresponding property for Weierstra
{
\ss
}
curves.
\begin{lemma}
...
...
@@ 172,9 +172,9 @@ corresponding property for Weierstra{\ss} curves.
$
\varphi
: M
_{
a,b
}
(
\K
)
\mapsto
E
_{
a',b'
}
(
\K
)
$
defined as:
\begin{align*}
\varphi
(
\Oinf
_
M)
&
=
\Oinf
_
E
\\
\varphi
( (x , y) )
&
= (
\frac
{
x
}{
b
}
+
\frac
{
a
}{
3b
}
,
\frac
{
y
}{
b
}
)
\varphi
( (x , y) )
&
=
\left
(
\frac
{
x
}{
b
}
+
\frac
{
a
}{
3b
}
,
\frac
{
y
}{
b
}
\right
)
\end{align*}
is an isomorphism between
group
s.
is an isomorphism between
elliptic curve
s.
\end{lemma}
\begin{lstlisting}
[language=Coq]
Definition ec
_
of
_
mc
_
point p :=
...
...
@@ 192,8 +192,6 @@ Definition ec_of_mc p :=
Lemma ec
_
of
_
mc
_
bij : bijective ec
_
of
_
mc.
\end{lstlisting}
% We use this isomorphism to derive that $(M_{a,b}(\K), + )$ is a group.
\subsubsection
{
Projective coordinates
}
\label
{
subsec:ECCprojective
}
...
...
@@ 203,8 +201,8 @@ Scalar multiples are representing the same point, \ie
for all
$
\lambda
\neq
0
$
, the triples
$
(
X:Y:Z
)
$
and
$
(
\lambda
X:
\lambda
Y:
\lambda
Z
)
$
represent
the same point.
For
$
Z
\neq
0
$
, the projective point
$
(
X:Y:Z
)
$
corresponds to the
point
$
(
X
/
Z,Y
/
Z
)
$
on the
Euclidean
plane. Likewise the point
$
(
X,Y
)
$
on the
Euclidean
plane corresponds to
$
(
X:Y:
1
)
$
on the projective plane.
point
$
(
X
/
Z,Y
/
Z
)
$
on the
affine
plane. Likewise the point
$
(
X,Y
)
$
on the
affine
plane corresponds to
$
(
X:Y:
1
)
$
on the projective plane.
Using fractions as coordinates, the equation for a Montgomery curve
$
M
_{
a,b
}
(
\K
)
$
becomes:
...
...
@@ 212,7 +210,7 @@ $$b \bigg(\frac{Y}{Z}\bigg)^2 = \bigg(\frac{X}{Z}\bigg)^3 + a \bigg(\frac{X}{Z}\
Multiplying both sides by
$
Z
^
3
$
yields:
$$
b Y
^
2
Z
=
X
^
3
+
a X
^
2
Z
+
XZ
^
2
$$
With this equation we can additionally represent the ``point at infinity''. By
setting
$
Z
=
0
$
, we derive
$
X
=
0
$
, giving us the ``infinite point
s
''
$
(
0
:
Y
:
0
)
$
with
$
Y
\neq
0
$
.
setting
$
Z
=
0
$
, we derive
$
X
=
0
$
, giving us the ``infinite point''
$
(
0
:
1
:
0
)
$
.
By restricting the parameter
$
a
$
of
$
M
_{
a,b
}
(
\K
)
$
such that
$
a
^
2

4
$
is not a
square in
\K
, we ensure that
$
(
0
,
0
)
$
is the only point with a
$
y
$
coordinate of
$
0
$
.
...
...
@@ 280,7 +278,7 @@ in the definition of \coqe{RFC}, and is easily proved to correspond to it.
In Coq this correspondence proof is hidden in the proof of
\coqe
{
RFC
_
Correct
}
shown above.)
%\ref to the def of montgomery_rec? relevant lemma(s) that show(s) these are "the same"?
We prove its correctness for any point
s
wh
ich
\xcoord
is not 0.
We prove its correctness for any point wh
ose
\xcoord
is not 0.
% By taking \aref{alg:montgomeryladder} and replacing \texttt{xDBL} and \texttt{xADD}
...
...
@@ 371,7 +369,7 @@ Theorem opt_montgomery_ok (n m: nat) (x : K) :
To be able to use the above theorem we need to satisfy hypothesis
\ref
{
hyp:a
_
minus
_
4
_
not
_
square
}
:
$
a
^
2

4
$
is not a square in
\K
:
$$
\forall
x
\in
\K
,
\
x
^
2
\neq
a
^
2

4
$$
$$
\forall
x
\in
\K
,
\
x
^
2
\neq
a
^
2

4
.
$$
If we consider the quadratic extension field
$
\F
{
p
^
2
}$
,
there exists
$
x
$
such that
$
x
^
2
=
a
^
2

4
$
, preventing use
\tref
{
thm:montgomeryladdercorrect
}
with
$
\K
=
\F
{
p
^
2
}$
.
...
...
paper/6_conclusion.tex
View file @
64002ca6
...
...
@@ 59,7 +59,7 @@ Indeed indexes 17 to 79 of the \TNaCle{i64 x[80]} intermediate variable of
we removed them.
Peter Wu and Jason A. Donenfeld brought to our attention that the original
\TNaCle
{
car25519
}
function
presented
risk of undefined behavior if
\texttt
{
c
}
\TNaCle
{
car25519
}
function
carried a
risk of undefined behavior if
\texttt
{
c
}
is a negative number.
\begin{lstlisting}
[language=Ctweetnacl]
c=o[i]>>16;
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment