1_Introduction.tex 1.56 KB
Newer Older
Benoit Viguier's avatar
Benoit Viguier committed
1
2
\section{Introduction}

3
Implementing cryptographic primitives without any bugs is hard.
Benoit Viguier's avatar
Benoit Viguier committed
4
5
6
While tests provides a some code coverage and are used in the limits,
they still don't cover 100\% of the possible input values.
Using Coq, we prove the correctness of the scalar multiplication in Tweetnacl.
7
8
9
10
11
12
13

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.
It maintains some degree of readability in order to be
easily auditable.

Benoit Viguier's avatar
Benoit Viguier committed
14
15
16
17
18
19
20
This library makes use of Curve25519\cite{Ber06}, a function over a \F{p}-restricted
x-coordinate 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$.
% It defines the function \texttt{crypto\_scalarmult} which
% takes as input a scalar $n$ and the $x$ coordinate of a
% point $P$ and returns the $x$ coordinate of the
% point $[n]P$.
21
22
23
24
25
26

Coq is a formal system that allows us to machine-check our proofs. The Compcert\cite{Leroy-backend}
compiler and the Verifiable Software Toolchain (VST)\cite{2012-Appel} are build
on top of it.

Our approach is as follow, we use the \textit{clightgen} tool from Compcert to
Benoit Viguier's avatar
Benoit Viguier committed
27
generate the \textit{semantic version} (Clight\cite{Blazy-Leroy-Clight-09}) of
28
29
30
31
the TweetNaCl C code. Using the Separation logic\cite{1969-Hoare,Reynolds02separationlogic}
with (VST) we show that the semantics of the program satisfies a functionnal
specification in Coq. We then prove that this specification represent the scalar
multiplication on Curve25519.