Commit 569f019b authored by Peter Schwabe's avatar Peter Schwabe
Browse files

Added lots of TODOs (and a few answers to reviewer comments)

parent d23fddd5
......@@ -91,6 +91,9 @@ above will soon be integrated in a new version of the library.
% As a result we do not believe the metric person-month to be
% a good representation of the verification effort.
\subheading{Lessons learned.}
\todo{Write something about VST etc.}
\subheading{Extending our work.}
The high-level definition (\sref{sec:maths}) can easily be ported to any
other Montgomery curves and with it the proof of the ladder's correctness
......
......@@ -192,18 +192,33 @@ Here are a few linear comments:
\item \textbf{page 6, column 2:}\\
"and the same code as a pure Coq function" $\rightarrow$ I would rephrase, the term "same code" is misleading.
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}
\todo{Answer}
\end{answer}
\begin{itemize}
\item \textbf{page 7:}\\
Discussion on memory aliasing is great, I would have liked more of this kind through the paper.\\
Figure 2: I had to fish back a little for the definition of "sh", but "Ews" has really never been defined I believe.\\
"Improving speed" $\rightarrow$ of what? This whole paragraph is quite hard to read. In particular be careful that it is not obvious to the reader whether you are speeding up the verification process or the runtime of the implementation. In particular it was unclear to me what you were referring to by saying "Optimizations of such definitions".\\
The following paragraph also is a bit cryptic. I assume you are saying that identifying finely the dependencies between definitions allow for parallelizing the work? Arguably, simply admitting temporarily yon the fly any specification needed achieves the same.\\
"Numbers in gf" $\rightarrow$ Please remind the reader what "gf" is. Good section overall
\end{itemize}
\begin{answer}
\todo{Answer}
\end{answer}
\begin{itemize}
\item \textbf{page 8:}\\
"Using reflection (...)" $\rightarrow$ Would deserve more explanations.\\
Figure 3: Please comment generously this figure, it looks great but it is frustrating to try to decipher it without help.
\end{itemize}
\begin{answer}
\todo{Answer}
\end{answer}
\begin{itemize}
\item \textbf{page 9:}\\
"the type of field which characteristic" $\rightarrow$ "whose characteristic"\\
"The value of add is proven to be on the curve (with coercion)" $\rightarrow$ This parenthesis is too cryptic, it should probably be dropped.
......@@ -237,10 +252,29 @@ Here are a few linear comments:
\end{center}
\begin{itemize}
\item Please provide high level explanations to your three Figures describing the infrastructure.
\end{itemize}
\begin{answer}
\todo{We added such high-level descriptions.}
\end{answer}
\begin{itemize}
\item Please reduce slightly the width of the technical material covered, and use the gained space to provide a bit more context to the one covered
\end{itemize}
\begin{answer}
We removed various technical details, in particular in Section 5. We used the space to extend the discussion
of various other points raised by the reviewers.
\end{answer}
\begin{itemize}
\item Please provide more get away lessons from this development that would benefit new similar works
\end{itemize}
\begin{answer}
We added a ``lessons learned'' paragraph in the conclusion.
\end{answer}
\begin{itemize}
\item Please give a sense of the difficulties encountered during the formalization.
\end{itemize}
\begin{answer}
Many difficulties were of technical nature; we cover some of this now in the ``lessons learned'' paragraph.
\end{answer}
\begin{center}
\subheading{===== Questions for authors' response =====}
......
......@@ -65,8 +65,15 @@ Section 4 shows that the TweetNaCl C code meets the Coq spec of RFC 7748. While
Even though you don't find any bugs in the C code it would be useful for the reader if you could describe the kinds of bugs you would have found. For example, there is a history of carry propagation bugs in X25519 code (both in C and in assembly). You could illustrate one of these bugs and show how the VST/Coq proof would be able to find it.
On page 23, you say "Constant-timeness is not a property verifiable with VST. This is not verifiable with our framework." Please say this prominently in Section 1. When readers sees your montgomery ladder, and sees the constant-time CSWAP function, they may well assume that you are verifying constant-timeness for the implementation. Stating that this is not the case early will help avoid misunderstanding. I recommend that you also cite other (complementary) tools that could be used just to verify constant-timeness for the code. It may be even better if you were to demonstrate the use of some such tool on the TweetNaCl code.
\begin{answer}
We added a paragraph on verification of implementation security, in particular ``constant-timeness'' to the introduction.
\end{answer}
I enjoyed Section 5 and I believe it is one of the more important (and reusable) parts of this work. However, the way it is presented reads like a long list of Lemmas and Theorems with hardly any explanation or motivation in between. By the end of this section, the reader has read 20 lemmas and definitions in a mixture of mathematical and Coq syntax. I recommend that the authors pick and choose 5 key lemmas and explain them, leaving the rest to an appendix. The high-level structure of the proof and some examples of "interesting" or "tricky" cases is the best they can hope to communicate in the body of the paper.
\begin{answer}
We reduced the amount of technical details in Section 5.
\end{answer}
\begin{center}
\subheading{===== Requested changes =====}
......
......@@ -45,8 +45,20 @@ This paper presents a formal specification and verification of X25519 in TweetNa
\begin{itemize}
\item Are the properties the only ones? How do we know that more important ones weren’t missed?
\end{itemize}
\begin{answer}
We verify correctness of the software. There are indeed other important properties, in particular
implementation security. We now discuss this in the introduction.
\end{answer}
\begin{itemize}
\item Only verified at the C level (maybe the CompCert chain proves some of the assembly?)
\end{itemize}
\begin{answer}
CompCert guarantees correct translation (via a formal verification in Coq),
but if the code is translated with, for example, gcc, we agree that the compiler becomes part of the TCB.
\end{answer}
\begin{center}
......
......@@ -60,4 +60,4 @@ Security audience (e.g., walking step-by-step through proofs, with no text
explaining why this is important or interesting). I also find bits of the text
somewhat rushed (e.g., paragraph from RFC with no context).
\todo{Should add some reply here somewhere}
......@@ -54,3 +54,6 @@ If the paper was proposing a new technique which could be applied more generally
\item Describe challenges for proving statements about the more complex (faster) implementations.
\item Describe which parts of the contributions could possibly be applied more generally.
\end{itemize}
\todo{Should add some reply here somewhere}
......@@ -91,7 +91,7 @@ the RFC uses an additional variable to decide whether a conditional swap
is required or not.
Later in our proof we use a simpler description of the ladder
(\coqe{montgomery_rec}) which follows strictly the \aref{alg:montgomery-ladder}
(\coqe{montgomery_rec}) which follows strictly \aref{alg:montgomery-ladder}
and prove those ladder equivalent.
\emph{``To implement the X25519(k, u) [...] functions (where k is
......
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