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

Benoit Viguier's avatar
forward    
Benoit Viguier committed
3
4
5
6
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.
Benoit Viguier's avatar
Benoit Viguier committed
7

Benoit Viguier's avatar
forward    
Benoit Viguier committed
8
9
10
11
12
13
14
15
16
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{this-that-use-curve25519}
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.
Benoit Viguier's avatar
Benoit Viguier committed
17
In order to get formal guaranties a software meets its specifications,
Benoit Viguier's avatar
forward    
Benoit Viguier committed
18
19
20
two methodologies exist.

The first one is by synthesizing a formal specification and
Benoit Viguier's avatar
Benoit Viguier committed
21
generating machine code by refinment. This approach is being used in the
Benoit Viguier's avatar
forward    
Benoit Viguier committed
22
23
B-method\cite{Abrial:1996:BAP:236705}, HACL*\cite{zinzindohoue2017hacl} and F* \cite{DBLP:journals/corr/BhargavanDFHPRR17}
with Kremlin, or with Coq \cite{CpdtJFR}.
Benoit Viguier's avatar
Benoit Viguier committed
24
25
26
27
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.

Benoit Viguier's avatar
Benoit Viguier committed
28
Verifying an existing cryptographic library, we use the second approach.
Benoit Viguier's avatar
Benoit Viguier committed
29
Our method can be seen as a static analysis over the input values coupled
Benoit Viguier's avatar
Benoit Viguier committed
30
with the formal proof that the code of the algorithm matches its specification.
Benoit Viguier's avatar
Benoit Viguier committed
31
Similar approaches have been used to prove the correctness of OpenSSL HMAC
Benoit Viguier's avatar
forward    
Benoit Viguier committed
32
\cite{Beringer2015VerifiedCA} and SHA-256 \cite{2015-Appel}.
33

Benoit Viguier's avatar
Benoit Viguier committed
34
Coq is a formal system that allows to machine-check our proofs.
Benoit Viguier's avatar
forward    
Benoit Viguier committed
35
A famous example of its use is the proof of the Four Color Theorem \cite{gonthier2008formal}.
Benoit Viguier's avatar
Benoit Viguier committed
36
37
The Compcert\cite{Leroy-backend} compiler and the Verifiable Software Toolchain
(VST)\cite{2012-Appel} are build on top of it.
38
39

Our approach is as follow, we use the \textit{clightgen} tool from Compcert to
Benoit Viguier's avatar
Benoit Viguier committed
40
generate the \textit{semantic version} (Clight\cite{Blazy-Leroy-Clight-09}) of
Benoit Viguier's avatar
Benoit Viguier committed
41
42
43
44
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.
Benoit Viguier's avatar
Benoit Viguier committed
45
46
We extend the work of Bartzia and Strub \cite{DBLP:conf/itp/BartziaS14} to
support Montgomery curves.
Benoit Viguier's avatar
Benoit Viguier committed
47
With this formalization, we prove the correctness of a generic Montgomery ladder
Benoit Viguier's avatar
forward    
Benoit Viguier committed
48
and show that our specification is an instance of it.
Benoit Viguier's avatar
forward    
Benoit Viguier committed
49

Benoit Viguier's avatar
forward    
Benoit Viguier committed
50
51
\todo[inline]{Add where the software is available}

Benoit Viguier's avatar
forward    
Benoit Viguier committed
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
% Five years ago:
% \url{https://www.imperialviolet.org/2014/09/11/moveprovers.html}
% \url{https://www.imperialviolet.org/2014/09/07/provers.html}

% \section{Related Works}
%
% \begin{itemize}
%   \item HACL*
%   \item Proving SHA-256 and HMAC
%   \item \url{http://www.iis.sinica.edu.tw/~bywang/papers/ccs17.pdf}
%   \item \url{http://www.iis.sinica.edu.tw/~bywang/papers/ccs14.pdf}
%   \item \url{https://cryptojedi.org/crypto/#gfverif}
%   \item \url{https://cryptojedi.org/crypto/#verify25519}
%   \item Fiat Crypto : synthesis
% \end{itemize}
%
% Add comparison with Fiat-crypto