1_Introduction.tex 3.07 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
8
9
10
11
12
13
14

In order to get formal guaranties a software meets its specifications,
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
B-method\cite{Abrial:1996:BAP:236705}, F* \cite{DBLP:journals/corr/BhargavanDFHPRR17} with Kremlin, or in 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.

Benoit Viguier's avatar
Benoit Viguier committed
15
Verifying an existing cryptographic library, we use the second approach.
Benoit Viguier's avatar
Benoit Viguier committed
16
Our method can be seen as a static analysis over the input values coupled
Benoit Viguier's avatar
Benoit Viguier committed
17
with the formal proof that the code of the algorithm matches its specification.
Benoit Viguier's avatar
Benoit Viguier committed
18
19
Similar approaches have been used to prove the correctness of OpenSSL HMAC
\cite{Beringer2015VerifiedCA} and SHA-256 \cite{Appel2015VerificationOA}.
20
21
22
23

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
24
It maintains some degree of readability in order to be easily auditable.
25

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

Benoit Viguier's avatar
Benoit Viguier committed
30
31
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.
Benoit Viguier's avatar
Benoit Viguier committed
32
33
The Compcert\cite{Leroy-backend} compiler and the Verifiable Software Toolchain
(VST)\cite{2012-Appel} are build on top of it.
34
35

Our approach is as follow, we use the \textit{clightgen} tool from Compcert to
Benoit Viguier's avatar
Benoit Viguier committed
36
generate the \textit{semantic version} (Clight\cite{Blazy-Leroy-Clight-09}) of
Benoit Viguier's avatar
Benoit Viguier committed
37
38
39
40
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
41
42
We extend the work of Bartzia and Strub \cite{DBLP:conf/itp/BartziaS14} to
support Montgomery curves.
Benoit Viguier's avatar
Benoit Viguier committed
43
44
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.
Benoit Viguier's avatar
forward    
Benoit Viguier committed
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62

% 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