Commit 4a863b49 authored by Peter Schwabe's avatar Peter Schwabe
Browse files

Done with review A and related changes to the paper.

parent c8a38ca3
......@@ -27,13 +27,14 @@ Lemma f_ext: forall (A B:Type),
\item \textbf{CompCert}. When compiling with CompCert we only need to trust
CompCert's {assembly} semantics, as the compilation chain has been formally proven correct.
However, when compiling with other C compilers like Clang or GCC, we need to
trust that the CompCert's Clight semantics matches the C17 standard.
However, when compiling with other C compilers like Clang or GCC, the
whole code base of these compilers becomes part of the TCB.
\item \textbf{\texttt{clightgen}}. The tool making the translation from {C} to
\item \textbf{\texttt{clightgen}}. The tool translating from {C} to
{Clight}, the first step of the CompCert compilation.
VST does not support the direct verification of \texttt{o[i] = a[i] + b[i]}.
This needs to be rewritten into:
This compilation step is not covered by the proofs of CompCert
and VST requires Clight input. For example, VST does not support the direct verification of
\texttt{o[i] = a[i] + b[i]}, which \texttt{clightgen} translates to
\begin{lstlisting}[language=Ctweetnacl,stepnumber=0,belowskip=-0.5 \baselineskip]
aux1 = a[i]; aux2 = b[i];
o[i] = aux1 + aux2;
......@@ -56,7 +57,7 @@ Indeed indexes 17 to 79 of the \TNaCle{i64 x[80]} intermediate variable of
\TNaCle{crypto_scalarmult} were adding unnecessary complexity to the code,
we removed them.
Peter Wu and Jason A. Donenfeld brought to our attention that the original
Wu and Donenfeld brought to our attention that the original
\TNaCle{car25519} function carried a risk of undefined behavior if \texttt{c}
is a negative number.
\begin{lstlisting}[language=Ctweetnacl,stepnumber=0]
......@@ -121,7 +122,9 @@ as $p=2^{255}-19$ is hard-coded in order to speed up some proofs.
With respect to the C code verification (\sref{sec:C-Coq}), the extension of
the verification effort to Ed25519 would make directly use of the low-level
arithmetic. The ladder steps formula being different this would require a high
level verification similar to \tref{thm:montgomery-ladder-correct}.
level verification similar to \tref{thm:montgomery-ladder-correct};
also, a full correctness verification of Ed25519 signatures would require
verifying correctness of SHA-512.
The verification of \eg X448~\cite{cryptoeprint:2015:625,rfc7748} in C would
require the adaptation of most of the low-level arithmetic (mainly the
......
......@@ -94,7 +94,7 @@ Such a paper is difficult to write. The authors have visibly devoted great effor
\item Skimming through the development convinces me that this is a consequent work. But the paper does not help evaluating this effort. It is always difficult to find relevant metrics to evaluate such things, but it would be great to get a sense of the aspects of the work that turned out difficult, and the extent of these difficulties.
\end{itemize}
\begin{answer}
\todo{We should say something regarding these two points.}
We extended the discussion in the conclusion and in particular added a paragraph on lessons learned.
\end{answer}
......@@ -205,8 +205,7 @@ Here are a few linear comments:
Specification: I think explaining the structure of a VST statement would be necessary to help an unfamiliar reader understand this specification.
\end{itemize}
\begin{answer}
We rephrased this paragraph to avoid misleading the reader on the translations done.\\
\todo{add some more text before "In this specification we state preconditions like:" ?}
We rephrased this paragraph and in particular do no not say ``same code'' anymore.
\end{answer}
\begin{itemize}
......@@ -220,9 +219,10 @@ Here are a few linear comments:
\begin{answer}
\begin{itemize}
\item[$-$] We added a description of "Ews" in the precondition paragraph, this should clarify the global memory share name.
\item[$-$] We clarified that we improve the speed of the verification effort. ``Optimization of such definition'' refers to the will of some developers to use for example a fancy recursive definition of a function.
\item[$-$] In order to verify a file, Coq need the compiled proof of dependencies. However in the case of VST it is possible to split the specification from the proof, as a result the proof of the full scalar multiplication does not require the proof of the the multiplication in \F{p}, only its specification.
\item[$-$] We reminded the reader that "gf" is a C type.
\item[$-$] We clarified that we improve the speed of the verification effort; we also clarified what we mean by ``optimizing the
definitions''.
\item[$-$] In order to verify a file, Coq needs the compiled proof of dependencies. However in the case of VST it is possible to split the specification from the proof. As a result the proof of the full scalar multiplication does not require the proof of the the multiplication in \F{p}, only its specification.
\item[$-$] We reminded the reader that "gf" is a type defined through a C \texttt{typedef} in TweetNaCl.
\end{itemize}
\end{answer}
......@@ -265,7 +265,16 @@ Here are a few linear comments:
\end{itemize}
\begin{answer}
\todo{Freek : which version of ISO.}
\begin{itemize}
\item[$-$] Sentence about other compilers (like GCC or Clang) is rephrased.
\item[$-$] Added some context to explain the relation between \texttt{clightgen} and VST.
\item[$-$] ``Other NaCl implementations'': It is not exactly clear to us what the reviewer means.
There are other cryptographic primitives in TweetNaCl and of course also in NaCl.
Large parts of our proof would be re-usable for a proof of Ed25519 signatures in
TweetNaCl (which we mention). Correctness proofs of other cryptographic primitives like
Salsa20 or SHA-512 would not be able to re-use much from our proof; verification
of optimized (assembly) implementations in NaCl would need a different approach.
\end{itemize}
\end{answer}
\begin{center}
......
......@@ -184,8 +184,9 @@ This solution does not cover all the possible cases of aliasing over 3 pointers
\subheading{Improving verification speed.}
To make the verification the smoothest, the Coq formal definition of the function
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, loop invariants.
Attempting to write definitions more ``elegantly'', for example through the extensive
use of recursion, is often counter-productive because such definitions increase the
amount of proofs required for, \eg bounds checking or 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
......
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