1_Introduction.tex 1.72 KB
Newer Older
Benoit Viguier's avatar
Benoit Viguier committed
1
2
\section{Introduction}

3
Implementing cryptographic primitives without any bugs is hard.
Benoit Viguier's avatar
Benoit Viguier committed
4
While tests provides a code coverage and are used in the limits,
Benoit Viguier's avatar
Benoit Viguier committed
5
they still don't cover 100\% of the possible input values.
Benoit Viguier's avatar
Benoit Viguier committed
6
7
Our method is 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.
8
9
10
11

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.
Benoit Viguier's avatar
Benoit Viguier committed
12
It maintains some degree of readability in order to be easily auditable.
13

Benoit Viguier's avatar
Benoit Viguier committed
14
This library makes use of Curve25519\cite{Ber06}, a function over a \F{p}-restricted
Benoit Viguier's avatar
Benoit Viguier committed
15
16
$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$.
17

Benoit Viguier's avatar
Benoit Viguier committed
18
19
20
Coq is a formal system that allows to machine-check our proofs.
A famous example of its use is the proof of the Four Color Theorem.
The Compcert\cite{Leroy-backend} compiler and the Verifiable Software Toolchain (VST)\cite{2012-Appel} are build
21
22
23
on top of it.

Our approach is as follow, we use the \textit{clightgen} tool from Compcert to
Benoit Viguier's avatar
Benoit Viguier committed
24
generate the \textit{semantic version} (Clight\cite{Blazy-Leroy-Clight-09}) of
Benoit Viguier's avatar
Benoit Viguier committed
25
26
27
28
29
30
31
the TweetNaCl C code.
Using the Separation logic\cite{1969-Hoare,Reynolds02separationlogic}
with with the Verifiable Software Toolchain we show that the semantics of the
program satisfies a functionnal specification in Coq.
We extend the work of Bartzia and Strub \cite{DBLP:conf/itp/BartziaS14} to 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.