1_Introduction.tex 1.72 KB
Newer Older
 Benoit Viguier committed Nov 13, 2017 1 2 \section{Introduction}  Benoit Viguier committed Feb 09, 2018 3 Implementing cryptographic primitives without any bugs is hard.  Benoit Viguier committed May 17, 2019 4 While tests provides a code coverage and are used in the limits,  Benoit Viguier committed Mar 13, 2018 5 they still don't cover 100\% of the possible input values.  Benoit Viguier committed May 17, 2019 6 7 Our method is can be seen as a static analysis over the input values coupled with the formal proof that the code of the algorithm matches its specification.  Benoit Viguier committed Feb 09, 2018 8 9 10 11  TweetNaCl\cite{BGJ+15} is a compact reimplementation of the NaCl\cite{BLS12} library. It does not aim for high speed application and has been optimized for source code compactness.  Benoit Viguier committed May 17, 2019 12 It maintains some degree of readability in order to be easily auditable.  Benoit Viguier committed Feb 09, 2018 13   Benoit Viguier committed May 03, 2019 14 This library makes use of Curve25519\cite{Ber06}, a function over a \F{p}-restricted  Benoit Viguier committed May 17, 2019 15 16 $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 Feb 09, 2018 17   Benoit Viguier committed May 17, 2019 18 19 20 Coq is a formal system that allows to machine-check our proofs. A famous example of its use is the proof of the Four Color Theorem. The Compcert\cite{Leroy-backend} compiler and the Verifiable Software Toolchain (VST)\cite{2012-Appel} are build  Benoit Viguier committed Feb 09, 2018 21 22 23 on top of it. Our approach is as follow, we use the \textit{clightgen} tool from Compcert to  Benoit Viguier committed Nov 13, 2017 24 generate the \textit{semantic version} (Clight\cite{Blazy-Leroy-Clight-09}) of  Benoit Viguier committed May 17, 2019 25 26 27 28 29 30 31 the TweetNaCl C code. Using the Separation logic\cite{1969-Hoare,Reynolds02separationlogic} with with the Verifiable Software Toolchain we show that the semantics of the program satisfies a functionnal specification in Coq. We extend the work of Bartzia and Strub \cite{DBLP:conf/itp/BartziaS14} to support Montgomery curves. With this formalization, we prove the correctness of a generic Montgomery ladder and show that our specification can be seen as an instance of it.