Commit 7067f229 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

finish paper: one todo left = conclusion

parent bb8cee63
......@@ -26,12 +26,11 @@ Lemma f_ext: forall (A B:Type),
\item \textbf{Verifiable Software Toolchain}. This framework developed at
Princeton allows a user to prove that a \texttt{CLight} code matches pure Coq
specification. However one must trust the framework properly captures and
map the CLight behavior to the basic pure Coq functions. At the beginning of
the project we found inconsistency and reported them to the authors.
map the CLight behavior to the basic pure Coq functions.
% At the beginning of the project we found inconsistency and reported them to the authors.
\item \textbf{CompCert}. The formally proven compiler. We trust that the Clight
model captures correctly the C standard.
\todo{VERIFY THIS, WHICH STANDARD ?}.
model captures correctly the C99 standard.
Our proof also assumes that the TweetNaCl code will behave as expected if
compiled under CompCert. We do not provide guarantees for other C compilers
such as Clang or GCC.
......@@ -47,10 +46,8 @@ o[i] = aux1 + aux2;
\end{lstlisting}
The trust of the proof relied on the trust of a correct translation from the
initial version of \textit{TweetNaCl} to \textit{TweetNaclVerificable}.
While this problem is still present, the CompCert developers provided us with
the \texttt{-normalize} option for \texttt{clightgen} which takes care of
generating auxiliary variables in order to automatically derive these steps.
\texttt{clightgen} now comes with \texttt{-normalize} flag which
factors out function calls and assignments from inside subexpressions.
The changes required for a C-code to make it Verifiable are now minimal.
\item Last but not the least, we must trust: the \textbf{Coq kernel} and its
......@@ -59,10 +56,26 @@ o[i] = aux1 + aux2;
done with this architecture \cite{2015-Appel,coq-faq}.
\end{itemize}
\subsection{Modifications in TweetNaCl}
\subsection{Corrections in TweetNaCl}
As a result of this verification, we removed superflous code.
Indeed 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.
Peter Wu and Jason A. Donenfeld brought to our attention that the original
\TNaCle{car25519} function presented risk of Undefined Behavior if \texttt{c}
is a negative number.
\begin{lstlisting}[language=Ctweetnacl]
c=o[i]>>16;
o[i]-=c<<16; // c < 0 = UB !
\end{lstlisting}
By replacing statement by a logical \texttt{and} (and proving the correctness)
we solved this problem.
\begin{lstlisting}[language=Ctweetnacl]
o[i]&=0xffff;
\end{lstlisting}
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.
We believe that the type change of the loop index (\TNaCle{int} instead of \TNaCle{i64})
does not impact the trust of our proof.
\todo{Mention Peter Wu and Jason A. Donenfeld change to car25519}
\todo{I don't see what to say more here.}
This diff is collapsed.
......@@ -296,6 +296,9 @@ We formalized this result in a generic way in Appendix~\ref{subsubsec:for}.
Using this formalization, we prove that the 255 steps of the Montgomery ladder
in C provide the same computations as in \coqe{CSM}.
\subsection{Number Representation and C Implementation}
As described in \sref{subsec:Number-TweetNaCl}, numbers in \TNaCle{gf} are represented
......@@ -323,7 +326,6 @@ 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{sec:maths}, we formally define \F{\p}.
Equivalence between operations under \coqe{:GF} and in \F{\p} are easily proven.
......@@ -363,6 +365,9 @@ Lemma M_bound_Zlength :
Forall (fun x => -38 <= x < 2^16 + 38) (Low.M a b).
\end{lstlisting}
\subsection{Inversions, Reflections and Packing}
We now turn our attention to the inversion in \Zfield and techniques to
......@@ -403,7 +408,6 @@ Function pow_fn_rev (a:Z) (b:Z)
let prev := pow_fn_rev (a - 1) b c g in
step_pow (b - a) prev g.
\end{lstlisting}
This \Coqe{Function} requires a proof of termination. It is done by proving the
well-foundedness of the decreasing argument: \Coqe{measure Z.to_nat a}. Calling
\Coqe{pow_fn_rev} 254 times allows us to reproduce the same behavior as the \texttt{Clight} definition.
......@@ -443,6 +447,7 @@ Lemma Inv25519_Z_GF : forall (g:list Z),
(Z16.lst (Inv25519 g)) :GF =
(Inv25519_Z (Z16.lst g)) :GF.
\end{lstlisting}
In TweetNaCl, \TNaCle{inv25519} computes an inverse in $\Zfield$.
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
......@@ -570,6 +575,7 @@ Definition decide_f_inv (f:formula_inv) : bool :=
| Eq_inv x y => decide_e_inv x y
end.
\end{lstlisting}
We prove our decision procedure correct.
\begin{lemma}
\label{lemma:decide}
......@@ -583,6 +589,7 @@ Lemma decide_formula_inv_impl :
decide_f_inv f = true ->
f_inv_denote f.
\end{lstlisting}
By reification to over DSL (\lref{lemma:reify}) and by applying our decision
(\lref{lemma:decide}), we prove the following corollary.
\begin{lemma}
......@@ -633,6 +640,7 @@ for(i=1;i<15;i++) {
m[i-1]&=0xffff;
}
\end{lstlisting}
This loop separation allows simpler proofs. The first loop is seen as the subtraction of a number in \Zfield.
We then prove that with the iteration of the second loop, the number represented in $\Zfield$ stays the same.
This leads to the proof that \TNaCle{pack25519} is effectively reducing modulo $\p$ and returning a number in base $2^8$.
......
......@@ -4,7 +4,7 @@
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{dfn}[theorem]{Definition}
\newtheorem{hypothesis}{Hypothesis}
\newtheorem{hypothesis}[theorem]{Hypothesis}
\newcommand\invisiblesection[1]{%
\refstepcounter{section}
......
......@@ -244,7 +244,6 @@ sv pack25519(u8 *o,const gf n)
}
}
\end{lstlisting}
As we can see, this function is considerably more complex than the
unpacking function. The reason is that it needs to convert
to a \emph{unique} representation before packing into the output
......
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