intro.tex 6.15 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
XXX: NaCl
XXX: TweetNaCl (find real-world use of TweetNaCl?)

XXX: 
``TweetNaCl is the
first cryptographic library that allows correct functionality to be verified
by auditors with reasonable effort''

XXX: One core component of TweetNaCl (and NaCl) is X25519, mention use
of X25519 in the wild.


Benoit Viguier's avatar
Benoit Viguier committed
13

Benoit Viguier's avatar
forward    
Benoit Viguier committed
14
TweetNaCl\cite{BGJ+15} is a compact reimplementation of the
Benoit Viguier's avatar
done    
Benoit Viguier committed
15
16
17
18
NaCl\cite{BLS12} high security cryptographic library.
It does not aim for high speed application and has been optimized for source
code compactness (100 tweets). It maintains some degree of readability in order
to be easily auditable.
Benoit Viguier's avatar
Benoit Viguier committed
19

Benoit Viguier's avatar
forward    
Benoit Viguier committed
20
21
22
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$.
Benoit Viguier's avatar
done    
Benoit Viguier committed
23
This function is used by a wide variety of applications\cite{this-that-use-curve25519}
Benoit Viguier's avatar
forward    
Benoit Viguier committed
24
25
26
to establish a shared secret over an insecure channel.

Implementing cryptographic primitives without any bugs is difficult.
Benoit Viguier's avatar
done    
Benoit Viguier committed
27
28
29
30
31
32
33
34
35
36
37
38
39
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 generating machine
code by refinment in order to get a software correct by construction.
This approach is being used in e.g. the B-method\cite{Abrial:1996:BAP:236705},
F* \cite{DBLP:journals/corr/BhargavanDFHPRR17}, or with Coq \cite{CpdtJFR}.

However this first method 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.

40
\subheading{Contribution of this paper}
Benoit Viguier's avatar
Benoit Viguier committed
41

42
43
44
45
46
\todo{Proof that TweetNaCl's X25519 code correctly implements math definition from 25519 paper}

\todo{State additional contributions, e.g., extension of EC framework by Bartiza and Strub.}

\subheading{Our Formal Approach.}
Benoit Viguier's avatar
Benoit Viguier committed
47
Verifying an existing cryptographic library, we use the second approach.
Benoit Viguier's avatar
Benoit Viguier committed
48
Our method can be seen as a static analysis over the input values coupled
Benoit Viguier's avatar
Benoit Viguier committed
49
with the formal proof that the code of the algorithm matches its specification.
50

Benoit Viguier's avatar
done    
Benoit Viguier committed
51
We use Coq\cite{coq-faq}, a formal system that allows us to machine-check our proofs.
Benoit Viguier's avatar
forward    
Benoit Viguier committed
52
A famous example of its use is the proof of the Four Color Theorem \cite{gonthier2008formal}.
Benoit Viguier's avatar
done    
Benoit Viguier committed
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
The CompCert, a C compiler\cite{Leroy-backend} proven correct and sound is being build on top of it.
To prove its correctness, CompCert uses multiple intermediate languages. The first step of CompCert is done by the parser \textit{clightgen}.
It takes as input C code and generates its Clight\cite{Blazy-Leroy-Clight-09} translation.

Using this intermediate representation Clight, we use the Verifiable Software Toolchain
(VST)\cite{2012-Appel}, a framework which uses Separation logic\cite{1969-Hoare,Reynolds02separationlogic}
and shows that the semantics of the program satisfies a functionnal specification in Coq.
VST steps through each line of Clight using a strongest post-condition strategy.
We write a specification of the crypto scalar multiplication of TweetNaCl and using
VST we prove that the code matches our definitions.

Bartzia and Strub wrote a formal library for elliptic curves\cite{DBLP:conf/itp/BartziaS14}.
We extend it to support Montgomery curves. With this formalization, we prove the
correctness of a generic Montgomery ladder and show that our specification is an instance of it.

68
\subheading{Related work.}
Benoit Viguier's avatar
done    
Benoit Viguier committed
69

70
71
72
73
\todo{Separate verification of existing code from generating proof-carrying code.}

Similar approaches have been used to prove the correctness of OpenSSL HMAC~\cite{Beringer2015VerifiedCA} 
and SHA-256~\cite{2015-Appel}. Compared to their work
Benoit Viguier's avatar
done    
Benoit Viguier committed
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
our approaches makes a complete link between the C implementation and the formal
mathematical definition of the group theory behind elliptic curves.

Using the synthesis approach, Zinzindohou{\'{e}} et al. wrote an verified extensible
library of elliptic curves\cite{Zinzindohoue2016AVE}. This served as ground work for the
cryptographic library HACL*\cite{zinzindohoue2017hacl} used in the NSS suite from Mozilla.

Coq does not only allows verification but also synthesis.
Using correct-by-construction finite field arithmetic\cite{Philipoom2018CorrectbyconstructionFF}
one can synthesize\cite{Erbsen2016SystematicSO} certified elliptic curve
implementations\cite{Erbsen2017CraftingCE}. These implementation are now being used in BoringSSL\cite{fiat-crypto}.

Curve25519 implementations has already been under the scrutiny \cite{Chen2014VerifyingCS}.
However in this paper we provide a proofs of correctness and soundness of a C program up to
the theory of elliptic curves.

90
\todo{Add 1-2 sentences about how this compares? Different limitations etc.}
Benoit Viguier's avatar
done    
Benoit Viguier committed
91

92
\subheading{Reproducing the proofs.}
Benoit Viguier's avatar
done    
Benoit Viguier committed
93
94
95
96
To maximize reusability of our results we placed the code of our formal proofs
presented in this paper into the public domain. They are available at XXXXXXX
with instructions of how to compile and verify our proofs.

97
98
\subheading{Organization of this paper.}
Section~\ref{sec2-implem} gives the necessary background on Curve25519
Benoit Viguier's avatar
done    
Benoit Viguier committed
99
implementation in TweetNaCl and provides the specifications we later prove correct.
100
101
Section~\ref{sec3-maths} describes our extension of the formal library by Bartzia and Strub.
Section~\ref{sec4-refl} makes the link between the mathematical model and the C implementation.
Benoit Viguier's avatar
done    
Benoit Viguier committed
102
In this section we also describe some of the techniques we used to speed up some of the proofs.
103
Section~\ref{sec5-vst} provides with attention points a VST user should be careful
Benoit Viguier's avatar
done    
Benoit Viguier committed
104
105
of in order to avoid unnecessary work.

Benoit Viguier's avatar
forward    
Benoit Viguier committed
106

Benoit Viguier's avatar
forward    
Benoit Viguier committed
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
% 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
124