Commit d23fddd5 authored by Peter Schwabe's avatar Peter Schwabe
Browse files

Addressed various reviewer comments

parent 61fd712d
......@@ -38,9 +38,9 @@ and to the USENIX Security Symposium (submission deadline February 15, 2020).
The paper received a ``reject'' decision from IEEE S\&P and a ``reject-and-resubmit''
decision from USENIX. In this supplementary material we provide the following documents:
\begin{itemize}
\item The reviews we received at USENIX, together the answers we provided
in the rebuttal phase. Note that we received only reviews \#324A, \#324B, and \#324C
before the rebuttal phase.
\item The reviews we received at USENIX, together with answers to specific comments.
Some of these answers are what we already provided in the USENIX rebuttal;
before this rebuttal we had only received reviews \#324A, \#324B, and \#324C.
\item The version of the manuscript we submitted to USENIX. This version
contains in Appendix D the reviews we received at IEEE S\&P and our replies
to those reviews explaining how we addressed them in the revised version
......
\section*{Usenix Security 2020 Review \#324A}
\begin{tabular}{rrp{.6\textwidth}}
\toprule
Review recommendation & 3.& Major revision \\
Writing quality & 3.& Adequate \\
Reviewer interest & 2.& I might go to a talk about this \\
Reviewer expertise & 3.& Knowledgeable \\
\bottomrule
\toprule
Review recommendation & 3.& Major revision \\
Writing quality & 3.& Adequate \\
Reviewer interest & 2.& I might go to a talk about this \\
Reviewer expertise & 3.& Knowledgeable \\
\bottomrule
\end{tabular}
\begin{center}
\subheading{===== Paper summary =====}
\subheading{===== Paper summary =====}
\end{center}
The Networking and Cryptography library (NaCl) admits a compact implementation,
......@@ -47,47 +47,59 @@ traditional Coq proof.
The complete formal development is provided as an artifact.
\begin{center}
\subheading{===== Strengths =====}
\subheading{===== Strengths =====}
\end{center}
I believe this paper describes a valuable work and contribution, that I appreciated learning about.
\begin{itemize}
\item The authors follow a thorough and valuable methodology, establishing excellent guarantees on the implementation considered.
\item It is great to see a development such as VST being used in this context.
\item Additionally, going the extra-mile to both refine the C code against RFC and prove this specification to be equivalent to the mathematical model is indeed I believe the right way to go.
\item They position their paper in a quite dense corpus of work in a quite satisfactory way.
\item The provided artifact showcase a significant proof effort.
\item I found barely a couple of typos while reading the paper.
\item The conclusion is particularly nice.
\item The diff provided between the verified C code and the original code is excellent. Overall there is a great care in stating clearly and precisely what has been proved.
\item The authors follow a thorough and valuable methodology, establishing excellent guarantees on the implementation considered.
\item It is great to see a development such as VST being used in this context.
\item Additionally, going the extra-mile to both refine the C code against RFC and prove this specification to be equivalent to the mathematical model is indeed I believe the right way to go.
\item They position their paper in a quite dense corpus of work in a quite satisfactory way.
\item The provided artifact showcase a significant proof effort.
\item I found barely a couple of typos while reading the paper.
\item The conclusion is particularly nice.
\item The diff provided between the verified C code and the original code is excellent. Overall there is a great care in stating clearly and precisely what has been proved.
\end{itemize}
\begin{center}
\subheading{===== Weaknesses =====}
\subheading{===== Weaknesses =====}
\end{center}
Such a paper is difficult to write. The authors have visibly devoted great efforts to tackle this difficulty, but it remains a challenging read.
\begin{itemize}
\item The paper takes us from one technical point to another in a manner that seems arbitrary at times, and hinders the overall structure. The problem is quite global, but a typical example is Definition 2.3: as a non-expert, it is hard to understand why this notion is important to introduce here, and it is essentially not used anywhere in the paper.
\item The paper takes us from one technical point to another in a manner that seems arbitrary at times, and hinders the overall structure. The problem is quite global, but a typical example is Definition 2.3: as a non-expert, it is hard to understand why this notion is important to introduce here, and it is essentially not used anywhere in the paper.
\end{itemize}
\begin{answer}
Computations over Curve25519 are done in $\F{p}$, as a result an easy mistake is to assume the curve defined over $\F{p}$ for all $x \in \F{p}$. However Curve25519 is defined over the quadratic extension which makes the Curve25519 over $\F{p}$ and its quadratic twist isomorphic over $\F{p^2}$ (Definition 2.3).
The notion of the twist of Curve25519 is quite central in the proof of the second main theorem of our paper,
which is linking our formalization of the RFC to the mathematical definition of Curve25519.
We therefore feel like it should not be omitted from the preliminaries, but we are of course
open to suggestions how to motivate the definition better at this early point of the paper.
\end{answer}
\begin{itemize}
\item Figure 1 and Figure 4 are great, and have the potential to help so much the reader against the previous issue. Unfortunately, they are not commenting, and hence fail to do so!
\item The protocol considered is standard, and its implementation made to be of reasonable complexity. The paper should therefore really aim to:
\begin{enumerate}
\item promote a new approach (full stack, use of VST, use of the B\&S elliptic curve library,...)
\item explain all specific difficulties and unexpected problems that came across to smooth the path to similar projects in the future;
\item give a sense of whether it would scale and/or be reusable for similar/related projects. In particular, the choice of TweetNaCl is never really motivated. How much of a challenge would proving the same result over a more complex/efficient implementation be?
\end{enumerate}
The paper does a good job at 1, but unfortunately a quite poor at 2 and 3.
\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.
\item Figure 1 and Figure 4 are great, and have the potential to help so much the reader against the previous issue. Unfortunately, they are not commenting, and hence fail to do so!
\end{itemize}
\begin{answer}
We extended the discussion of Figures 1, 3, and 4 to address this point.
\end{answer}
\begin{itemize}
\item The protocol considered is standard, and its implementation made to be of reasonable complexity. The paper should therefore really aim to:
\begin{enumerate}
\item promote a new approach (full stack, use of VST, use of the B\&S elliptic curve library,...)
\item explain all specific difficulties and unexpected problems that came across to smooth the path to similar projects in the future;
\item give a sense of whether it would scale and/or be reusable for similar/related projects. In particular, the choice of TweetNaCl is never really motivated. How much of a challenge would proving the same result over a more complex/efficient implementation be?
\end{enumerate}
The paper does a good job at 1, but unfortunately a quite poor at 2 and 3.
\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.}
\end{answer}
\begin{center}
\subheading{===== Detailed comments for authors =====}
\subheading{===== Detailed comments for authors =====}
\end{center}
My feelings are essentially summed up through the strengths and weaknesses described above. I find this work to be a great contribution, but regret having a hard time getting as much as I would like out of the paper.
......@@ -97,144 +109,187 @@ You mention in the rebuttal to a previous submission that constant time is not a
On a side note, I failed to compile the project: setting up an opam switch with Coq pinned to 8.8.2 as instructed, I had dependency issues with respect to `coq-coqprime`when running `opam install --deps-only coq-verif-tweetnacl `. Having installed manually `coq-coqprime`, I then ended up with the following error:
{\footnotesize\texttt{
"The following dependencies couldn't be met:\\
- coq-verif-tweetnacl $\rightarrow$ coq-stdpp \\
unknown package\\
No solution found, exiting"}}
"The following dependencies couldn't be met:\\
- coq-verif-tweetnacl $\rightarrow$ coq-stdpp \\
unknown package\\
No solution found, exiting"}}
\begin{answer}
We were not able to reproduce this error, but
now make the code available in an anonymous GitHub repository that also contains
a virtual-machine image with all software that is required to reproduce the proofs.
\end{answer}
Here are a few linear comments:
\begin{itemize}
\item \textbf{page 1, column 2:}\\
- "the program satisfy" $\rightarrow$ "the program satisfies"\\
- "the result of this paper can readily be used in mechanized proofs of higher-level protocols (...)"
This statement should probably be made more precise, it is quite unclear to me what you mean exactly.
\item \textbf{page 2:}\\
Figure 1 is great, but would deserve a lengthy explanation!
\item \textbf{page 1, column 2:}\\
- "the program satisfy" $\rightarrow$ "the program satisfies"\\
- "the result of this paper can readily be used in mechanized proofs of higher-level protocols (...)"
This statement should probably be made more precise, it is quite unclear to me what you mean exactly.
\end{itemize}
\begin{answer}
We added an additional description of the figure.
Typo fixed (the satisfy/satisfies actually refers to the semantics of a program in this sentence).
We rephrased the second statement to (hopefully) clarify what we mean.
\end{answer}
\begin{itemize}
\item \textbf{page 3, column 1:}\\
Definition 2.3: It's been very unclear to me as a non-expert in cryptography and this protocole in particular what was the purpose of this definition.\\
{\color{gray}"depending of" $\rightarrow$ "depending on"}\\
"depending of the value of the kth bit" $\rightarrow$ unclear what k is at this point
\item \textbf{page 3, column 2:}\\
Algorithm 1: unclear what "m" is\\
{\color{gray}"RFC 7748 standardize" $\rightarrow$ "RFC 7748 standardizes"}
\item \textbf{page 4, column 2:}\\
It's minor, but it is more shiny nowadays to cite The Odd Order theorem that the Four Color theorem as a mathematical achievement in Coq\\
CompCert $\rightarrow$ Wrong hyphenation\\
Hoare-seq $\rightarrow$ It is clearly hard to find the balance with respect to what should be assumed on the crypto side, and what should be assumed on the verification side. I nonetheless think that this should be omitted.\\
"Separation logic is an extension of Hoare logic" $\rightarrow$ Minor, but the work "extension" does not quite sit right with me. The model is quite intrinsically different.
\item \textbf{page 2:}\\
Figure 1 is great, but would deserve a lengthy explanation!
\end{itemize}
\begin{answer}
We added an additional description of the figure.
\end{answer}
\item \textbf{page 5, column 2:}\\
"'To implement (...)" $\rightarrow$ I am very confused by this. The whole paragraph is an unannounced quote, it would need context/explanation.
\begin{itemize}
\item \textbf{page 6, column 1:}\\
In ListofZn\_fp $\rightarrow$ The use of fuel might deserve a comment. Don't you end up having to prove at some point that you can always compute ahead of time an overapproximation of the fuel needed? Wouldn't it have been simple to use the strong recursion principle of naturals to define the function?
\item \textbf{page 3, column 1:}\\
Definition 2.3: It's been very unclear to me as a non-expert in cryptography and this protocole in particular what was the purpose of this definition.\\
{\color{gray}"depending of" $\rightarrow$ "depending on"}\\
"depending of the value of the kth bit" $\rightarrow$ unclear what k is at this point
\end{itemize}
\begin{answer}
Regarding Definition 2.3 see our answer above. Typo fixed.
We updated the text to clarify what we mean by the $k$th bit.
\end{answer}
\begin{answer}
In our case the fuel is used to garantee to have as an output a list of 32 elements. This allows to prove that for all List of 32 bytes, ListofZn\_fp (ZofList L) = L. With this lemma at hand we can later simplify some of the expressions.
\end{answer}
\begin{itemize}
\item \textbf{page 3, column 2:}\\
Algorithm 1: unclear what "m" is\\
"RFC 7748 standardize" $\rightarrow$ "RFC 7748 standardizes"
\end{itemize}
\begin{answer}
Clarified that $m$ is an upper bound on the bitlength of the scalar. Typo fixed.
\end{answer}
\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.
\begin{itemize}
\item \textbf{page 4, column 2:}\\
It's minor, but it is more shiny nowadays to cite The Odd Order theorem that the Four Color theorem as a mathematical achievement in Coq\\
CompCert $\rightarrow$ Wrong hyphenation\\
Hoare-seq $\rightarrow$ It is clearly hard to find the balance with respect to what should be assumed on the crypto side, and what should be assumed on the verification side. I nonetheless think that this should be omitted.\\
"Separation logic is an extension of Hoare logic" $\rightarrow$ Minor, but the work "extension" does not quite sit right with me. The model is quite intrinsically different.
\end{itemize}
\begin{answer}
\todo{Fix, comment here.}
\end{answer}
\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
\begin{itemize}
\item \textbf{page 5, column 2:}\\
"'To implement (...)" $\rightarrow$ I am very confused by this. The whole paragraph is an unannounced quote, it would need context/explanation.
\end{itemize}
\begin{answer}
\todo{Fix, comment here.}
\end{answer}
\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.
\begin{itemize}
\item \textbf{page 6, column 1:}\\
In ListofZn\_fp $\rightarrow$ The use of fuel might deserve a comment. Don't you end up having to prove at some point that you can always compute ahead of time an overapproximation of the fuel needed? Wouldn't it have been simple to use the strong recursion principle of naturals to define the function?
\end{itemize}
\begin{answer}
In our case the fuel is used to garantee to have as an output a list of 32 elements. This allows to prove that for all List of 32 bytes, ListofZn\_fp (ZofList L) = L. With this lemma at hand we can later simplify some of the expressions.
\end{answer}
\item \textbf{page 9:}\\
{\color{gray}"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.}
\begin{itemize}
\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.
\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
\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.
\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.
\end{itemize}
\begin{answer}
Fixed.
\end{answer}
\item \textbf{page 11:}\\
Figure 4: this one is the apex: it would deserve a full column of explanations
\begin{itemize}
\item \textbf{page 11:}\\
Figure 4: this one is the apex: it would deserve a full column of explanations
\end{itemize}
\begin{answer}
\todo{How much explanation did we actually add here?}
\end{answer}
\item \textbf{Conclusion:}\\
Great wrap up overall.\\
CompCert: "However, when compiling (...)" $\rightarrow$ I am quite confused about this sentence. Do you mean when compiling the verified C code with gcc? If so, beyond the question whether CompCert matches C17 (which it doesn't, it matches C99), the real problem is to assume that gcc is bug free! I would expect with this whole approach that the expectation is to run a protocole compiled with CompCert.\\
clightGen: "VST does not support (...)" $\rightarrow$ Hard to undertand the relation between this sentence and the previous one.\\
Extending our work: What about proving other NaCl implementations?
\begin{itemize}
\item \textbf{Conclusion:}\\
Great wrap up overall.\\
CompCert: "However, when compiling (...)" $\rightarrow$ I am quite confused about this sentence. Do you mean when compiling the verified C code with gcc? If so, beyond the question whether CompCert matches C17 (which it doesn't, it matches C99), the real problem is to assume that gcc is bug free! I would expect with this whole approach that the expectation is to run a protocole compiled with CompCert.\\
clightGen: "VST does not support (...)" $\rightarrow$ Hard to undertand the relation between this sentence and the previous one.\\
Extending our work: What about proving other NaCl implementations?
\end{itemize}
\begin{answer}
\todo{Freek : which version of ISO.}
\todo{Freek : which version of ISO.}
\end{answer}
\begin{center}
\subheading{===== Requested changes =====}
\subheading{===== Requested changes =====}
\end{center}
\begin{itemize}
\item Please provide high level explanations to your three Figures describing the infrastructure.
\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
\item Please provide more get away lessons from this development that would benefit new similar works
\item Please give a sense of the difficulties encountered during the formalization.
\item Please provide high level explanations to your three Figures describing the infrastructure.
\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
\item Please provide more get away lessons from this development that would benefit new similar works
\item Please give a sense of the difficulties encountered during the formalization.
\end{itemize}
\begin{center}
\subheading{===== Questions for authors' response =====}
\subheading{===== Questions for authors' response =====}
\end{center}
\begin{itemize}
\item What made TweetNaCl the right choice for this project?
\item What made TweetNaCl the right choice for this project?
\end{itemize}
\begin{answer}
One goal of the project was to investigate how suitable the combination of
VST+Coq is for verifying correctness of existing C code for asymmetric
crypto primitives. The X25519 implementation in TweetNaCl was chosen because
it is relatively simple, it has some real-world use cases, and the original
paper claims that the library should be verifiable.
One goal of the project was to investigate how suitable the combination of
VST+Coq is for verifying correctness of existing C code for asymmetric
crypto primitives. The X25519 implementation in TweetNaCl was chosen because
it is relatively simple, it has some real-world use cases, and the original
paper claims that the library should be verifiable.
\end{answer}
\begin{itemize}
\item Would following the same approach for other implementation radically change the proof effort?
\item Would following the same approach for other implementation radically change the proof effort?
\end{itemize}
\begin{answer}
We would expect that the proof effort for another C implementation of X25519
does not change drastically, as long as it does not use any features that are
not supported by VST (e.g., the 128-bit integers used by the donna64
implementation). The proof relating the RFC to the mathematical definition
does not change for other implementations.
We would expect that the proof effort for another C implementation of X25519
does not change drastically, as long as it does not use any features that are
not supported by VST (e.g., the 128-bit integers used by the donna64
implementation). The proof relating the RFC to the mathematical definition
does not change for other implementations.
\end{answer}
\begin{itemize}
\item Does compiling TweetNaCl with CompCert rather than gcc impact the performance beyond what is acceptable?
\item Does compiling TweetNaCl with CompCert rather than gcc impact the performance beyond what is acceptable?
\end{itemize}
\begin{answer}
For the X25519 implementation in TweetNaCl, CompCert generates code that is
about 6x slower than code generated with gcc. While this sounds like a lot, it
may not be too much of an issue for projects that use TweetNaCl, because they
chose for a library that prioritizes simplicity over performance in the first
place. A more serious issue however can be the non-free CompCert license.
For the X25519 implementation in TweetNaCl, CompCert generates code that is
about 6$\times$ slower than code generated with gcc. While this sounds like a lot, it
may not be too much of an issue for projects that use TweetNaCl, because they
chose for a library that prioritizes simplicity over performance in the first
place. A more serious issue however can be the non-free CompCert license.
\end{answer}
\begin{itemize}
\item If so, what trust do you consider this proof effort to bring to a gcc compiled implementation?
\item If so, what trust do you consider this proof effort to bring to a gcc compiled implementation?
\end{itemize}
\begin{answer}
We are not aware of any bugs that were introduced into ECC software by bugs in
gcc; so from a practical, crypto-engineering point of view we rule out all
classes of bugs that users are typically concerned about. From a more
theoretical point of view, relying on gcc (or any other unverified C compiler)
massively expands the TCB and should be reason for concern.
We are not aware of any bugs that were introduced into ECC software by bugs in
gcc; so from a practical, crypto-engineering point of view we rule out all
classes of bugs that users are typically concerned about. From a more
theoretical point of view, relying on gcc (or any other unverified C compiler)
massively expands the TCB and should be reason for concern.
\end{answer}
\newpage
\section{Usenix Security 2020 Review \#324B}
\section*{Usenix Security 2020 Review \#324B}
\begin{tabular}{rrp{.6\textwidth}}
\toprule
......@@ -31,9 +31,27 @@ This paper presents two formal proofs. The first links a C implementation of the
\begin{itemize}
\item The C code analyzed here is very simple; prior works have verified much more complex and optimized implementations of X25519
\end{itemize}
\begin{answer}
It is true that the C code is more simple and less optimized than the code considered in other verification efforts.
However, unlike \emph{most} previous X25519 verification efforts we verify pre-existing code written in a language
that is not developed with easy verification in mind (like jasmin or F$^*$).
Also, our proof goes beyond what all previous X25519 verification efforts targeted and links the
high-level specification to the mathematical definition of X25519.
\end{answer}
\begin{itemize}
\item The proof does not cover side-channel resistance ("constant-time")
\end{itemize}
\begin{answer}
We added a comment on ``constant-time'' verification in the introduction.
\end{answer}
\begin{itemize}
\item The details of the Coq formalization may be less interesting for non-formally oriented readers
\end{itemize}
\begin{answer}
This is true; we hope that the audience of CSF is generally more oriented towards formal verification
than (most of) the USENIX audience.
\end{answer}
\begin{center}
\subheading{===== Detailed comments for authors =====}
......@@ -56,6 +74,25 @@ I enjoyed Section 5 and I believe it is one of the more important (and reusable)
\begin{itemize}
\item Show a known bug that the VST proof would prevent
\end{itemize}
\begin{answer}
The most concerning bugs are, as the reviewer mentions, carry bugs that are triggered only with
very small probability on random inputs. As TweetNaCl uses a different internal representation
of field elements than the speed-optimized implementations that had such bugs in the past, we
cannot easily put precisely such a known bug into the software.\\
As we provide the software together with the proofs, it is easy though, to see how the proof fails,
if, for example the final call to \texttt{car25519} in the \texttt{M} routine is omitted.
\end{answer}
\begin{itemize}
\item Clarify that constant-timeness is not proved here
\end{itemize}
\begin{answer}
This is clarified in the introduction now.
\end{answer}
\begin{itemize}
\item Rewrite section 5 to focus on proof structure and a few well-chosen lemmas/definitions
\end{itemize}
\begin{answer}
\todo{Say what we did here}
\end{answer}
\newpage
\section{Usenix Security 2020 Review \#324C}
\section*{Usenix Security 2020 Review \#324C}
\begin{tabular}{rrp{.6\textwidth}}
\toprule
......@@ -95,6 +95,7 @@ Let me start by stating that I’m no expert but rather an enthusiast hoping to
\item bugs in the freezing (full modular reduction) of the final result,
\item inconsistencies between the specification and the mathematical model.
\end{itemize}
We extended the discussion with regards to [12] in our related-work session now.
\end{answer}
\begin{center}
......
\newpage
\section{Usenix Security 2020 Review \#324D}
\section*{Usenix Security 2020 Review \#324D}
\begin{tabular}{rrp{.6\textwidth}}
\toprule
......@@ -56,4 +56,7 @@ So, while I really like this work, the lack of reproducibility even with access
Please provide a working version, either clear instructions on how to build, or maybe a virtual machine image.
\begin{answer}
The revised version of the paper includes a link to an anonymous GitHub repository,
which also contains a virtual-machine image.
\end{answer}
\newpage
\section{Usenix Security 2020 Review \#324E}
\section*{Usenix Security 2020 Review \#324E}
\begin{tabular}{rrp{.6\textwidth}}
\toprule
......@@ -40,5 +40,9 @@ In the end, I strongly feel that this paper must be rewritten with the low level
\end{center}
Why was this submitted to USENIX? S\&P seems like a much better venue.
\begin{answer}
Apparently the reviewer did not realize that the work had been submitted to S\&P before.
We hope that CSF is also a much better venue.
\end{answer}
What am I to take away from this? How does this generalize?
\newpage
\section{Usenix Security 2020 Review \#324F}
\section*{Usenix Security 2020 Review \#324F}
\begin{tabular}{rrp{.6\textwidth}}
\toprule
......
\newpage
\section{Usenix Security 2020 Review \#324G}
\section*{Usenix Security 2020 Review \#324G}
\begin{tabular}{rrp{.6\textwidth}}
\toprule
......
......@@ -53,12 +53,41 @@ To our knowledge, this verification effort is the first to not just
connect a low-level implementation to a higher-level implementation (or ``specification''),
but to prove correctness all the way up
to the mathematical definition in terms of scalar multiplication on an elliptic curve.
As a consequence, the result of this paper can readily be used in mechanized proofs of
higher-level protocols that work with the mathematical definition of X25519.
As a consequence, the result of this paper can readily be used in mechanized proofs
arguing about the security of cryptographic constructions on the more abstract
level of operations in groups and related problems, like the elliptic-curve
discrete-logarithm (ECDLP) or elliptic-curve Diffie-Hellman (ECDH) problem.
\todo{Add examples of such mechanized proofs?}
Also, connecting our formalization of the RFC to the mathematical definition
significantly increases trust into the correctness of the formalization and
reduces the effort of manual auditing of that formalization.
\subheading{The bigger picture of high-assurance crypto.}
This work fits into the bigger area of \emph{high-assurance} cryptography,
i.e., a line of work that applies techniques and tools from formal methods
to obtain computer-verified guarantees for cryptographic software.
Traditionally, high-assurance cryptography is concerned with three main properties
of cryptographic software:
\begin{enumerate}
\item verifying \textbf{correctness} of cryptographic software,
typically against a high-level specification;\label{hacs:correct}
\item verifying \textbf{implementation security} and in particular
security against timing attacks; and\label{hacs:sca}
\item verifying \textbf{cryptographic security} notions of primitives and protocols
through computer-checked reductions from some assumed-to-be-hard mathematical problem.\label{hacs:secure}
\end{enumerate}
A recent addition to this triplet (or rather an extension of implementation security)
is security also against speculative attacks. See, e.g.,~\cite{XXX}.
This paper targets only the first point and attempts to make results
immediately usable for verification efforts of cryptographic security.
Verification of implementation security is probably equally important as
verification of correctness, but working on the C language level as we do
in this paper is not helpful. To obtain guarantees of security against
timing-attack we recommend verifying \emph{compiled} code on LLVM level with,
e.g., ct-verif~\cite{XXX},
or even better on binary level with, e.g., BinSec/Rel~\cite{XXX}.
\subheading{Related work.}
The field of computer-aided cryptography, i.e., using computer-verified proofs
to strengthen our trust into cryptographic constructions and cryptographic software,
......@@ -103,6 +132,10 @@ Their proof takes a different approach from ours.
It uses heavy annotation of the assembly-level code in order to ``guide'' a SAT solver;
also, it does not cover the full X25519 functionality and does
not make the link to the mathematical definition from~\cite{Ber06}.
As a consequence, this work would not find bugs in any of the routines
processing the scalar (like ``clamping'', see Section~\ref{subsec:X25519-key-exchange}),
bugs in the the serialization routines or, maybe most importantly,
bugs in the high-level specification that the code is verified against.
Finally, in terms of languages and tooling the work closest to what we present here
is the proof of correctness of OpenSSL's
......
......@@ -23,7 +23,6 @@ Finally, we provide a brief description of the formal tools we use in our proofs
\end{dfn}
Details of the formalization can be found in \sref{subsec:ECC-Montgomery}.
For $M_{a,b}$ over a finite field $\F{p}$, the parameter $b$ is known as the ``twisting factor''.
For $b'\in \F{p}\backslash\{0\}$ and $b' \neq b$, the curves $M_{a,b}$ and $M_{a,b'}$
are isomorphic via $(x,y) \mapsto (x, \sqrt{b/b'} \cdot y)$.
......@@ -51,10 +50,13 @@ We define the operation:
\texttt{xDBL\&ADD} & : (x_{Q-P}, (X_P:Z_P), (X_Q:Z_Q)) \mapsto \\
& ((X_{2 \cdot P}:Z_{2 \cdot P}), (X_{P + Q}:Z_{P + Q}))
\end{align*}
In the Montgomery ladder, % notice that
% the arguments of \texttt{xADD} and \texttt{xDBL}
A pseudocode description of the Montgomery ladder
is given in Algorithm~\ref{alg:montgomery-ladder}.
The main loop iterates over the bits of the scalar $n$.
The $k^{\text{th}}$ iteration conditionally swaps
the arguments $P$ and $Q$ of \texttt{xDBL\&ADD}
are swapped depending on the value of the $k^{\text{th}}$ bit.
depending on the value of the $k^{\text{th}}$ bit of $n$.
We use a conditional swap \texttt{CSWAP} to change the arguments of the above
function while keeping the same body of the loop. \label{cswap}
Given a pair $(P_0, P_1)$ and a bit $b$, \texttt{CSWAP} returns the pair
......@@ -66,7 +68,7 @@ computing a \xcoord-only scalar multiplication (see \aref{alg:montgomery-ladder}
\caption{Montgomery ladder for scalar mult.}
\label{alg:montgomery-ladder}
\begin{algorithmic}
\REQUIRE{\xcoord $x_P$ of a point $P$, scalar $n$ with $n < 2^m$}
\REQUIRE{\xcoord $x_P$ of a point $P$, scalar $n$ of bitlength upperbound by some integer $m$}
\ENSURE{\xcoord $x_Q$ of $Q = n \cdot P$}
\STATE $Q = (X_Q:Z_Q) \leftarrow (1:0)$
\STATE $R = (X_R:Z_R) \leftarrow (x_P:1)$
......
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