intro.tex 6.68 KB
 Peter Schwabe committed Jun 20, 2019 1 2 XXX: NaCl XXX: TweetNaCl (find real-world use of TweetNaCl?)  Benoit Viguier committed Jun 21, 2019 3 4 5 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 Zeromq a messaging queue system uses tweetnacl to provide portability to it's users. http://zeromq.org/  Peter Schwabe committed Jun 20, 2019 6   Benoit Viguier committed Jun 21, 2019 7 8  XXX:  Peter Schwabe committed Jun 20, 2019 9 10 11 12 13 14 15 TweetNaCl is the first cryptographic library that allows correct functionality to be verified by auditors with reasonable effort'' XXX: One core component of TweetNaCl (and NaCl) is X25519, mention use of X25519 in the wild.  Benoit Viguier committed Jun 21, 2019 16 17 18 19 Originally, the name Curve25519'' referred to this keyexchange protocol, 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.  Peter Schwabe committed Jun 20, 2019 20   Benoit Viguier committed Jun 21, 2019 21 22 TweetNaCl~\cite{BGJ+15} is a compact reimplementation of the NaCl~\cite{BLS12} high security cryptographic library.  Benoit Viguier committed Jun 06, 2019 23 24 25 It does not aim for high speed application and has been optimized for source code compactness (100 tweets). It maintains some degree of readability in order to be easily auditable.  Benoit Viguier committed May 24, 2019 26   Benoit Viguier committed Jun 21, 2019 27 This library makes use of Curve25519~\cite{Ber06}, a function over a \F{p}-restricted  Benoit Viguier committed Jun 04, 2019 28 29 $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 committed Jun 21, 2019 30 This function is used by a wide variety of applications~\cite{this-that-use-curve25519}  Benoit Viguier committed Jun 04, 2019 31 32 to establish a shared secret over an insecure channel.  Benoit Viguier committed Jun 21, 2019 33 34 35 36 37 38 39  \subheading{Contribution of this paper} \todo{Proof that TweetNaCl's X25519 code correctly implements math definition from 25519 paper} \todo{State additional contributions, e.g., extension of EC framework by Bartiza and Strub.}  Benoit Viguier committed Jun 04, 2019 40 Implementing cryptographic primitives without any bugs is difficult.  Benoit Viguier committed Jun 06, 2019 41 42 43 44 45 46 While tests provides with code coverage, they still don't cover 100\% of the possible input values. In order to get formal guaranties a software meets its specifications, two methodologies exist. The first one is by synthesizing a formal specification and generating machine code by refinment in order to get a software correct by construction.  Benoit Viguier committed Jun 21, 2019 47 48 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 49 50 51 52 53  However this first method cannot be applied to an existing piece of software. In such case we need to write the specifications and then verify the correctness of the implementation.  Peter Schwabe committed Jun 20, 2019 54 \subheading{Our Formal Approach.}  Benoit Viguier committed May 27, 2019 55 Verifying an existing cryptographic library, we use the second approach.  Benoit Viguier committed May 24, 2019 56 Our method can be seen as a static analysis over the input values coupled  Benoit Viguier committed May 17, 2019 57 with the formal proof that the code of the algorithm matches its specification.  Benoit Viguier committed Feb 09, 2018 58   Benoit Viguier committed Jun 21, 2019 59 60 61 We use Coq~\cite{coq-faq}, a formal system that allows us to machine-check our proofs. A famous example of its use is the proof of the Four Color Theorem~\cite{gonthier2008formal}. The CompCert, a C~compiler~\cite{Leroy-backend} proven correct and sound is being build on top of it.  Benoit Viguier committed Jun 06, 2019 62 To prove its correctness, CompCert uses multiple intermediate languages. The first step of CompCert is done by the parser \textit{clightgen}.  Benoit Viguier committed Jun 21, 2019 63 It takes as input C code and generates its Clight~\cite{Blazy-Leroy-Clight-09} translation.  Benoit Viguier committed Jun 06, 2019 64 65  Using this intermediate representation Clight, we use the Verifiable Software Toolchain  Benoit Viguier committed Jun 21, 2019 66 (VST)~\cite{2012-Appel}, a framework which uses Separation logic~\cite{1969-Hoare,Reynolds02separationlogic}  Benoit Viguier committed Jun 06, 2019 67 68 69 70 71 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. We write a specification of the crypto scalar multiplication of TweetNaCl and using VST we prove that the code matches our definitions.  Benoit Viguier committed Jun 21, 2019 72 Bartzia and Strub wrote a formal library for elliptic curves~\cite{DBLP:conf/itp/BartziaS14}.  Benoit Viguier committed Jun 06, 2019 73 74 75 We extend it 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.  Peter Schwabe committed Jun 20, 2019 76 \subheading{Related work.}  Benoit Viguier committed Jun 06, 2019 77   Peter Schwabe committed Jun 20, 2019 78 79 \todo{Separate verification of existing code from generating proof-carrying code.}  Benoit Viguier committed Jun 21, 2019 80 Similar approaches have been used to prove the correctness of OpenSSL HMAC~\cite{Beringer2015VerifiedCA}  Peter Schwabe committed Jun 20, 2019 81 and SHA-256~\cite{2015-Appel}. Compared to their work  Benoit Viguier committed Jun 06, 2019 82 83 84 85 our approaches makes a complete link between the C implementation and the formal mathematical definition of the group theory behind elliptic curves. Using the synthesis approach, Zinzindohou{\'{e}} et al. wrote an verified extensible  Benoit Viguier committed Jun 21, 2019 86 87 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 88 89  Coq does not only allows verification but also synthesis.  Benoit Viguier committed Jun 21, 2019 90 91 92 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 93   Benoit Viguier committed Jun 21, 2019 94 Curve25519 implementations has already been under the scrutiny~\cite{Chen2014VerifyingCS}.  Benoit Viguier committed Jun 06, 2019 95 96 97 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 98 \todo{Add 1-2 sentences about how this compares? Different limitations etc.}  Benoit Viguier committed Jun 06, 2019 99   Peter Schwabe committed Jun 20, 2019 100 \subheading{Reproducing the proofs.}  Benoit Viguier committed Jun 06, 2019 101 102 103 104 To maximize reusability of our results we placed the code of our formal proofs presented in this paper into the public domain. They are available at XXXXXXX with instructions of how to compile and verify our proofs.  Peter Schwabe committed Jun 20, 2019 105 106 \subheading{Organization of this paper.} Section~\ref{sec2-implem} gives the necessary background on Curve25519  Benoit Viguier committed Jun 06, 2019 107 implementation in TweetNaCl and provides the specifications we later prove correct.  Peter Schwabe committed Jun 20, 2019 108 109 Section~\ref{sec3-maths} describes our extension of the formal library by Bartzia and Strub. Section~\ref{sec4-refl} makes the link between the mathematical model and the C implementation.  Benoit Viguier committed Jun 06, 2019 110 In this section we also describe some of the techniques we used to speed up some of the proofs.  Peter Schwabe committed Jun 20, 2019 111 Section~\ref{sec5-vst} provides with attention points a VST user should be careful  Benoit Viguier committed Jun 06, 2019 112 113 of in order to avoid unnecessary work.  Benoit Viguier committed Jun 04, 2019 114   Benoit Viguier committed May 30, 2019 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 % 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