intro.tex 6.18 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 \subheading{Related work.}  Benoit Viguier committed Aug 05, 2019 49 50 51 52 Two methodologies exist to get formal guarantees a software meets its specifications. 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 committed Jul 22, 2019 53   Benoit Viguier committed Aug 05, 2019 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 % One of the earliest example of this first approach is the % B-method~\cite{Abrial:1996:BAP:236705} in 1986. Using the synthesis approach, Zinzindohou{\'{e}} et al. wrote an verified extensible 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. Coq does not only allows verification but also synthesis~\cite{CpdtJFR}. 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}. The verification approach, have been used to prove the correctness of OpenSSL HMAC~\cite{Beringer2015VerifiedCA} and SHA-256~\cite{2015-Appel}. Compared to  Benoit Viguier committed Jul 22, 2019 70 71 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 72   Benoit Viguier committed Jul 03, 2019 73 74 75 76 77 78 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 79   Benoit Viguier committed Aug 05, 2019 80 81 82 83 It has to be noted that Curve25519 implementations has already been under the scrutiny~\cite{Chen2014VerifyingCS}. However in this paper we provide a proofs of correctness and soundness of a C program up to the theory of elliptic curves.  Peter Schwabe committed Jun 20, 2019 84 \subheading{Reproducing the proofs.}  Benoit Viguier committed Jul 22, 2019 85 To maximize reusability of our results we placed the code of our formal proof  Benoit Viguier committed Jun 06, 2019 86 presented in this paper into the public domain. They are available at XXXXXXX  Benoit Viguier committed Jul 22, 2019 87 with instructions of how to compile and verify our proof.  Benoit Viguier committed Aug 05, 2019 88 89 A description of the content of the archive is provided in Appendix~\ref{appendix:proof-folders}.  Benoit Viguier committed Jun 06, 2019 90   Peter Schwabe committed Jun 20, 2019 91 \subheading{Organization of this paper.}  Benoit Viguier committed Aug 12, 2019 92 \sref{sec:preliminaries} give the necessary background on Curve25519  Benoit Viguier committed Aug 05, 2019 93 implementation and a rough understanding of how formal verification works.  Benoit Viguier committed Aug 12, 2019 94 95 96 \sref{sec:C-Coq-RFC} provides the specification of X25519 and the in addition to proofs techniques used to show the correctness with respect to RFC~7748~\cite{rfc7748}. \sref{sec:maths} describes our extension of the formal library by Bartzia  Benoit Viguier committed Jul 03, 2019 97 98 and Strub and the correctness of X25519 implementation with respect to Bernstein specifications~\cite{Ber14}.  Benoit Viguier committed Aug 12, 2019 99 And lastly in \sref{sec:Conclusion} we discuss the trust in this proof.  Benoit Viguier committed Jun 06, 2019 100   Benoit Viguier committed Jun 04, 2019 101   Benoit Viguier committed May 30, 2019 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 % 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