intro.tex 7.52 KB
Newer Older
1
2
\section{Introduction}
\label{sec:intro}
3

4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
The Networking and Cryptography library (NaCl)~\cite{BLS12} 
is an easy-to-use high-security high-speed crypto library.
It uses specialized code for different platform, making it complex and hard to audit.
TweetNaCl~\cite{BGJ+15} is a compact reimplementation in C
of the core functionalities of NaCl and is claimed to be 
\emph{``the first cryptographic library that allows correct functionality
to be verified by auditors with reasonable effort''}~\cite{BGJ+15}.
The original paper presenting TweetNaCl describes some effort to support
this claim, like formal verification of memory safety, but does not actually
prove correctness of any of the primitives offered by the library.

A 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{things-that-use-curve25519}
such as SSH, Signal Protocol, Tor, Zcash, TLS to establish a shared secret over
an insecure channel.

% For example TweetNaCl is being used by ZeroMQ~\cite{zmq}
%messaging queue system to provide portability to its users.
Benoit Viguier's avatar
Benoit Viguier committed
22
23
24
% 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
25

Benoit Viguier's avatar
Benoit Viguier committed
26

27
This library makes use of Curve25519~\cite{Ber06}, a function over a \F{p}-restricted
Benoit Viguier's avatar
forward    
Benoit Viguier committed
28
29
30
$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
31
Originally, the name ``Curve25519'' referred to the key exchange protocol,
Benoit Viguier's avatar
Benoit Viguier committed
32
33
34
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.
Benoit Viguier's avatar
Benoit Viguier committed
35
% do we need to specify which "this" refers to ?
36
37

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

Benoit Viguier's avatar
Benoit Viguier committed
44
45
46
47
48
49
50
% In order to get formal guaranties a software meets its
% specifications, two methodologies exist.
There are two methodologies to get formal guarantees a software meets its
specifications.
The first one is by synthesizing a formal specification and then generating machine
code by refinement.
 % in order to get a software correct by construction.
51
52
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
53
However this first method cannot be applied to an existing piece of software.
Benoit Viguier's avatar
Benoit Viguier committed
54
55
56
57
58

The second approach consists of writing the specifications and then verifying
the correctness of the implementation.
Because we verify the TweetNaCl cryptographic library, we use this second method.

Benoit Viguier's avatar
done    
Benoit Viguier committed
59

60
\subheading{Our Formal Approach.}
Benoit Viguier's avatar
Benoit Viguier committed
61
62
Our verification process 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.
63

64
We use Coq~\cite{coq-faq}, a formal system that allows us to machine-check our proofs.
Benoit Viguier's avatar
Benoit Viguier committed
65
66
Some famous examples of its use are the proof of the Four Color Theorem~\cite{gonthier2008formal}; or
CompCert, a C~compiler~\cite{Leroy-backend} which proven correct and sound by being build on top of it.
Benoit Viguier's avatar
Benoit Viguier committed
67
In its proof, CompCert uses multiple intermediate languages and show equivalence between them.
Benoit Viguier's avatar
Benoit Viguier committed
68
The first step of the compilation by CompCert is done by the parser \textit{clightgen}.
69
It takes as input C code and generates its Clight~\cite{Blazy-Leroy-Clight-09} translation.
Benoit Viguier's avatar
done    
Benoit Viguier committed
70
71

Using this intermediate representation Clight, we use the Verifiable Software Toolchain
72
(VST)~\cite{2012-Appel}, a framework which uses Separation logic~\cite{1969-Hoare,Reynolds02separationlogic}
Benoit Viguier's avatar
done    
Benoit Viguier committed
73
74
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.
Benoit Viguier's avatar
Benoit Viguier committed
75
We write a specification of TweetNaCl's crypto scalar multiplication and using
Benoit Viguier's avatar
done    
Benoit Viguier committed
76
77
VST we prove that the code matches our definitions.

Benoit Viguier's avatar
Benoit Viguier committed
78
79
80
We extend Bartzia and Strub's elliptic curves library~\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 is an instance of it.
Benoit Viguier's avatar
done    
Benoit Viguier committed
81

82
\subheading{Related work.}
Benoit Viguier's avatar
done    
Benoit Viguier committed
83

84
85
\todo{Separate verification of existing code from generating proof-carrying code.}

Benoit Viguier's avatar
Benoit Viguier committed
86
87
88
89
Similar approaches have been used to prove the correctness of OpenSSL
HMAC~\cite{Beringer2015VerifiedCA} and SHA-256~\cite{2015-Appel}. Compared to
their work our approaches makes a complete link between the C implementation and
the formal mathematical definition of the group theory behind elliptic curves.
Benoit Viguier's avatar
done    
Benoit Viguier committed
90
91

Using the synthesis approach, Zinzindohou{\'{e}} et al. wrote an verified extensible
92
93
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
94
95

Coq does not only allows verification but also synthesis.
96
97
98
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
99

100
Curve25519 implementations has already been under the scrutiny~\cite{Chen2014VerifyingCS}.
Benoit Viguier's avatar
done    
Benoit Viguier committed
101
102
103
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
104
105
106
107
108
109
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
110

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

116
\subheading{Organization of this paper.}
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
117
118
119
120
121
122
123
124
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
125

Benoit Viguier's avatar
forward    
Benoit Viguier committed
126

Benoit Viguier's avatar
forward    
Benoit Viguier committed
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
% 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