Commit 6a8234f6 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

spelling

parent b9049dff
......@@ -6,7 +6,7 @@ chain of trust.
\subsection{Trusted Core Base of the proof}
Our proof relies on a trusted base , i.e. a foundation of specifications
Our proof relies on a trusted base, i.e. a foundation of specifications
and implementations that must stay correct with respect to their specifications.
One should not be able to prove a false statement in that system e.g. by proving
an inconsistency.
......@@ -16,7 +16,7 @@ In our case we rely on:
\item \textbf{Calculus of Inductive Construction}. The intuitionistic logic
used by Coq must be consistent in order to trust the proofs. As an axiom,
we assumed that the functional extensionality, which is also consistent with that logic.
$$\forall x, f(x) = g(x) ) \implies f = g$$
$$\forall x, f(x) = g(x) \implies f = g$$
\begin{lstlisting}[language=Coq]
Lemma f_ext: forall (A B:Type),
forall (f g: A -> B),
......
......@@ -83,7 +83,7 @@ end.
\subsubsection{ZCrypto\_Scalarmult}
\label{subsubsec:ZCryptoScalarmult}
~
Instanciation of the Class \Coqe{Ops} with operations over \Z and modulo \p.
Instantiation of the Class \Coqe{Ops} with operations over \Z and modulo \p.
\begin{lstlisting}[language=Coq]
Definition modP (x:Z) : Z :=
Z.modulo x (Z.pow 2 255 - 19).
......
......@@ -37,7 +37,7 @@ This equation $E(x,y)$ can be reduced into its short Weierstra{\ss} form.
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.
along with an additional formal point $\Oinf$, ``at infinity''. Such a curve does not present any singularity.
\end{dfn}
In this setting, Bartzia and Strub defined the parametric type \texttt{ec} which
......@@ -450,7 +450,7 @@ Given $n$ and $x$, $Curve25519\_Fp(n,x) = \chi_0(n \cdot P)$.
such that $P \in M_{486662,2}(\F{p})$ and $\chi_0(P) = x$.
Given $n$ and $x$, $Twist25519\_Fp(n,x) = \chi_0(n \cdot P)$.
\end{lemma}
As the Montgomery ladder defined above does not depends on $b$, it is trivial to see that the computations done for points of $M_{486662,1}(\F{p})$ and of $M_{486662,2}(\F{p})$ are the same.
As the Montgomery ladder defined above does not depend on $b$, it is trivial to see that the computations done for points of $M_{486662,1}(\F{p})$ and of $M_{486662,2}(\F{p})$ are the same.
\begin{lstlisting}[language=Coq]
Theorem curve_twist_eq: forall n x,
curve25519_Fp_ladder n x = twist25519_Fp_ladder n x.
......
......@@ -3,7 +3,7 @@
The Networking and Cryptography library (NaCl)~\cite{BLS12}
is an easy-to-use, high-security, high-speed cryptography library.
It uses specialized code for different platform, which makes it rather complex and hard to audit.
It uses specialized code for different platforms, which makes it rather complex and hard to audit.
TweetNaCl~\cite{BGJ+15} is a compact re-implementation in C
of the core functionalities of NaCl and is claimed to be
\emph{``the first cryptographic library that allows correct functionality
......@@ -53,31 +53,31 @@ implementation satisfies it.
% One of the earliest example of this first approach is the
% B-method~\cite{Abrial:1996:BAP:236705} in 1986.
Using the synthesis approach, Zinzindohou{\'{e}} et al. wrote an verified extensible
Using the synthesis approach, Zinzindohou{\'{e}} et al. wrote a verified extensible
library of elliptic curves~\cite{Zinzindohoue2016AVE} in F*~\cite{DBLP:journals/corr/BhargavanDFHPRR17}.
This served as ground work for the cryptographic library HACL*~\cite{zinzindohoue2017hacl}
used in the NSS suite from Mozilla.
Coq does not only allows verification but also synthesis~\cite{CpdtJFR}.
Coq not only allows verification but also synthesis~\cite{CpdtJFR}.
Erbsenm; Philipoom; Gross; and Chlipala et al. make use of it to have
correct-by-construction finite field arithmetic~\cite{Philipoom2018CorrectbyconstructionFF}.
In such way, they synthesized~\cite{Erbsen2016SystematicSO} certified elliptic curve
implementations~\cite{Erbsen2017CraftingCE}. These are now being used in
BoringSSL~\cite{fiat-crypto}.
The verification approach, have been used to prove the correctness of OpenSSL
The verification approach has been used to prove the correctness of OpenSSL
HMAC~\cite{Beringer2015VerifiedCA} and SHA-256~\cite{2015-Appel}. Compared to
their work our approaches makes a complete link between the C implementation and
the formal mathematical definition of the group theory behind elliptic curves.
Synthesis approaches forces the user to depend on generated code which may not
be optimal (speed, compactness...), they require to tweak the compiler in order
to achieve the desired properties. On the other hand a carefully handcrafted
be optimal (speed, compactness...) and they require compiler tweaks in order
to achieve the desired properties. On the other hand, carefully handcrafted
optimized code will force the verifier to consider all the possible special cases
and write a complex low level specification in order to prove the correctness of
the algorithm.
It has to be noted that Curve25519 implementations has already been under the scrutiny~\cite{Chen2014VerifyingCS}.
It has to be noted that Curve25519 implementations have already been under scrutiny~\cite{Chen2014VerifyingCS}.
However in this paper we provide a proofs of correctness and soundness of a C program up to
the theory of elliptic curves.
......
......@@ -42,7 +42,7 @@ in \sref{sec:maths}.
\label{tikz:ProofOverview}
\end{figure}
Verifying \TNaCle{crypto_scalarmult} also implies to verify all the functions
Verifying \TNaCle{crypto_scalarmult} also implies verifying all the functions
subsequently called: \TNaCle{unpack25519}; \TNaCle{A}; \TNaCle{Z}; \TNaCle{M};
\TNaCle{S}; \TNaCle{car25519}; \TNaCle{inv25519}; \TNaCle{set25519}; \TNaCle{sel25519};
\TNaCle{pack25519}.
......@@ -95,7 +95,7 @@ This guarantees us the correctness of the implementation.
TweetNaCl implements X25519 with numbers represented as arrays.
RFC~7748 defines X25519 over field elements. In order to simplify our proofs,
we define operations used in the ladder over generic types
\coqe{T} and \coqe{T'}. Those types are later instanciated as natural number,
\coqe{T} and \coqe{T'}. Those types are later instantiated as natural numbers,
integers, field elements, list of integers...
The generic definition of the ladder (\coqe{montgomery_rec}) and its match with
the definition of RFC~7748 are provided in Appendix~\ref{subsubsec:coq-ladder}.
......@@ -103,15 +103,15 @@ It has to be noted that the RFC uses an additional variable to optimize the numb
of \texttt{CSWAP}:
\emph{``Note that these formulas are slightly different from Montgomery's
original paper. Implementations are free to use any correct formulas.''}~\cite{rfc7748}.
We later prove our lader correct in that respect (\sref{sec:maths}).
We later prove our ladder correct in that respect (\sref{sec:maths}).
\coqe{montgomery_rec} only computes the ladder steps.
While the inversion; the packing; the unpacking (setting bit 255 to \texttt{0})
and clamping are not defined in a generic manner, we show their equivalence
While the inversion, the packing, the unpacking (setting bit 255 to \texttt{0})
and the clamping are not defined in a generic manner, we show their equivalence
between the different representations.
Appendix~\ref{subsubsec:ZCryptoScalarmult} show the instantiation of our ladder
over Intergers (type \coqe{Z}). We call it \coqe{ZCrypto_Scalarmult}.
Appendix~\ref{subsubsec:ZCryptoScalarmult} shows the instantiation of our ladder
over Integers (type \coqe{Z}). We call it \coqe{ZCrypto_Scalarmult}.
The modulo reduction is applied in \coqe{ZPack25519} translating every
underlying operations as over \Zfield. As a result this specification can be
interpreted as the formalization of X25519 in RFC~7748.
......@@ -126,7 +126,7 @@ The location of the definitions are listed in Appendix~\ref{appendix:proof-files
\label{subsec:with-VST}
We now turn our focus to the specification of the Hoare triple with our
specifications of \TNaCle{crypto_scalarmult} over list of integers and proving
specifications of \TNaCle{crypto_scalarmult} over lists of integers and proving
its correctness.
\subheading{Specifications.}
......@@ -232,7 +232,7 @@ The location of the proof of this Hoare triple can be found in Appendix~\ref{app
\subheading{Memory aliasing.}
In the VST, 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}),
distinct memory share. When called with three memory shares (\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 (\texttt{a}) which does not \textit{exist} anymore.
......@@ -265,10 +265,10 @@ However we must define invariants which are true for each iteration step.
Assume we want to prove a decreasing loop where indexes go from 3 to 0.
Define a function $g : \N \rightarrow State \rightarrow State $ which takes as
input an integer for the index and a state, then return a state.
It simulate the body of the \texttt{for} loop.
input an integer for the index and a state, then returns a state.
It simulates the body of the \texttt{for} loop.
Assume its recursive call: $f : \N \rightarrow State \rightarrow State $ which
iteratively apply $g$ with decreasing index:
iteratively applies $g$ with decreasing index:
\begin{equation*}
f ( i , s ) =
\begin{cases}
......@@ -301,7 +301,7 @@ in C provide the same computations as in \coqe{CSM}.
As described in \sref{subsec:Number-TweetNaCl}, numbers in \TNaCle{gf} are represented
in base $2^{16}$ and we use a direct mapping to represent that array as a list
integers in Coq. However in order to show the correctness of the basic operations,
we need to convert this number as a full integer.
we need to convert this number to a full integer.
\begin{dfn}
Let \Coqe{ZofList} : $\Z \rightarrow \texttt{list} \Z \rightarrow \Z$,
a parameterized map by $n$ between a list $l$ and its little endian representation
......@@ -444,9 +444,9 @@ Lemma Inv25519_Z_GF : forall (g:list Z),
(Inv25519_Z (Z16.lst g)) :GF.
\end{lstlisting}
In TweetNaCl, \TNaCle{inv25519} computes an inverse in $\Zfield$.
It uses the Fermat's little theorem by doing an exponentiation to $2^{255}-21$.
It uses Fermat's little theorem by doing an exponentiation to $2^{255}-21$.
This is done by applying a square-and-multiply algorithm. The binary representation
of $p-2$ implies to always do multiplications aside for bits 2 and 4.
of $p-2$ implies to always do multiplications except for bits 2 and 4.
To prove the correctness of the result we can use multiple strategies such as:
\begin{itemize}
\item Proving it is a special case of square-and-multiply algorithm applied to $2^{255}-21$.
......@@ -511,7 +511,7 @@ Definition f_inv_denote (t : formula_inv) : Prop :=
All denote functions also take as an argument the environment containing the variables.
We do not show it here for the sake of readability,
given that an environment, \Coqe{term_denote} returns the appropriate variable.
With such Domain Specific Language we have the following equality:
With this Domain Specific Language we have the following equality:
\begin{lstlisting}[backgroundcolor=\color{white}]
f_inv_denote
(Eq_inv (M_inv R_inv (S_inv R_inv))
......@@ -614,7 +614,7 @@ Corollary Inv25519_Zpow_GF :
\subheading{Another applications of reflections: packing}
This reflection technique can also be used where proofs requires some computing
over a small and finite domain of variable to test e.g. for all $i$ such that $0 \le i < 16$.
over a small and finite domain of variables to test e.g. for all $i$ such that $0 \le i < 16$.
Using reflection we prove that we can split the for loop in \TNaCle{pack25519} into two parts.
\begin{lstlisting}[language=Ctweetnacl]
for(i=1;i<15;i++) {
......@@ -622,7 +622,7 @@ for(i=1;i<15;i++) {
m[i-1]&=0xffff;
}
\end{lstlisting}
The first loop is computing the subtraction while the second is applying the carrying.
The first loop is computing the subtraction while the second is applying the carries.
\begin{lstlisting}[language=Ctweetnacl]
for(i=1;i<15;i++) {
m[i]=t[i]-0xffff
......
......@@ -258,7 +258,7 @@ In order to compute the scalar multiplication,
X25519 uses the Montgomery ladder~\cite{Mon85}.
$x$-coordinates are represented as fractions, the computation of the actual
value is differed to the end of the ladder with \TNaCle{inv25519}.
value is deffered to the end of the ladder with \TNaCle{inv25519}.
First extract and clamp the value of $n$. Then unpack the value of $p$.
As per RFC~7748~\cite{rfc7748}, set its most significant bit to 0.
......@@ -355,6 +355,6 @@ The first step consists of translating the source code into CLight,
an intermediate representation used by CompCert.
For such purpose we use the parser CompCert: \texttt{clightgen}.
In second step we define the Hoare triple encapsulating the specification of the
piece of software we want to prove. Then using VST, we uses a strongest
piece of software we want to prove. Then using VST, we use a strongest
postcondition approach to prove the correctness of the triple.
This approach can be seen as a forward symbolic execution of the program.
......@@ -33,7 +33,7 @@ In this folder the reader will find multiple levels of implementation of X25519.
twists, quadratic extensions and ladder.
It also proves the correctness of the ladder over $\F{\p}$.
\item \textbf{\texttt{Gen/}} defines a generic Montgomery ladder which can be
instanciated with different operations. This ladder is the stub for the
instantiated with different operations. This ladder is the stub for the
following implementations.
\item \textbf{\texttt{Mid/}} provides a list-based implementation of the
basic operations \TNaCle{A}, \TNaCle{Z}, \TNaCle{M} \ldots and the ladder. It
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment