Commit 8d2303d4 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

more rewrite

parent 64af5cd9
\documentclass{article}
\usepackage{geometry}
\geometry{
a4paper,
total={190mm,257mm},
left=10mm,
top=20mm,
}
\usepackage{epsfig}
\usepackage{setup}
\input{macros}
\begin{document}
Generic definition of the ladder:
\begin{lstlisting}[language=Coq]
(* Define a typeclass to encapsulate the operations *)
Class Ops (T T': Type) (Mod: T -> T):=
{
+ : T -> T -> T; (* Add *)
* : T -> T -> T; (* Mult *)
- : T -> T -> T; (* Sub *)
x^2 : T -> T; (* Square *)
C_0 : T; (* Const 0 *)
C_1 : T; (* Const 1 *)
C_121665: T; (* const (a-2)/4 *)
Sel25519: Z -> T -> T -> T;(* CSWAP *)
Getbit: Z -> T' -> Z; (* ith bit *)
}.
Fixpoint montgomery_rec (m : nat) (z : T')
(a: T) (b: T) (c: T) (d: T) (e: T) (f: T) (x: T) :
(* a: x2 *)
(* b: x3 *)
(* c: z2 *)
(* d: z3 *)
(* e: temporary var *)
(* f: temporary var *)
(* x: x1 *)
(T * T * T * T * T * T) :=
match m with
| 0%nat => (a,b,c,d,e,f)
| S n =>
let r := Getbit (Z.of_nat n) z in
(* k_t = (k >> t) & 1 *)
(* swap <- k_t *)
let (a, b) := (Sel25519 r a b, Sel25519 r b a) in
(* (x_2, x_3) = cswap(swap, x_2, x_3) *)
let (c, d) := (Sel25519 r c d, Sel25519 r d c) in
(* (z_2, z_3) = cswap(swap, z_2, z_3) *)
let e := a + c in (* A = x_2 + z_2 *)
let a := a - c in (* B = x_2 - z_2 *)
let c := b + d in (* C = x_3 + z_3 *)
let b := b - d in (* D = x_3 - z_3 *)
let d := e ^2 in (* AA = A^2 *)
let f := a ^2 in (* BB = B^2 *)
let a := c * a in (* CB = C * B *)
let c := b * e in (* DA = D * A *)
let e := a + c in (* x_3 = (DA + CB)^2 --- (1/2) *)
let a := a - c in (* z_3 = x_1 * (DA - CB)^2 --- (1/3) *)
let b := a ^2 in (* z_3 = x_1 * (DA - CB)^2 --- (2/3) *)
let c := d - f in (* E = AA - BB *)
let a := c * C_121665 in (* z_2 = E * (AA + a24 * E) --- (1/3) *)
let a := a + d in (* z_2 = E * (AA + a24 * E) --- (2/3) *)
let c := c * a in (* z_2 = E * (AA + a24 * E) --- (3/3) *)
let a := d * f in (* x_2 = AA * BB *)
let d := b * x in (* z_3 = x_1 * (DA - CB)^2 --- (3/3) *)
let b := e ^2 in (* x_3 = (DA + CB)^2 --- (2/2) *)
let (a, b) := (Sel25519 r a b, Sel25519 r b a) in
(* (x_2, x_3) = cswap(swap, x_2, x_3) *)
let (c, d) := (Sel25519 r c d, Sel25519 r d c) in
(* (z_2, z_3) = cswap(swap, z_2, z_3) *)
montgomery_rec n z a b c d e f x
end.
Definition get_a (t:(T * T * T * T * T * T)) : T :=
match t with
(a,b,c,d,e,f) => a
end.
Definition get_c (t:(T * T * T * T * T * T)) : T :=
match t with
(a,b,c,d,e,f) => c
end.
\end{lstlisting}
\newpage
Instanciation of the Class \Coqe{Ops} with operations over $\ZZ$ and modulo \p.
\begin{lstlisting}[language=Coq]
Definition modP x := Z.modulo x (Z.pow 2 255 - 19).
(* Encapsulate in a module. *)
Module Mid.
Definition getCarry (m:Z) : Z := Z.shiftr m n.
Definition getResidue (m:Z) : Z := m - Z.shiftl (getCarry m) n.
Definition car25519 (n:Z) : Z := 38 * getCarry 256 n + getResidue 256 n.
(* The carry operation is invariant under modulo *)
Lemma Zcar25519_correct: forall n, n:GF = (Mid.car25519 n) :GF.
(* Define Mid.A, Mid.M ... *)
Definition A a b := Z.add a b.
Definition M a b := Mid.car25519 (Mid.car25519 (Z.mul a b)).
Definition Zub a b := Z.sub a b.
Definition Sq a := M a a.
Definition C_0 := 0.
Definition C_1 := 1.
Definition C_121665 := 121665.
Definition Sel25519 (b p q:Z) := if (Z.eqb b 0) then p else q.
Definition getbit (i:Z) (a: Z) :=
if (Z.ltb a 0) then
0
else
if (Z.ltb i 0) then
Z.land a 1
else
Z.land (Z.shiftr a i) 1.
End Mid.
Definition ZPack25519 n :=
Z.modulo n (Z.pow 2 255 - 19).
Definition Zclamp (n : Z) : Z :=
(Z.lor (Z.land n (Z.land (Z.ones 255) (-8))) (Z.shiftl 64 (31 * 8))).
(* x^{p - 2} *)
Definition ZInv25519 (x:Z) : Z := Z.pow x (Z.pow 2 255 - 21).
(* instanciate over Z *)
Instance Z_Ops : (Ops Z Z modP) := {}.
Proof.
apply Mid.A. (* instanciate + *)
apply Mid.M. (* instanciate * *)
apply Mid.Zub. (* instanciate - *)
apply Mid.Sq. (* instanciate x^2 *)
apply Mid.C_0. (* instanciate Const 0 *)
apply Mid.C_1. (* instanciate Const 1 *)
apply Mid.C_121665. (* instanciate (a-2)/4 *)
apply Mid.Sel25519. (* instanciate CSWAP *)
apply Mid.getbit. (* instanciate ith bit *)
Defined.
(* instanciate montgomery_rec with Z_Ops *)
Definition ZCrypto_Scalarmult n p :=
let t := montgomery_rec
255 (* iterate 255 times *)
(Zclamp n) (* clamped n *)
1 (* x_2 *)
(ZUnpack25519 p) (* x_3 *)
0 (* z_2 *)
1 (* z_3 *)
0 (* dummy *)
0 (* dummy *)
(ZUnpack25519 p) (* x_1 *) in
ZPack25519 (Z.mul (get_a t) (ZInv25519 (get_c t))).
\end{lstlisting}
\newpage
\begin{lstlisting}[language=Coq]
Definition Crypto_Scalarmult n p :=
let t := (montgomery_rec 255
(clamp n) Low.C_1 (Unpack25519 p) Low.C_0 Low.C_1
Low.C_0 Low.C_0 (Unpack25519 p)) in
let a := get_a t in
let c := get_c t in
Pack25519 (Low.M a (Inv25519 c)).
Definition CSM := Crypto_Scalarmult.
Theorem Crypto_Scalarmult_Eq : forall (n p:list Z),
Zlength n = 32 ->
Zlength p = 32 ->
Forall (fun x : Z, 0 <= x /\ x < 2 ^ 8) n ->
Forall (fun x : Z, 0 <= x /\ x < 2 ^ 8) p ->
ZofList 8 (Crypto_Scalarmult n p) =
ZCrypto_Scalarmult (ZofList 8 n) (ZofList 8 p).
\end{lstlisting}
\end{document}
\section{Conclusion}
\label{Conclusion}
\label{sec:Conclusion}
Any formal system relies on a trusted base. In this section we describe our
chain of trust.
......@@ -59,4 +59,10 @@ o[i] = aux1 + aux2;
done with this architecture \cite{2015-Appel,coq-faq}.
\end{itemize}
\subsection{Proof toolchain}
\subsection{Modifications in TweetNaCl}
The upper 64 indexes of the \TNaCle{i64 x[80]} intermediate variable of
\TNaCle{crypto_scalarmult} were adding unnecessary complexity to the code,
we fixed it.
\todo{Mention Peter Wu and Jason A. Donenfeld change to car25519}
\section{Proving that X25519 in Coq matches the mathematical model}
\label{sec3-maths}
\label{sec:maths}
In this section we first present the work of Bartzia and Strub \cite{DBLP:conf/itp/BartziaS14} (\ref{Weierstrass}).
We extend it to support Montgomery curves (\ref{montgomery}) with homogeneous coordinates (\ref{projective}) and prove the correctness of the ladder (\ref{ladder}).
\begin{theorem}\label{thm:Elliptic-CSM}
\todo{DESCRIBE}
\end{theorem}
In this section we first present the work of Bartzia and Strub \cite{DBLP:conf/itp/BartziaS14} (\ref{subsec:ECC-Weierstrass}).
We extend it to support Montgomery curves (\ref{subsec:ECC-Montgomery}) with homogeneous coordinates (\ref{subsec:ECC-projective}) and prove the correctness of the ladder (\ref{subsec:ECC-ladder}).
We then prove the Montgomery ladder computes
the x-coordinate of scalar multiplication over $\F{p^2}$
(Theorem 2.1 by Bernstein \cite{Ber06}) where $p$ is the prime $\p$.
\subsection{Formalization of Elliptic Curves}
\label{subsec:ECC}
We consider elliptic curves over a field $\K$. We assume that the
characteristic of $\K$ is neither 2 or 3.
\begin{definition}
\begin{dfn}
Let a field $\K$, using an appropriate choice of coordinates, an elliptic curve $E$
is a plane cubic algebraic curve $E(x,y)$ defined by an equation of the form:
$$E : y^2 + a_1 xy + a_3 y = x^3 + a_2 x^2 + a_4 x + a_6$$
......@@ -21,18 +26,19 @@ where the $a_i$'s are in \K\ and the curve has no singular point (\ie no cusps
or self-intersections). The set of points, written $E(\K)$, is formed by the
solutions $(x,y)$ of $E$ augmented by a distinguished point $\Oinf$ (called point at infinity):
$$E(\K) = \{(x,y) \in \K \times \K | E(x,y)\} \cup \{\Oinf\}$$
\end{definition}
\end{dfn}
\subsubsection{Weierstra{\ss} Curves}
\label{Weierstrass}
\label{subsec:ECC-Weierstrass}
This equation $E(x,y)$ can be reduced into its short Weierstra{\ss} form.
\begin{definition}
\begin{dfn}
Let $a \in \K$, and $b \in \K$ such that $$\Delta(a,b) = -16(4a^3 + 27b^2) \neq 0.$$
The \textit{elliptic curve} $E_{a,b}(\K)$ is the set of all points $(x,y) \in \K^2$ satisfying the equation:
$$y^2 = x^3 + ax + b,$$
along with an additional formal point $\Oinf$, ``at infinity''. Such curve does not present any singularity.
\end{definition}
\end{dfn}
In this setting, Bartzia and Strub defined the parametric type \texttt{ec} which
represent the points on a specific curve. It is parameterized by
......@@ -87,17 +93,18 @@ Definition addec (p1 p2 : ec) : ec :=
\end{lstlisting}
\subsubsection{Montgomery Curves}
\label{montgomery}
\label{subsec:ECC-Montgomery}
Computation over elliptic curves are hard. Speedups can be obtained by using
homogeneous coordinates and other forms than the Weierstra{\ss} form. We consider
the Montgomery form \cite{MontgomerySpeeding}.
\begin{definition}
\begin{dfn}
Let $a \in \K \backslash \{-2, 2\}$, and $b \in \K \backslash \{ 0\}$.
The \textit{Montgomery curve} $M_{a,b}(\K)$ is the set of all points $(x,y) \in \K^2$ satisfying the equation:
$$by^2 = x^3 + ax^2 + x,$$
along with an additional formal point $\Oinf$, ``at infinity''.
\end{definition}
\end{dfn}
Using a similar representation, we defined the parametric type \texttt{mc} which
represent the points on a specific Montgomery curve. It is parameterized by
a \texttt{K : ecuFieldType} -- the type of fields which characteristic is not 2 or 3 --
......@@ -165,7 +172,8 @@ Lemma ec_of_mc_bij : bijective ec_of_mc.
\end{lstlisting}
\subsubsection{Projective Coordinates}
\label{projective}
\label{subsec:ECC-projective}
Points on a projective plane are represented with a triple $(X:Y:Z)$. Any points
except $(0:0:0)$ defines a point on a projective plane. A scalar multiple of a point defines the same point, \ie
for all $\alpha \neq 0$, $(X:Y:Z)$ and $(\alpha X:\alpha Y:\alpha Z)$ defines
......@@ -190,12 +198,12 @@ Hypothesis mcu_no_square : forall x : K, x^+2 != (M#a)^+2 - 4%:R.
\end{lstlisting}
With those coordinates we prove the following lemmas for the addition of two points.
\begin{definition}Define the functions $\chi$ and $\chi_0$:\\
\begin{dfn}Define the functions $\chi$ and $\chi_0$:\\
-- $\chi : M_{a,b}(\K) \to \K \cup \{\infty\}$\\
such that $\chi(\Oinf) = \infty$ and $\chi((x,y)) = x$.\\
-- $\chi_0 : M_{a,b}(\K) \to \K$\\
such that $\chi_0(\Oinf) = 0$ and $\chi_0((x,y)) = x$.
\end{definition}
\end{dfn}
\begin{lemma}
\label{lemma-add}
Let $M_{a,b}(\K)$ be a Montgomery curve such that $a^2-4$ is not a square, and
......@@ -270,7 +278,7 @@ With these two lemmas (\ref{lemma-add} and \ref{lemma-double}), we have the basi
tools to compute efficiently additions and point doubling on projective coordinates.
\subsubsection{Scalar Multiplication Algorithms}
\label{ladder}
\label{subsec:ECC-ladder}
Suppose we have a scalar $n$ and a point $P$ on some curve. The most straightforward
way to compute $n \cdot P$ is to repetitively add $P$ \ie computing $P + \ldots + P$.
......@@ -278,66 +286,24 @@ However there is an more efficient algorithm which makes use of the binary
representation of $n$ and by combining doubling and adding and starting from $\Oinf$.
\eg for $n=11$, we compute $2(2(2(2\Oinf + P)) + P)+ P$.
% \begin{algorithm}
% \caption{Double-and-add for scalar mult.}
% \label{double-add}
% \begin{algorithmic}
% \REQUIRE{Point $P$, scalars $n$ and $m$, $n < 2^m$}
% \ENSURE{$Q = n \cdot P$}
% \STATE $Q \leftarrow \Oinf$
% \FOR{$k$ := $m$ downto $1$}
% \STATE $Q \leftarrow 2Q$
% \IF{$k^{\text{th}}$ bit of $n$ is $1$}
% \STATE $Q \leftarrow Q + P$
% \ENDIF
% \ENDFOR
% \end{algorithmic}
% \end{algorithm}
% \begin{lemma}
% \label{lemma-double-add}
% Algorithm \ref{double-add} is correct, \ie it respects its output conditions given the input conditions.
% \end{lemma}
% We prove Lemma \ref{lemma-double-add}. However
With a simple double-and-add algorithm, with careful timing, an attacker could reconstruct $n$.
In the case of X25519, $n$ is the private key. With the Montgomery's ladder, while
it provides slightly more computations and an extra variable, we can prevent such weakness.
See Algorithm \ref{montgomery-ladder}.
% \begin{algorithm}
% \caption{Montgomery ladder for scalar mult.}
% \label{montgomery-ladder}
% \begin{algorithmic}
% \REQUIRE{Point $P$, scalars $n$ and $m$, $n < 2^m$}
% \ENSURE{$Q = n \cdot P$}
% \STATE $Q \leftarrow \Oinf$
% \STATE $R \leftarrow P$
% \FOR{$k$ := $m$ downto $1$}
% \IF{$k^{\text{th}}$ bit of $n$ is $0$}
% \STATE $R \leftarrow Q + R$
% \STATE $Q \leftarrow 2Q$
% \ELSE
% \STATE $Q \leftarrow Q + R$
% \STATE $R \leftarrow 2R$
% \ENDIF
% \ENDFOR
% \end{algorithmic}
% \end{algorithm}
See \aref{alg:montgomery-ladder}.
\begin{lemma}
\label{lemma-montgomery-ladder}
Algorithm \ref{montgomery-ladder} is correct, \ie it respects its output conditions given the input conditions.
\aref{alg:montgomery-ladder} is correct, \ie it respects its output conditions given the input conditions.
\end{lemma}
In Curve25519 we are only interested in the $x$ coordinate of points, using
Lemmas \ref{lemma-add} and \ref{lemma-double}, and replacing the if statements
with conditional swapping we can define a ladder similar to the one used in TweetNaCl.
See Algorithm \ref{montgomery-double-add}
See \aref{alg:montgomery-double-add}
\begin{algorithm}
\caption{Montgomery ladder for scalar multiplication on $M_{a,b}(\K)$ with optimizations}
\label{montgomery-double-add}
\label{alg:montgomery-double-add}
\begin{algorithmic}
\REQUIRE{$x \in \K\backslash \{0\}$, scalars $n$ and $m$, $n < 2^m$}
\ENSURE{$a/c = \chi_0(n \cdot P)$ for any $P$ such that $\chi_0(P) = x$}
......@@ -375,7 +341,7 @@ See Algorithm \ref{montgomery-double-add}
\begin{lemma}
\label{lemma-montgomery-double-add}
Algorithm \ref{montgomery-double-add} is correct, \ie it respects its output
\aref{alg:montgomery-double-add} is correct, \ie it respects its output
conditions given the input conditions.
\end{lemma}
......@@ -410,7 +376,7 @@ And thus the theorem of the correctness of the Montgomery ladder.
\begin{theorem}
\label{montgomery-ladder-correct}
For all $n, m \in \N$, $x \in \K$, $P \in M_{a,b}(\K)$,
if $\chi_0(P) = x$ then Algorithm \ref{montgomery-double-add} returns $\chi_0(n \cdot P)$
if $\chi_0(P) = x$ then \aref{alg:montgomery-double-add} returns $\chi_0(n \cdot P)$
\end{theorem}
\begin{lstlisting}[language=Coq]
Theorem opt_montgomery_ok (n m: nat) (x : K) :
......@@ -512,7 +478,7 @@ Theorem x_is_on_curve_or_twist: forall x : Zmodp.type,
We use the same definitions as in \cite{Ber06}. We consider the extension field $\F{p^2}$ as the set $\F{p} \times \F{p}$ with $\delta = 2$, in other words,
the polynomial with coefficients in $\F{p}$ modulo $X^2 - 2$. In a similar way as for $\F{p}$ we use Module in Coq.
\begin{lstlisting}[language=Coq]
Module Zmodp.
Module Zmodp2.
Inductive type :=
Zmodp2 (x: Zmodp.type) (y:Zmodp.type).
......@@ -567,7 +533,7 @@ Theorem x_is_on_curve_or_twist_implies_x_in_Fp2:
\end{lstlisting}
We now study the case of the scalar multiplication and show similar proofs.
\begin{definition}
\begin{dfn}
Define the functions $\varphi_c$, $\varphi_t$ and $\psi$\\
-- $\varphi_c: M_{486662,1}(\F{p}) \mapsto M_{486662,1}(\F{p^2})$\\
such that $\varphi((x,y)) = ((x,0), (y,0))$.\\
......@@ -575,7 +541,7 @@ Define the functions $\varphi_c$, $\varphi_t$ and $\psi$\\
such that $\varphi((x,y)) = ((x,0), (0,y))$.\\
-- $\psi: \F{p^2} \mapsto \F{p}$\\
such that $\psi(x,y) = (x)$.
\end{definition}
\end{dfn}
\begin{lemma}
For all $n \in \N$, for all point $P\in\F{p}\times\F{p}$ on the curve $M_{486662,1}(\F{p})$ (respectively on the quadratic twist $M_{486662,2}(\F{p})$), we have:
......@@ -605,3 +571,31 @@ Lemma curve25519_Fp2_ladder_ok (n : nat) (x:Zmodp.type) :
p #x0 = Zmodp2.Zmodp2 x 0 ->
curve25519_Fp_ladder n x = (p *+ n)#x0 /p.
\end{lstlisting}
By converting those array of 32 bytes into their respective little-endian value
we prove the correctness of \TNaCle{crypto_scalarmult} (Theorem \ref{CSM-correct})
in Coq (for the sake of simplicity we do not display the conversion in the theorem).
\begin{theorem}
\label{CSM-correct}
For all $n \in \N, n < 2^{255}$ and where the bits 1, 2, 5 248, 249, 250
are cleared and bit 6 is set, for all $P \in E(\F{p^2})$,
for all $p \in \F{p}$ such that $P.x = p$,
there exists $Q \in E(\F{p^2})$ such that $Q = \cdot P$ where $Q.x = q$ and $q$ = \VSTe{CSM} $n$ $p$.
\end{theorem}
A more complete description in Coq of Theorem \ref{CSM-correct} with the associated conversions
is as follow:
\begin{lstlisting}[language=Coq]
Theorem Crypto_Scalarmult_Correct:
forall (n p:list Z) (P:mc curve25519_Fp2_mcuType),
Zlength n = 32 ->
Zlength p = 32 ->
Forall (fun x => 0 <= x /\ x < 2^8) n ->
Forall (fun x => 0 <= x /\ x < 2^8) p ->
Fp2_x (ZUnpack25519 (ZofList 8 p)) = P#x0 ->
ZofList 8 (Crypto_Scalarmult n p) =
(P *+ (Z.to_nat (Zclamp (ZofList 8 n)))) _x0.
\end{lstlisting}
......@@ -89,14 +89,14 @@ A description of the content of the archive is provided in
Appendix~\ref{appendix:proof-folders}.
\subheading{Organization of this paper.}
Section~\ref{preliminaries} give the necessary background on Curve25519
\sref{sec:preliminaries} give the necessary background on Curve25519
implementation and a rough understanding of how formal verification works.
Section~\ref{C-Coq} provides the specification of X25519 in addition to proofs
techniques used to show the correctness.
Section~\ref{sec3-maths} describes our extension of the formal library by Bartzia
\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
and Strub and the correctness of X25519 implementation with respect to Bernstein
specifications~\cite{Ber14}.
And lastly in Section~\ref{Conclusion} we discuss the trust in this proof.
And lastly in \sref{sec:Conclusion} we discuss the trust in this proof.
% Five years ago:
......
\section{Proving equivalence of X25519 in C and Coq}
\label{C-Coq}
In this section we prove the following theorem:
%\begin{lstlisting}[language=Coq]
%Lemma body_crypto_scalarmult: semax_body Vprog Gprog f_crypto_scalarmult_curve25519_tweet crypto_scalarmult_spec.
%\end{lstlisting}
\label{sec:C-Coq-RFC}
In this section we prove the following theorems:
\begin{theorem}
\label{thm:VST}
The implementation X25519 in TweetNaCl (\TNaCle{crypto_scalarmult}) matches our
functional specification in Coq.
\end{theorem}
We first describe the global structure of our proof.
Then we discuss techniques used to prove the equivalence between the
Clight description of TweetNaCl and Coq functions producing similar behaviors.
\begin{theorem}
\label{thm:RFC}
Our functional specification in Coq matches the specifications of RFC~7748~\cite{rfc7748}.
\end{theorem}
In order to prove the correctness of X25519 in TweetNaCl code, we use VST to prove
that the code matches our functional specification of \TNaCle{crypto_scalarmult}
(abbreviated as \texttt{CSM}) in Coq. Then, we prove that our specification of the scalar
multiplication matches the mathematical definition of elliptic curves and Theorem 2.1 by
Bernstein~\cite{Ber06}. Figure~\ref{tk:ProofOverview} shows a graph of dependencies
of the proofs considered. The mathematical proof of our specification is presented
in Section~\ref{sec3-maths}.
We first describe the global structure of our proof (\ref{subsec:proof-structure}).
Then we introduce our specification (\ref{}), we specify the Hoare triple and prove it
correct with VST (\tref{thm:VST}).
Then we discuss techniques used to prove equivalence of operations between
different number representations (\ref{}), proving the equivalence with the RFC (\tref{thm:RFC}).
\subsection{Structure of our proof}
\label{subsec:proof-structure}
In order to prove the correctness of X25519 in TweetNaCl code \TNaCle{crypto_scalarmult},
we use VST to prove that the code matches our functional Coq specification of \Coqe{Crypto_Scalarmult}
(sometimes abbreviated as \Coqe{CSM}). Then, we prove that our specification of the scalar
multiplication matches the mathematical definition of elliptic curves and Theorem 2.1 by
Bernstein~\cite{Ber06} (\tref{thm:Elliptic-CSM}).
\fref{tikz:ProofOverview} shows a graph of dependencies of the proofs considered.
The mathematical proof of our specification is presented
in \sref{sec:maths}.
\begin{figure}[h]
\centering
\include{tikz/proof}
\caption{Overview of the proof}
\label{tk:ProofOverview}
\label{tikz:ProofOverview}
\end{figure}
Verifying \TNaCle{crypto_scalarmult} also implies to verify all the functions
subsequently called: \TNaCle{unpack25519}; \TNaCle{A}; \TNaCle{Z}; \TNaCle{M};
\TNaCle{S}; \TNaCle{car25519}; \TNaCle{inv25519}; \TNaCle{set25519}; \TNaCle{sel25519};
......@@ -43,7 +49,7 @@ We prove the implementation of X25519 is \textbf{sound}, \ie:
\end{itemize}
We also prove that TweetNaCl's code is \textbf{correct}:
\begin{itemize}
\item X25519 is correctly implemented (we get what we expect).
\item X25519 is correctly implemented (we get what we expect) .
\item Operations on \texttt{gf} (\texttt{A}, \texttt{Z}, \texttt{M}, \texttt{S})
are equivalent to operations ($+,-,\times,x^2$) in \Zfield.
\item The Montgomery ladder computes a scalar multiplication between a natural
......@@ -65,22 +71,35 @@ This low level specification gives us the soundness assurance.
By showing that operations over instances ($\K = \Zfield$, $\Z$, list of $\Z$) are
equivalent, we bridge the gap between the low level and the high level specification
with Curve25519 parameters.
As such, we prove all specifications to equivalent (Fig.\ref{tk:ProofStructure}).
As such, we prove all specifications to equivalent (\fref{tikz:ProofStructure}).
This guarantees us the correctness of the implementation.
\begin{figure}[h]
\centering
\include{tikz/specifications}
\caption{Structural construction of the proof}
\label{tk:ProofStructure}
\label{tikz:ProofStructure}
\end{figure}
\subsection{Correctness Specification}
TweetNaCl implements X25519 with numbers represented as arrays.
RFC~7748 defines X25519 over field elements.
\noindent
-- Definition of \Coqe{Crypto_Scalarmult} CSM\\
-- explain why we have a generic definition, explain instanciation
\subsection{With the Verifiable Software Toolchain}
\label{subsec:with-VST}
\subheading{Specifications}
We show the soundness of TweetNaCl by proving the following specification matches a pure Coq function. % why "pure" ?
This defines the equivalence between the Clight representation and a Coq definition of the ladder.
\begin{CoqVST}
\begin{lstlisting}[language=CoqVST]
Definition crypto_scalarmult_spec :=
DECLARE _crypto_scalarmult_curve25519_tweet
WITH
......@@ -111,7 +130,7 @@ SEP (sh [{ v_q }] <<(uch32)-- mVI (CSM n p);
sh [{ v_n }] <<(uch32)-- mVI n;
sh [{ v_p }] <<(uch32)-- mVI p;
Ews [{ c121665 }] <<(lg16)-- mVI64 c_121665
\end{CoqVST}
\end{lstlisting}
In this specification we state as preconditions:
\begin{itemize}
......@@ -150,36 +169,127 @@ As Post-condition we have:
This specification shows that \TNaCle{crypto_scalarmult} in C computes the same
result as \VSTe{CSM} in Coq provided that inputs are within their respective
bounds.
bounds: arrays of 32 bytes.
\todo{TO MOVE TO THE NEXT SECTION}
By converting those array of 32 bytes into their respective little-endian value
we prove the correctness of \TNaCle{crypto_scalarmult} (Theorem \ref{CSM-correct})
in Coq (for the sake of simplicity we do not display the conversion in the theorem).
\begin{theorem}
\label{CSM-correct}
For all $n \in \N, n < 2^{255}$ and where the bits 1, 2, 5 248, 249, 250
are cleared and bit 6 is set, for all $P \in E(\F{p^2})$,
for all $p \in \F{p}$ such that $P.x = p$,
there exists $Q \in E(\F{p^2})$ such that $Q = \cdot P$ where $Q.x = q$ and $q$ = \VSTe{CSM} $n$ $p$.
\end{theorem}
A more complete description in Coq of Theorem \ref{CSM-correct} with the associated conversions
is as follow:
The Verifiable Software Toolchain uses a strongest postcondition strategy.
The user must first write a formal specification of the function he wants to verify in Coq.
This should be as close as possible to the C implementation behavior.
This will simplify the proof and help with stepping through the CLight version of the software.
With the range of inputs defined, VST mechanically steps through each instruction
and ask the user to verify auxiliary goals such as array bound access, or absence of overflows/underflows.
We call this specification a low level specification. A user will then have an easier
time to prove that his low level specification matches a simpler higher level one.
In order to further speed-up the verification process, it has to be know that to
prove the specification \TNaCle{crypto_scalarmult}, a user only need the specification of e.g. \TNaCle{M}.
This provide with multiple advantages: the verification by the Coq kernel can be done
in parallel and multiple users can work on proving different functions at the same time.
For the sake of completeness we proved all intermediate functions.
\subheading{Memory aliasing} is the next point a user should pay attention. The way VST
deals with the separation logic is similar to a consumer producer problem.
A simple specification of \texttt{M(o,a,b)} will assume three distinct memory share.
When called with three memory share (\texttt{o, a, b}), the three of them will be consumed.
However assuming this naive specification when \texttt{M(o,a,a)} is called (squaring),
the first two memory shares (\texttt{o, a}) are consumed and VST will expect a third
memory share where the last \texttt{a} is pointing at which does not \textit{exist} anymore.
Examples of such cases are summarized in \fref{tikz:MemSame}.
\begin{figure}[h]