Commit fdfe7791 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

incorporating Freek's comments

parent 8b9f4c04
......@@ -17,15 +17,16 @@ the \xcoord $x_P \in \F{p}$ of a point in $E(\F{p^2})$,
using the standard mapping of integers modulo $p$ to elements in $\F{p}$.
The X25519 function first computes a scalar $n'$ from $n$ by setting
bits at position 0, 1, 2 and 255 to \texttt{0}; and to \texttt{1} bit at
position 254.
bits at position 0, 1, 2 and 255 to \texttt{0}; and at position 254
to \texttt{1}.
This operation is often called ``clamping'' of the scalar $n$.
Note that $n' \in 2^{254} + 8\{0,1,\ldots,2^{251}-1\}$.
X25519 then computes the \xcoord of $n'\cdot P$.
RFC~7748~\cite{rfc7748} standardized the X25519 Diffie–Hellman key-exchange algorithm.
RFC~7748~\cite{rfc7748} standardize the X25519 Diffie–Hellman key-exchange algorithm.
Given the base point $B$ where $X_B=9$, each party generates a secret random number
$s_a$ (respectively $s_b$), and computes $X_{P_a}$ (respectively $X_{P_b}$), the
\xcoord of $P_A = s_a \cdot B$ (respectively $P_B = s_b \cdot B$).
The parties exchange $X_{P_a}$ and $X_{P_b}$ and compute their shared secret with
The parties exchange $X_{P_a}$ and $X_{P_b}$ and compute their shared secret
$s_a \cdot s_b \cdot B$ with
X25519 on $s_a$ and $X_{P_b}$ (respectively $s_b$ and $X_{P_a}$).
......@@ -15,7 +15,7 @@ TweetNaCl functions take pointers as arguments. By convention the first one
points to the output array \texttt{o}. It is then followed by the input arguments.
Due to some limitations of the VST, indexes used in \TNaCle{for} loops have to be
of type \TNaCle{int} instead of \TNaCle{i64}. We change the code to allow our
of type \TNaCle{int} instead of \TNaCle{i64}. We changed the code to allow our
proofs to carry through. We believe this does not affect the correctness of the
original code. A complete diff of our modifications to TweetNaCl can be found in
Appendix~\ref{verified-C-and-diff}.
......@@ -67,7 +67,7 @@ This function is considerably more complex as it needs to convert
to a \emph{unique} representation, i.e., also fully reduce modulo
$p$ and remove the redundancy of the radix-$2^{16}$ representation.
The C definition of those functions are available in
The C definitions of those functions are available in
Appendix \ref{verified-C-and-diff}.
\subheading{The Montgomery ladder.}
......@@ -126,4 +126,4 @@ int crypto_scalarmult(u8 *q,
}
\end{lstlisting}
Also note that lines 10 \& 11 represent the ``clamping'' operation.
Note that lines 10 \& 11 represent the ``clamping'' operation.
......@@ -33,7 +33,7 @@ memory shared such as being disjoint.
We discuss this limitation further in \sref{subsec:with-VST}.
The Verified Software Toolchain (VST)~\cite{cao2018vst-floyd} is a framework
which uses Separation logic proven correct with respect to CompCert semantics
which uses separation logic (proven correct with respect to CompCert semantics)
to prove the functional correctness of C programs.
The first step consists of translating the source code into Clight,
an intermediate representation used by CompCert.
......@@ -41,4 +41,4 @@ For such purpose one uses the parser of CompCert called \texttt{clightgen}.
In a second step one defines the Hoare triple representing the specification of
the piece of software one wants to prove. Then using the VST, one uses a strongest
postcondition approach to prove the correctness of the triple.
This approach can be seen as a forward symbolic execution of the program.
This can be seen as a forward symbolic execution of the program.
......@@ -4,7 +4,7 @@
In this section we present our formalization of RFC~7748~\cite{rfc7748}.
\begin{informaltheorem}
The specification of X25519 in RFC~7748 is formalized by \Coqe{RFC} in Coq.
The specification of X25519 in RFC~7748 is formalized by the function \Coqe{RFC} in Coq.
\end{informaltheorem}
More specifically, we formalized X25519 with the following definition:
......@@ -84,14 +84,15 @@ match m with
end.
\end{lstlisting}
Our formalization matches perfectly the RFC. In order to optimize the
The comments in the ladder represent the text from the RFC which
our formalization matches perfectly. In order to optimize the
number of calls to \texttt{CSWAP} (defined in \sref{cswap})
the RFC uses an additional variable to decide whether a conditional swap
is required or not, this differ from \aref{alg:montgomery-ladder}.
is required or not.
Later in our proof we use a simpler description of the ladder
(\coqe{montgomery_rec}) which follows strictly the shape of
the exponent and prove those ladder equivalent.
(\coqe{montgomery_rec}) which follows strictly the \aref{alg:montgomery-ladder}
and prove those ladder equivalent.
\emph{``To implement the X25519(k, u) [...] functions (where k is
the scalar and u is the u-coordinate), first decode k and u and then
......
......@@ -84,10 +84,10 @@ As postcondition we have conditions like:
We show that the computation for \VSTe{RFC} fits in \TNaCle{u8[32]}.
\end{itemize}
computes the same result as \VSTe{RFC} in Coq provided that inputs are within
their respective bounds: arrays of 32 bytes.
\TNaCle{crypto_scalarmult} computes the same result as \VSTe{RFC}
in Coq provided that inputs are within their respective bounds: arrays of 32 bytes.
The correctness of this specification is formally proven in Coq with
The correctness of this specification is formally proven in Coq as
\coqe{Theorem body_crypto_scalarmult}.
% \begin{sloppypar}
......@@ -141,18 +141,19 @@ we define an additional parameter $k$ with values in $\{0,1,2,3\}$:
\item else there is no aliasing.
\end{itemize}
In the proof of our specification, we do a case analysis over $k$ when needed.
This solution does not generate all the possible cases of aliasing over 3 pointers
(\eg \texttt{o} = \texttt{a} = \texttt{b}) but it is enough to cover our needs.
This solution does not cover all the possible cases of aliasing over 3 pointers
(\eg \texttt{o} = \texttt{a} = \texttt{b}) but it is enough to satisfy our needs.
\subheading{Improving speed.}
To make the verification the smoothest, the Coq formal definition of the function
should be as close as possible to the C implementation behavior.
should be as close as possible to the C implementation.
Optimizations of such definitions are often counter-productive as they increase the
amount of proofs required for \eg bounds checking, loops invariants.
amount of proofs required for \eg bounds checking, loop invariants.
In order to further speed-up the verification process, to prove the specification
\TNaCle{crypto_scalarmult}, we only need the specification of the subsequently
called functions (\eg \TNaCle{M}).
This provide with multiple advantages: the verification by the Coq kernel can be
This provide with multiple advantages: the verification by Coq 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.
the same time.
% We proved all intermediate functions.
......@@ -4,7 +4,7 @@
As described in \sref{subsec:Number-TweetNaCl}, numbers in \TNaCle{gf} are represented
in $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 to a full integer.
we need to convert this number to an integer.
We reuse the mapping
$\text{\coqe{ZofList}} : \Z \rightarrow \texttt{list}~\Z \rightarrow \Z$ from \sref{sec:Coq-RFC}
and define a notation where $n$ is $16$, placing us with a radix of $2^{16}$.
......@@ -15,7 +15,7 @@ To facilitate working in $\Zfield$, we define the \coqe{:GF} notation.
\begin{lstlisting}[language=Coq]
Notation "A :GF" := (A mod (2^255-19)).
\end{lstlisting}
Later in \sref{subsec:Zmodp}, we formally define $\Ffield$.
Later in \sref{subsec:Zmodp}, we formally define $\Ffield$ as a field.
Equivalence between operations in $\Zfield$ (\ie under \coqe{:GF}) and in $\Ffield$ are easily proven.
Using these two definitions, we prove intermediate lemmas such as the correctness of the
......
Then using ``Reflections'' techniques (chapter 15 in \cite{CpdtJFR}), we prove
the functional correctness of the inversion over \Zfield.
Using ``Reflections'' techniques (chapter 15 in \cite{CpdtJFR}), we prove
the functional correctness of the multiplicative inverse over \Zfield.
\begin{lemma}
\label{cor:inv_comput_field}
\Coqe{Inv25519} computes an inverse in \Zfield.
......@@ -16,7 +16,7 @@ Corollary Inv25519_Zpow_GF : forall (g:list Z),
By using each function \coqe{Low.M}; \coqe{Low.A}; \coqe{Low.Sq}; \coqe{Low.Zub};
\coqe{Unpack25519}; \coqe{clamp}; \coqe{Pack25519}; \coqe{Inv25519}; \coqe{car25519};
\coqe{montgomery_rec}, we defined in Coq \coqe{Crypto_Scalarmult} and with VST
proved it mimics the exact behavior of X25519 in TweetNaCl.
proved it matches the exact behavior of X25519 in TweetNaCl.
\end{sloppypar}
\begin{sloppypar}
......
Markdown is supported
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