1_Introduction.tex 1.66 KB
Newer Older
Benoit Viguier's avatar
Benoit Viguier committed
1
2
3
4
5
\section{Introduction}

Implementing cryptographic primitives without any bugs is hard. While tests
provides a decent code coverage, they don't cover 100\% of the possible values.

6
7
8
9
10
11
We verify the implementation in C of Curve25519 in Tweetnacl\cite{BGJ+15}.




Using the \textit{clightgen} tool from Compcert\cite{Leroy-backend}, we can
Benoit Viguier's avatar
Benoit Viguier committed
12
13
14
generate the \textit{semantic version} (Clight\cite{Blazy-Leroy-Clight-09}) of
the C code. Using the Floyd–Hoare logic\cite{1969-Hoare} with the Verifiable
Software Toolchain (VST)\cite{2012-Appel} we can show that the semantic of the
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
program is equivalent to a functionnal specification in Coq.
We can then prove that this specification is represent the scalar multiplication
on Curve25519\cite{}.

\subsection{Meet-in-the-middle Approach}

In order to prove that \texttt{crypto\_scalarmult} is computing a scalar
multiplication over the x-coordinate of a point P, we need to define multiples
levels of specifications and show equivalence between them.

\begin{enumerate}
  \item Write a high level specification (over a generic field $\mathbb{F}$).
  \item Show that the high level specification is equivalent to the
  computation of a montgomery ladder.
  \item Write a low level specification (e.g. over lists of $\mathbb{Z}$).
  \item Show that the low level specification represent the operations of
  defined C code.
  \item Show that the low level specification are equivalent to simple
  operations in $\mathbb{Z}_{2^{255}-19}$ (middle level specification).
  \item Show that the middle level specification is an instance of the high
  level one.
\end{enumerate}

The equivalence between each level, garantees us the correctness of the
implementation.