1_intro.tex 6.72 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.
Benoit Viguier's avatar
Benoit Viguier committed
6
It uses specialized code for different platforms, 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
X25519 for the protocol and Curve25519 for the underlying elliptic curve~\cite{Ber14}.
25
We make use of this updated terminology 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
implementation in TweetNaCl.
Benoit Viguier's avatar
Benoit Viguier committed
30
31
32
33
34
35
This proof is done in three steps:
we first formalize RFC~7748~\cite{rfc7748} in Coq~\cite{coq-faq}.
% This part uses generic techniques to facilitate later proofs.

In a second step we prove equivalence of the C implementation of X25519
to our RFC formalization.
Peter Schwabe's avatar
Peter Schwabe committed
36
This part of the proof uses the Verifiable Software Toolchain (VST)~\cite{2012-Appel}
Benoit Viguier's avatar
Benoit Viguier committed
37
to establish a link between C and Coq.
Peter Schwabe's avatar
Peter Schwabe committed
38
39
40
41
42
43
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.

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

Peter Schwabe's avatar
Peter Schwabe committed
51
\subheading{Related work.}
52
Two methodologies exist to get formal guarantees that software meets its specification.
Benoit Viguier's avatar
Benoit Viguier committed
53
54
55
This can be done either by synthesizing a formal specification and then generating
machine code by refinement, or by writing a specification and verifying that the
implementation satisfies it.
Benoit Viguier's avatar
Benoit Viguier committed
56

Benoit Viguier's avatar
Benoit Viguier committed
57
58
% One of the earliest example of this first approach is the
% B-method~\cite{Abrial:1996:BAP:236705} in 1986.
Benoit Viguier's avatar
Benoit Viguier committed
59
Using the synthesis approach, Zinzindohou{\'{e}} et al. wrote a verified extensible
Benoit Viguier's avatar
Benoit Viguier committed
60
61
62
63
library of elliptic curves~\cite{Zinzindohoue2016AVE} in F*~\cite{DBLP:journals/corr/BhargavanDFHPRR17}.
This served as ground work for the cryptographic library HACL*~\cite{zinzindohoue2017hacl}
used in the NSS suite from Mozilla.

Benoit Viguier's avatar
Benoit Viguier committed
64
Coq not only allows verification but also synthesis~\cite{CpdtJFR}.
Benoit Viguier's avatar
Benoit Viguier committed
65
66
67
68
69
70
Erbsenm; Philipoom; Gross; and Chlipala et al. make use of it to have
correct-by-construction finite field arithmetic~\cite{Philipoom2018CorrectbyconstructionFF}.
In such way, they synthesized~\cite{Erbsen2016SystematicSO} certified elliptic curve
implementations~\cite{Erbsen2017CraftingCE}. These are now being used in
BoringSSL~\cite{fiat-crypto}.

Benoit Viguier's avatar
Benoit Viguier committed
71
The verification approach has been used to prove the correctness of OpenSSL
Benoit Viguier's avatar
Benoit Viguier committed
72
HMAC~\cite{Beringer2015VerifiedCA} and SHA-256~\cite{2015-Appel}. Compared to
73
that work our approach makes a complete link between the C implementation and
Benoit Viguier's avatar
Benoit Viguier committed
74
the formal mathematical definition of the group theory behind elliptic curves.
Benoit Viguier's avatar
done    
Benoit Viguier committed
75

76
Synthesis approaches force the user to depend on generated code which may not
Benoit Viguier's avatar
Benoit Viguier committed
77
78
be optimal (speed, compactness...) and they require compiler tweaks in order
to achieve the desired properties. On the other hand, carefully handcrafted
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
79
optimized code will force the verifier to consider all the possible special cases
80
81
and write a low level specification of the details of the code in order to prove
the correctness of the algorithm.
Benoit Viguier's avatar
done    
Benoit Viguier committed
82

Benoit Viguier's avatar
Benoit Viguier committed
83
It has to be noted that Curve25519 implementations have already been under scrutiny~\cite{Chen2014VerifyingCS}.
Benoit Viguier's avatar
Benoit Viguier committed
84
85
86
However in this paper we provide a proofs of correctness and soundness of a C program up to
the theory of elliptic curves.

87
\subheading{Reproducing the proofs.}
Benoit Viguier's avatar
Benoit Viguier committed
88
To maximize reusability of our results we placed the code of our formal proof
Benoit Viguier's avatar
Benoit Viguier committed
89
90
91
presented in this paper into the public domain.
\ifpublic
They are available at XXXXXXX
Benoit Viguier's avatar
Benoit Viguier committed
92
with instructions of how to compile and verify our proof.
Benoit Viguier's avatar
Benoit Viguier committed
93
94
95
96
\else
They are available in the associated materials with instructions of how
to compile and verify our proof.
\fi
Benoit Viguier's avatar
Benoit Viguier committed
97
98
A description of the content of the archive is provided in
Appendix~\ref{appendix:proof-folders}.
Benoit Viguier's avatar
done    
Benoit Viguier committed
99

100
\subheading{Organization of this paper.}
101
102
\sref{sec:preliminaries} give the necessary background on Curve25519 and X25519
implementations and a brief explanation of how formal verification works.
Benoit Viguier's avatar
Benoit Viguier committed
103
\sref{sec:Coq-RFC} provides our formalization of RFC~7748~\cite{rfc7748}'s X25519.
Benoit Viguier's avatar
Benoit Viguier committed
104
\sref{sec:C-Coq} provides the specifications of TweetNaCl's X25519 and some of the
Benoit Viguier's avatar
Benoit Viguier committed
105
proofs techniques used to show the correctness with respect to RFC~7748~\cite{rfc7748}.
Benoit Viguier's avatar
Benoit Viguier committed
106
\sref{sec:maths} describes our extension of the formal library by Bartzia
107
and Strub and the correctness of X25519 implementation with respect to Bernstein's
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
108
specifications~\cite{Ber14}.
109
And lastly in \sref{sec:Conclusion} we discuss the trusted code base of this proof.
Benoit Viguier's avatar
Benoit Viguier committed
110
111
112
113
114
115
116
117
\fref{tikz:ProofOverview} shows a graph of dependencies of the proofs.

\begin{figure}[h]
  \centering
  \include{tikz/proof}
  \caption{Structure of the proof}
  \label{tikz:ProofOverview}
\end{figure}
Benoit Viguier's avatar
done    
Benoit Viguier committed
118

Benoit Viguier's avatar
forward    
Benoit Viguier committed
119

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