intro.tex 6.26 KB
 Peter Schwabe committed Jul 29, 2019 1 2 \section{Introduction} \label{sec:intro}  Peter Schwabe committed Jun 20, 2019 3   Benoit Viguier committed Aug 01, 2019 4 5 The Networking and Cryptography library (NaCl)~\cite{BLS12} is an easy-to-use, high-security, high-speed cryptography library.  Peter Schwabe committed Jul 30, 2019 6 It uses specialized code for different platform, which makes it rather complex and hard to audit.  Benoit Viguier committed Aug 01, 2019 7 8 TweetNaCl~\cite{BGJ+15} is a compact re-implementation in C of the core functionalities of NaCl and is claimed to be  Peter Schwabe committed Jul 29, 2019 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 committed Jul 30, 2019 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.  Peter Schwabe committed Jul 29, 2019 14   Peter Schwabe committed Jul 30, 2019 15 One core component of TweetNaCl (and NaCl) is the key-exchange protocol X25519~\cite{rfc7748}.  Peter Schwabe committed Jul 29, 2019 16 This protocol is being used by a wide variety of applications~\cite{things-that-use-curve25519}  Peter Schwabe committed Jul 30, 2019 17 such as SSH, Signal Protocol, Tor, Zcash, and TLS to establish a shared secret over  Peter Schwabe committed Jul 29, 2019 18 an insecure channel.  Benoit Viguier committed Aug 01, 2019 19 The X25519 key exchange protocol is a an $x$-coordinate only  Peter Schwabe committed Jul 30, 2019 20 elliptic-curve Diffie-Hellman key-exchange using the Montgomery  Benoit Viguier committed Aug 01, 2019 21 curve $E: y^2 = x^3 + 486662 x^2 + x$ over the field $\F{\p}$.  Peter Schwabe committed Jul 30, 2019 22 Note that originally, the name Curve25519'' referred to the key exchange protocol,  Benoit Viguier committed Jun 25, 2019 23 but Bernstein suggested to rename the scheme to X25519 and to use the name  Peter Schwabe committed Jul 30, 2019 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.  Benoit Viguier committed Jun 21, 2019 26 27  \subheading{Contribution of this paper}  Peter Schwabe committed Jul 30, 2019 28 We provide a mechanized formal proof of the correctness of the X25519  Benoit Viguier committed Aug 01, 2019 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 committed Jul 30, 2019 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 committed Aug 01, 2019 34 to establish a link between C and Coq.  Peter Schwabe committed Jul 30, 2019 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 committed Aug 01, 2019 45 support Montgomery curves (and in particular Curve25519).  Peter Schwabe committed Jul 30, 2019 46 This extension may be of independent interest.  Benoit Viguier committed Jul 03, 2019 47   Peter Schwabe committed Jul 30, 2019 48 49 \subheading{Related work.} \todo{Fix this subsection}  Benoit Viguier committed Jul 22, 2019 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.  Benoit Viguier committed Jun 21, 2019 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 committed Jun 06, 2019 57 However this first method cannot be applied to an existing piece of software.  Benoit Viguier committed Jul 22, 2019 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 committed Jun 06, 2019 63   Peter Schwabe committed Jun 20, 2019 64 65 \todo{Separate verification of existing code from generating proof-carrying code.}  Benoit Viguier committed Jul 22, 2019 66 Similar approaches have been used to prove the correctness of OpenSSL  Peter Schwabe committed Jul 30, 2019 67 HMAC~\cite{Beringer2015VerifiedCA} and . Compared to  Benoit Viguier committed Jul 22, 2019 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 committed Jun 06, 2019 70 71  Using the synthesis approach, Zinzindohou{\'{e}} et al. wrote an verified extensible  Benoit Viguier committed Jun 21, 2019 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 committed Jun 06, 2019 74 75  Coq does not only allows verification but also synthesis.  Benoit Viguier committed Jun 21, 2019 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 committed Jun 06, 2019 79   Benoit Viguier committed Jun 21, 2019 80 Curve25519 implementations has already been under the scrutiny~\cite{Chen2014VerifyingCS}.  Benoit Viguier committed Jun 06, 2019 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 committed Jul 03, 2019 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 committed Jun 06, 2019 90   Peter Schwabe committed Jun 20, 2019 91 \subheading{Reproducing the proofs.}  Benoit Viguier committed Jul 22, 2019 92 To maximize reusability of our results we placed the code of our formal proof  Benoit Viguier committed Jun 06, 2019 93 presented in this paper into the public domain. They are available at XXXXXXX  Benoit Viguier committed Jul 22, 2019 94 with instructions of how to compile and verify our proof.  Benoit Viguier committed Jun 06, 2019 95   Peter Schwabe committed Jun 20, 2019 96 \subheading{Organization of this paper.}  Benoit Viguier committed Jul 03, 2019 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 committed Jun 06, 2019 105   Benoit Viguier committed Jun 04, 2019 106   Benoit Viguier committed May 30, 2019 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