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

Benoit Viguier's avatar
Benoit Viguier committed
4
5
The Networking and Cryptography library (NaCl)~\cite{BLS12}
is an easy-to-use, high-security, high-speed cryptography library.
Peter Schwabe's avatar
Peter Schwabe committed
6
It uses specialized code for different platform, which makes it rather complex and hard to audit.
Benoit Viguier's avatar
Benoit Viguier committed
7
8
TweetNaCl~\cite{BGJ+15} is a compact re-implementation in C
of the core functionalities of NaCl and is claimed to be
9
10
11
\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
Peter Schwabe's avatar
Peter Schwabe committed
12
13
this claim, for example, formal verification of memory safety, but does not actually
prove correctness of any of the primitives implemented by the library.
14

Peter Schwabe's avatar
Peter Schwabe committed
15
One core component of TweetNaCl (and NaCl) is the key-exchange protocol X25519~\cite{rfc7748}.
16
This protocol is being used by a wide variety of applications~\cite{things-that-use-curve25519}
Peter Schwabe's avatar
Peter Schwabe committed
17
such as SSH, Signal Protocol, Tor, Zcash, and TLS to establish a shared secret over
18
an insecure channel.
Benoit Viguier's avatar
Benoit Viguier committed
19
The X25519 key exchange protocol is a an $x$-coordinate only
Peter Schwabe's avatar
Peter Schwabe committed
20
elliptic-curve Diffie-Hellman key-exchange using the Montgomery
Benoit Viguier's avatar
Benoit Viguier committed
21
curve $E: y^2 = x^3 + 486662 x^2 + x$ over the field $\F{\p}$.
Peter Schwabe's avatar
Peter Schwabe committed
22
Note that originally, the name ``Curve25519'' referred to the key exchange protocol,
Benoit Viguier's avatar
Benoit Viguier committed
23
but Bernstein suggested to rename the scheme to X25519 and to use the name
Peter Schwabe's avatar
Peter Schwabe committed
24
25
X25519 for the protocol and Curve25519 for the underlying elliptic curve~\cite{Ber14}.
We make use of this updated notation in this paper.
26
27

\subheading{Contribution of this paper}
Peter Schwabe's avatar
Peter Schwabe committed
28
We provide a mechanized formal proof of the correctness of the X25519
Benoit Viguier's avatar
Benoit Viguier committed
29
30
31
implementation in TweetNaCl.
This proof is done in two steps:
We first prove equivalence of the C implementation of X25519
Peter Schwabe's avatar
Peter Schwabe committed
32
33
to an implementation in Coq~\cite{coq-faq}.
This part of the proof uses the Verifiable Software Toolchain (VST)~\cite{2012-Appel}
Benoit Viguier's avatar
Benoit Viguier committed
34
to establish a link between C and Coq.
Peter Schwabe's avatar
Peter Schwabe committed
35
36
37
38
39
40
41
42
43
44
VST uses Separation logic~\cite{1969-Hoare,Reynolds02separationlogic}
to show that the semantics of the program satisfy a functional specification in Coq.
To the best of our knowledge, this is the first time that
VST is used in the formal proof of correctness of an implementation
of an asymmetric cryptographic primitive.

In a second step we prove that the Coq implementation matches
the mathematical definition of X25519 as given in~\cite[Sec.~2]{Ber06}.
We accomplish this step of the proof by extending the Coq library
for elliptic curves~\cite{DBLP:conf/itp/BartziaS14} by Bartzia and Strub to
Benoit Viguier's avatar
Benoit Viguier committed
45
support Montgomery curves (and in particular Curve25519).
Peter Schwabe's avatar
Peter Schwabe committed
46
This extension may be of independent interest.
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
47

Peter Schwabe's avatar
Peter Schwabe committed
48
49
\subheading{Related work.}
\todo{Fix this subsection}
Benoit Viguier's avatar
Benoit Viguier committed
50
51
52
53
54
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.
55
56
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
57
However this first method cannot be applied to an existing piece of software.
Benoit Viguier's avatar
Benoit Viguier committed
58
59
60
61
62

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
63

64
65
\todo{Separate verification of existing code from generating proof-carrying code.}

Benoit Viguier's avatar
Benoit Viguier committed
66
Similar approaches have been used to prove the correctness of OpenSSL
Peter Schwabe's avatar
Peter Schwabe committed
67
HMAC~\cite{Beringer2015VerifiedCA} and . Compared to
Benoit Viguier's avatar
Benoit Viguier committed
68
69
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
70
71

Using the synthesis approach, Zinzindohou{\'{e}} et al. wrote an verified extensible
72
73
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
74
75

Coq does not only allows verification but also synthesis.
76
77
78
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
79

80
Curve25519 implementations has already been under the scrutiny~\cite{Chen2014VerifyingCS}.
Benoit Viguier's avatar
done    
Benoit Viguier committed
81
82
83
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
84
85
86
87
88
89
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
90

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

96
\subheading{Organization of this paper.}
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
97
98
99
100
101
102
103
104
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
105

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