Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Benoit Viguier
coqveriftweetnacl
Commits
6af3609e
Commit
6af3609e
authored
Jun 04, 2019
by
Benoit Viguier
Browse files
forward
parent
23b1d007
Changes
4
Expand all
Hide whitespace changes
Inline
Sidebyside
readings/1_Introduction.tex
View file @
6af3609e
\section
{
Introduction
}
Implementing cryptographic primitives without any bugs is hard.
While tests provides a code coverage and are used in the limits,
they still don't cover 100
\%
of the possible input values.
TweetNaCl
\cite
{
BGJ+15
}
is a compact reimplementation of the
NaCl
\cite
{
BLS12
}
library. It does not aim for high speed
application and has been optimized for source code compactness.
It maintains some degree of readability in order to be easily auditable.
This library makes use of Curve25519
\cite
{
Ber06
}
, a function over a
\F
{
p
}
restricted
$
x
$
coordinate computing a scalar multiplication on
$
E
(
\F
{
p
^
2
}
)
$
, where
$
p
$
is
the prime number
$
\p
$
and
$
E
$
is the elliptic curve
$
y
^
2
=
x
^
3
+
486662
x
^
2
+
x
$
.
This function is used by a wide variety of applications
\cite
{
thisthatusecurve25519
}
to establish a shared secret over an insecure channel.
Implementing cryptographic primitives without any bugs is difficult.
While tests provides with code coverage,
they still don't cover 100
\%
of the possible input values.
In order to get formal guaranties a software meets its specifications,
two methodologies exist. The first one is by synthesizing a formal specification and
two methodologies exist.
The first one is by synthesizing a formal specification and
generating machine code by refinment. This approach is being used in the
Bmethod
\cite
{
Abrial:1996:BAP:236705
}
, F*
\cite
{
DBLP:journals/corr/BhargavanDFHPRR17
}
with Kremlin, or in Coq
\cite
{
CpdtJFR
}
.
Bmethod
\cite
{
Abrial:1996:BAP:236705
}
, HACL*
\cite
{
zinzindohoue2017hacl
}
and F*
\cite
{
DBLP:journals/corr/BhargavanDFHPRR17
}
with Kremlin, or with Coq
\cite
{
CpdtJFR
}
.
This gives you a software correct by construction. However it cannot be applied
to an existing piece of software. In such case we need to write the specifications
and then verify the correctness of the implementation.
...
...
@@ 16,19 +29,10 @@ Verifying an existing cryptographic library, we use the second approach.
Our method can be seen as a static analysis over the input values coupled
with the formal proof that the code of the algorithm matches its specification.
Similar approaches have been used to prove the correctness of OpenSSL HMAC
\cite
{
Beringer2015VerifiedCA
}
and SHA256
\cite
{
Appel2015VerificationOA
}
.
TweetNaCl
\cite
{
BGJ+15
}
is a compact reimplementation of the
NaCl
\cite
{
BLS12
}
library. It does not aim for high speed
application and has been optimized for source code compactness.
It maintains some degree of readability in order to be easily auditable.
This library makes use of Curve25519
\cite
{
Ber06
}
, a function over a
\F
{
p
}
restricted
$
x
$
coordinate computing a scalar multiplication on
$
E
(
\F
{
p
^
2
}
)
$
, where
$
p
$
is
the prime number
\p
and
$
E
$
is the elliptic curve
$
y
^
2
=
x
^
3
+
486662
x
^
2
+
x
$
.
\cite
{
Beringer2015VerifiedCA
}
and SHA256
\cite
{
2015Appel
}
.
Coq is a formal system that allows to machinecheck our proofs.
A famous example of its use is the proof of the Four Color Theorem.
A famous example of its use is the proof of the Four Color Theorem
\cite
{
gonthier2008formal
}
.
The Compcert
\cite
{
Leroybackend
}
compiler and the Verifiable Software Toolchain
(VST)
\cite
{
2012Appel
}
are build on top of it.
...
...
@@ 43,6 +47,8 @@ support Montgomery curves.
With this formalization, we prove the correctness of a generic Montgomery ladder
and show that our specification can be seen as an instance of it.
\todo
[inline]
{
Add where the software is available
}
% Five years ago:
% \url{https://www.imperialviolet.org/2014/09/11/moveprovers.html}
% \url{https://www.imperialviolet.org/2014/09/07/provers.html}
...
...
readings/3_Maths.tex
View file @
6af3609e
...
...
@@ 95,7 +95,6 @@ the Montgomery form \cite{MontgomerySpeeding}.
$$
by
^
2
=
x
^
3
+
ax
^
2
+
x,
$$
along with an additional formal point
$
\Oinf
$
, ``at infinity''.
\end{definition}
Using a similar representation, we defined the parametric type
\texttt
{
mc
}
which
represent the points on a specific montgomery curve. It is parametrized by
a
\texttt
{
K : ecuFieldType
}
 the type of fields which characteristic is not 2 or 3 
...
...
@@ 112,7 +111,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 the same way as it it is in the Weierstra
{
\ss
}
form,
however the actual computations will be slightly different.
\begin{lstlisting}
[language=Coq]
...
...
@@ 130,7 +128,6 @@ Definition add (p1 p2 : point K) :=
( xs,  s * (xs  x1)  y1 )
end.
\end{lstlisting}
But we prove it is internal to the curve (again with coercion):
\begin{lstlisting}
[language=Coq]
Lemma addO (p q : mc) : oncurve (add p q).
...
...
@@ 139,17 +136,15 @@ Definition addmc (p1 p2 : mc) : mc :=
\end{lstlisting}
We then prove a bijection between a Montgomery curve and its Weierstra
{
\ss
}
equation.
\begin{lemma}
Let
$
M
_{
a,b
}
(
\K
)
$
be a Montgomery curve,
D
efine
$$
a'
=
\frac
{
3

a
^
2
}{
3
b
^
2
}
\text
{
\ \ \ \
and
\ \ \ \
}
b'
=
\frac
{
2
a
^
3

9
a
}{
27
b
^
3
}
.
$$
T
hen
$
E
_{
a',b'
}
(
\K
)
$
is an elliptic curve, and the mapping
$
\varphi
: M
_{
a,b
}
(
\K
)
\mapsto
E
_{
a',b'
}
(
\K
)
$
defined as:
Let
$
M
_{
a,b
}
(
\K
)
$
be a Montgomery curve,
d
efine
$$
a'
=
\frac
{
3

a
^
2
}{
3
b
^
2
}
\text
{
\ \ \ \
and
\ \ \ \
}
b'
=
\frac
{
2
a
^
3

9
a
}{
27
b
^
3
}
.
$$
t
hen
$
E
_{
a',b'
}
(
\K
)
$
is an elliptic curve, and the mapping
$
\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
}
)
\end{align*}
is an isomorphism between groups.
\end{lemma}
\begin{lstlisting}
[language=Coq]
Definition ec
_
of
_
mc
_
point p :=
match p with
...
...
@@ 166,7 +161,6 @@ Definition ec_of_mc p :=
Lemma ec
_
of
_
mc
_
bij : bijective ec
_
of
_
mc.
\end{lstlisting}
\subsubsection
{
Projective coordinates
}
\label
{
projective
}
Points on a projective plane are represented with a triple
$
(
X:Y:Z
)
$
. Any points except
$
(
0
:
0
:
0
)
$
defines a point on a projective plane. A scalar multiple of a point defines the same point,
\ie
...
...
@@ 188,7 +182,7 @@ Hypothesis mcu_no_square : forall x : K, x^+2 != (M#a)^+2  4%:R.
\end{lstlisting}
With those coordinates we prove the following lemmas for the addition of two points.
\begin{definition}
We d
efine the functions
$
\chi
$
and
$
\chi
_
0
$
:
\\
\begin{definition}
D
efine the functions
$
\chi
$
and
$
\chi
_
0
$
:
\\

$
\chi
: M
_{
a,b
}
(
\K
)
\to
\K
\cup
\{\infty\}
$
\\
such that
$
\chi
(
\Oinf
)
=
\infty
$
and
$
\chi
((
x,y
))
=
x
$
.
\\

$
\chi
_
0
: M
_{
a,b
}
(
\K
)
\to
\K
$
\\
...
...
@@ 514,7 +508,7 @@ Coercion repr (x : type) : Zmodp.type*Zmodp.type :=
let: Zmodp2 u v := x in (u, v).
Definition zero : type :=
pi ( 0
%:R, 0%:R).
pi ( 0
%:R, 0%:R
).
Definition one : type :=
pi ( 1, 0
%:R ).
Definition opp (x : type) : type :=
...
...
readings/6_UsingVST.tex
View file @
6af3609e
...
...
@@ 90,8 +90,26 @@ Example of such cases are summarized in Fig \ref{tk:MemSame}.
\subsection
{
Verifiying
\texttt
{
for
}
loops: head and tail recursion
}
While the final state of a For loops can be computed by a simple recursive function,
we must define invariants that are true for each step of the iteration.
Final state of
\texttt
{
for
}
loops can be computed by simple recursive functions.
However we must define invariants which are true for each step of the iterations.
For a lower value of the iterator
\texttt
{
i
}
, a normal recursive function in Coq
would only compute the last
\texttt
{
i
}
steps instead of the first
\texttt
{
i
}
ones
as we would like for our invariant.
e.g. for a function
$
g :
\N
\rightarrow
T
\rightarrow
T
$
iterated a maximum of
5 times, for
$
i
=
2
$
,
$
g
(
4
, g
(
3
, x
))
$
instead of
$
g
(
1
, g
(
0
, x
))
$
.
This requires us to define each function with
an accumulator.
We define two recursive functions
\Coqe
{
rec
_
fn
}
and
\Coqe
{
rec
_
fn
_
rev
_
acc
}
.
They emulate the behavior of
\texttt
{
for
}
loops and take as implicit argument a
function
\Coqe
{
g
}
which emulate the body of the loop.
\begin{lemma}
With their appropriate
\texttt
{
for
}
loops, Head recursion and Tail recursion
compute the same result.
\end{lemma}
The intuition behind the proof
\begin{Coq}
Variable T : Type.
...
...
@@ 117,9 +135,6 @@ Lemma Tail_Head_equiv :
rec
_
fn n s = rec
_
fn
_
rev n s.
\end{Coq}
In order to prove the for loops, we must define invariants.
Those have to be
\todo
[inline]
{
How many lines of specification ?
}
...
...
readings/collection.bib
View file @
6af3609e
This diff is collapsed.
Click to expand it.
Write
Preview
Supports
Markdown
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