intro.tex 7.31 KB
Newer Older
Benoit Viguier's avatar
Benoit Viguier committed
1
2
3
4
5
6
7
8
NaCl~\cite{BLS12} is an easy-to-use high-security high-speed software library
for network communication, encryption, decryption, signatures, etc.
TweetNaCl~\cite{BGJ+15} is its compact reimplementation.
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.
TweetNaCl is being used by ZeroMQ~\cite{zmq} messaging queue system to provide
portability to its users.
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
9
10
% ``TweetNaCl is the first cryptographic library that allows correct functionality
% to be verified by auditors with reasonable effort''~\cite{BGJ+15}
11

Benoit Viguier's avatar
Benoit Viguier committed
12
13
14
% XXX: TweetNaCl (find real-world use of TweetNaCl?)
% Mega.nz uses tweetnacl-js (as JS port of tweetnacl) for their webclient https://mega.nz/
% Keybase client: https://github.com/keybase/node-nacl/blob/master/lib/tweetnacl.js
15

Benoit Viguier's avatar
Benoit Viguier committed
16
17
18
19
One core component of TweetNaCl (and NaCl) is the key exchange protocol X25519~\cite{rfc7748}.
This protocol is being used by a wide variety of applications~\cite{this-that-use-curve25519}
such as SSH~\cite{rfc4253}, Signal Protocol, Tor, Zcash, TLS to establish a shared secret over
an insecure channel.
Benoit Viguier's avatar
Benoit Viguier committed
20

21
This library makes use of Curve25519~\cite{Ber06}, a function over a \F{p}-restricted
Benoit Viguier's avatar
forward    
Benoit Viguier committed
22
23
24
$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
Benoit Viguier committed
25
26
27
28
Originally, the name ``Curve25519'' referred to this keyexchange protocol,
but Bernstein suggested to rename the scheme to X25519 and to use the name
Curve25519 for the underlying elliptic curve~\cite{Ber14}.
We make use of this notation in this paper.
29
30

\subheading{Contribution of this paper}
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
31
32
33
34
35
36
37
38
39
40
We provide a mechanized formal proof of the correctness of X25519
implementation in TweetNaCl. This is done by first extending the formal library for
elliptic curves~\cite{DBLP:conf/itp/BartziaS14} of Bartzia and Strub wrote to
support Curve25519. Then proving that the code correctly implements the definitions
from the original paper by Bernstein~\cite{Ber14}.

% 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
Benoit Viguier's avatar
done    
Benoit Viguier committed
41
42
43
44
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.
45
46
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}.
Benoit Viguier's avatar
done    
Benoit Viguier committed
47
48
49
50
51

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.

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

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

Using this intermediate representation Clight, we use the Verifiable Software Toolchain
64
(VST)~\cite{2012-Appel}, a framework which uses Separation logic~\cite{1969-Hoare,Reynolds02separationlogic}
Benoit Viguier's avatar
done    
Benoit Viguier committed
65
66
67
68
69
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.

70
Bartzia and Strub wrote a formal library for elliptic curves~\cite{DBLP:conf/itp/BartziaS14}.
Benoit Viguier's avatar
done    
Benoit Viguier committed
71
72
73
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.

74
\subheading{Related work.}
Benoit Viguier's avatar
done    
Benoit Viguier committed
75

76
77
\todo{Separate verification of existing code from generating proof-carrying code.}

78
Similar approaches have been used to prove the correctness of OpenSSL HMAC~\cite{Beringer2015VerifiedCA}
79
and SHA-256~\cite{2015-Appel}. Compared to their work
Benoit Viguier's avatar
done    
Benoit Viguier committed
80
81
82
83
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
84
85
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.
Benoit Viguier's avatar
done    
Benoit Viguier committed
86
87

Coq does not only allows verification but also synthesis.
88
89
90
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}.
Benoit Viguier's avatar
done    
Benoit Viguier committed
91

92
Curve25519 implementations has already been under the scrutiny~\cite{Chen2014VerifyingCS}.
Benoit Viguier's avatar
done    
Benoit Viguier committed
93
94
95
However in this paper we provide a proofs of correctness and soundness of a C program up to
the theory of elliptic curves.

Benoit Viguier's avatar
WIP    
Benoit Viguier committed
96
97
98
99
100
101
Synthesis approaches forces the user to depend on generated code which may not
be optimal (speed, compactness...), they require to tweak the compiler in order
to achieve the desired properties. On the other hand a carefully handcrafted
optimized code will force the verifier to consider all the possible special cases
and write a complex low level specification in order to prove the correctness of
the algorithm.
Benoit Viguier's avatar
done    
Benoit Viguier committed
102

103
\subheading{Reproducing the proofs.}
Benoit Viguier's avatar
done    
Benoit Viguier committed
104
105
106
107
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.

108
\subheading{Organization of this paper.}
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
109
110
111
112
113
114
115
116
Section~\ref{preliminaries} give the necessary background on Curve25519
implementation and a rough understand of how formal verification works.
Section~\ref{C-Coq} provides the specification of X25519 in addition to proofs
techniques used to show the correctness.
Section~\ref{sec3-maths} describes our extension of the formal library by Bartzia
and Strub and the correctness of X25519 implementation with respect to Bernstein
specifications~\cite{Ber14}.
And lastly in Section~\ref{Conclusion} we discuss the trust in this proof.
Benoit Viguier's avatar
done    
Benoit Viguier committed
117

Benoit Viguier's avatar
forward    
Benoit Viguier committed
118

Benoit Viguier's avatar
forward    
Benoit Viguier committed
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
% 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