Commit 68f0e50f authored by benoit's avatar benoit
Browse files

more answers

parent 040287a7
all: tweetverif.pdf csf-supplementary/previous.pdf
SOURCES= code-tweetnacl.tex collection.bib conclusion.tex coq.tex highlevel.tex intro.tex lowlevel.tex preliminaries.tex proofs.tex rfc.tex t.bib tweetverif.tex tweetnacl.diff
PREVIOUS= csf-supplementary/previous.tex csf-supplementary/usenix-*.tex csf-supplementary/tweetverif-USENIX.pdf csf-supplementary/tweetverif-SP.pdf
tweetverif.pdf: $(SOURCES)
pdflatex tweetverif.tex
......@@ -8,7 +9,7 @@ tweetverif.pdf: $(SOURCES)
pdflatex tweetverif.tex
pdflatex tweetverif.tex
csf-supplementary/previous.pdf:
csf-supplementary/previous.pdf: $(PREVIOUS)
make -C csf-supplementary
tweetnacl.diff:
......
......@@ -2,10 +2,10 @@
\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 \\
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}
......@@ -71,7 +71,7 @@ Such a paper is difficult to write. The authors have visibly devoted great effor
\end{itemize}
\begin{answer}
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.
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}
......@@ -84,13 +84,13 @@ Such a paper is difficult to write. The authors have visibly devoted great effor
\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}
\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.
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}
......@@ -114,7 +114,7 @@ On a side note, I failed to compile the project: setting up an opam switch with
unknown package\\
No solution found, exiting"}}
\begin{answer}
We were not able to reproduce this error, but
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}
......@@ -123,18 +123,20 @@ 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.
- "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}
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.
\begin{itemize}
\item[$-$] Typo fixed (the satisfy/satisfies actually refers to the semantics of a program in this sentence).
\item[$-$]We rephrased the second statement to (hopefully) clarify what we mean.
\end{itemize}
\end{answer}
\begin{itemize}
\item \textbf{page 2:}\\
Figure 1 is great, but would deserve a lengthy explanation!
Figure 1 is great, but would deserve a lengthy explanation!
\end{itemize}
\begin{answer}
We added an additional description of the figure.
......@@ -143,19 +145,22 @@ Here are a few linear comments:
\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
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.
\begin{itemize}
\item[$-$] Regarding Definition 2.3 see our answer above.
\item[$-$] Typo fixed.
\item[$-$] We updated the text to clarify what we mean by the $k$th bit.
\end{itemize}
\end{answer}
\begin{itemize}
\item \textbf{page 3, column 2:}\\
Algorithm 1: unclear what "m" is\\
"RFC 7748 standardize" $\rightarrow$ "RFC 7748 standardizes"
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.
......@@ -163,70 +168,80 @@ Here are a few linear comments:
\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.
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}
\begin{itemize}
\item \todo{address other comments}
\item The paper introducing separation logic describes it as \emph{``an extension of Hoare logic''}.
See \url{https://www.cs.cmu.edu/~jcr/seplogic.pdf}.
\item \todo{address other comments}
\item[$-$] While the Odd Order theorem is shinier for the complexity of the work, it may not be as well known as the Four Color theorem. This lack of exposition makes its proof less impressive to readers not familiar with the subject.
\item[$-$] We fixed the hyphenation.
\item[$-$] The Hoare logic is not a known subject for most cryptographers not familiar with formal methods. In our opinion, the Hoare-Sec rule is the easiest rule with material (as opposed to Hoare-Skip) to understand by its composition nature and as it also relates to how instructions are read in the source code of a program.
\item[$-$] The Separation Logic was introduced by their authors \emph{``an extension of Hoare logic''}. See See \url{https://www.cs.cmu.edu/~jcr/seplogic.pdf}.
\end{itemize}
\end{answer}
\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.
"'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.}
Fixed, we added an introduction sentence.
\end{answer}
\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?
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}
\begin{answer}
In our case the fuel is used to garantee to have as an output a list of 32 elements. This allows us 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 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.
"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}
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:" ?}
\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
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 on 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}
\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.
\end{itemize}
\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.
"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}
\begin{itemize}
\item[$-$] We removed the reflection mention, more explanations would require too many implementation details.
\item[$-$] We added a paragraph to describe the content of Figure 3.
\end{itemize}
\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.
"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.
......@@ -234,18 +249,19 @@ Here are a few linear comments:
\begin{itemize}
\item \textbf{page 11:}\\
Figure 4: this one is the apex: it would deserve a full column of explanations
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?}
In addition to Figure 4, we added a full paragraph providing the red line of the proof of this theorem.
We hope to provide suficiant insights of the dependencies between lemmas to arrive into the final theorem.
\end{answer}
\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?
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}
......@@ -259,7 +275,7 @@ Here are a few linear comments:
\item Please provide high level explanations to your three Figures describing the infrastructure.
\end{itemize}
\begin{answer}
\todo{We added such high-level descriptions.}
We added high-level description of Figures 1, 3 and 4. They should help the reader to follow the line of the proof.
\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
......
......@@ -2,51 +2,51 @@
\section*{Usenix Security 2020 Review \#324B}
\begin{tabular}{rrp{.6\textwidth}}
\toprule
Review recommendation & 4. & Minor revision \\
Writing quality & 4. & Well-written \\
Reviewer interest & 3. & I would definitely go to this talk and tell my students or colleagues colleages to read this paper \\
Reviewer expertise & 4. & Expert \\
\bottomrule
\toprule
Review recommendation & 4. & Minor revision \\
Writing quality & 4. & Well-written \\
Reviewer interest & 3. & I would definitely go to this talk and tell my students or colleagues colleages to read this paper \\
Reviewer expertise & 4. & Expert \\
\bottomrule
\end{tabular}
\begin{center}
\subheading{===== Paper summary =====}
\subheading{===== Paper summary =====}
\end{center}
This paper presents two formal proofs. The first links a C implementation of the popular X25519 elliptic curve Diffie-Hellman construction, taken from a crypto library called TweetNaCl, to a formalization of its specification as per RFC 7748. The second links the RFC 7748 formalization to the mathematical theory of elliptic curves. In composition, the two results mean that the TweetNaCl implementation of X25519 meets the abstract mathematical description of Curve25519 in [7]. All proofs are mechanized in the Coq theorem prover, with some help from the Verified Software Toolchain (VST).
\begin{center}
\subheading{===== Strengths =====}
\subheading{===== Strengths =====}
\end{center}
\begin{itemize}
\item A formal proof of an important component of TweetNaCl, a popular crypto library
\item A proof that RFC 7748 meets its mathematical spec, which is of independent interest
\item A major new case study for the VST framework
\item A formal proof of an important component of TweetNaCl, a popular crypto library
\item A proof that RFC 7748 meets its mathematical spec, which is of independent interest
\item A major new case study for the VST framework
\end{itemize}
\begin{center}
\subheading{===== Weaknesses =====}
\subheading{===== Weaknesses =====}
\end{center}
\begin{itemize}
\item The C code analyzed here is very simple; prior works have verified much more complex and optimized implementations of X25519
\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$^*$).
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")
\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.
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
\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
......@@ -54,7 +54,7 @@ This paper presents two formal proofs. The first links a C implementation of the
\end{answer}
\begin{center}
\subheading{===== Detailed comments for authors =====}
\subheading{===== Detailed comments for authors =====}
\end{center}
This works provides a rare fully formalized proof linking a mathematical description of a cryptographic construction to a concrete widely-used C implementation. Bridging this gap with a theorem prover requires expertise in the underlying mathematics, in formal verification, and in cryptographic engineering. We need more papers like this to show how this can be done.
......@@ -76,30 +76,33 @@ I enjoyed Section 5 and I believe it is one of the more important (and reusable)
\begin{center}
\subheading{===== Requested changes =====}
\subheading{===== Requested changes =====}
\end{center}
\begin{itemize}
\item Show a known bug that the VST proof would prevent
\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,
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
\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
\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}
By including a descriptions to figures 3 and 4, we provide a better readding experience of the subsequent proofs.
The reader is not faced anymore with a list of lemmas and theorem but can understand why they arrive in such order.
In addition to those paragraphs we reduced the technical material provided; these two modifications results in
improved readability of the full section.
\end{answer}
......@@ -3,10 +3,10 @@
\begin{tabular}{rrp{.6\textwidth}}
\toprule
Review recommendation & 1.& Reject \\
Writing quality & 2.& Needs improvement \\
Reviewer interest & 1.& I am not interested in this paper \\
Reviewer expertise & 2.& Some familiarity \\
Review recommendation & 1. & Reject \\
Writing quality & 2. & Needs improvement \\
Reviewer interest & 1. & I am not interested in this paper \\
Reviewer expertise & 2. & Some familiarity \\
\bottomrule
\end{tabular}
......@@ -41,8 +41,8 @@ In the end, I strongly feel that this paper must be rewritten with the low level
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.
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?
......@@ -3,10 +3,10 @@
\begin{tabular}{rrp{.6\textwidth}}
\toprule
Review recommendation & 2.& Reject and resubmit \\
Writing quality & 2.& Needs improvement \\
Reviewer interest & 2.& I might go to a talk about this \\
Reviewer expertise & 3.& Knowledgeable \\
Review recommendation & 2. & Reject and resubmit \\
Writing quality & 2. & Needs improvement \\
Reviewer interest & 2. & I might go to a talk about this \\
Reviewer expertise & 3. & Knowledgeable \\
\bottomrule
\end{tabular}
......@@ -60,4 +60,6 @@ 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}
\begin{answer}
\todo{Should add some reply here somewhere}
\end{answer}
......@@ -3,10 +3,10 @@
\begin{tabular}{rrp{.6\textwidth}}
\toprule
Review recommendation & 4.& Minor revision \\
Writing quality & 4.& Well-written \\
Reviewer interest & 2.& I might go to a talk about this \\
Reviewer expertise & 2.& Some familiarity \\
Review recommendation & 4. & Minor revision \\
Writing quality & 4. & Well-written \\
Reviewer interest & 2. & I might go to a talk about this \\
Reviewer expertise & 2. & Some familiarity \\
\bottomrule
\end{tabular}
......@@ -55,5 +55,7 @@ If the paper was proposing a new technique which could be applied more generally
\item Describe which parts of the contributions could possibly be applied more generally.
\end{itemize}
\begin{answer}
\todo{Should add some reply here somewhere}
\end{answer}
\todo{Should add some reply here somewhere}
......@@ -5,8 +5,8 @@ In this section we prove the following theorem:
% In this section we outline the structure of our proofs of the following theorem:
\begin{informaltheorem}
The implementation of X25519 in TweetNaCl (\TNaCle{crypto_scalarmult}) matches
the specifications of RFC~7748~\cite{rfc7748} (\Coqe{RFC}).
The implementation of X25519 in TweetNaCl (\TNaCle{crypto_scalarmult}) matches
the specifications of RFC~7748~\cite{rfc7748} (\Coqe{RFC}).
\end{informaltheorem}
More formally:
......@@ -242,8 +242,9 @@ the same time.
\subsection{Number representation and C implementation}
\label{subsec:num-repr-rfc}
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
As described in \sref{subsec:Number-TweetNaCl}, numbers in \TNaCle{gf}
(typedef of an array of 16 \TNaCle{long long}) 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 an integer.
We reuse the mapping
......@@ -262,8 +263,8 @@ Equivalence between operations in $\Zfield$ (\ie under \coqe{:GF}) and in $\Ffie
Using these two definitions, we prove intermediate lemmas such as the correctness of the
multiplication \Coqe{Low.M} where \Coqe{Low.M} replicates the computations and steps done in C.
\begin{lemma}
\label{lemma:mult_correct}
\Coqe{Low.M} correctly implements the multiplication over $\Zfield$.
\label{lemma:mult_correct}
\Coqe{Low.M} correctly implements the multiplication over $\Zfield$.
\end{lemma}
And specified in Coq as follows:
\begin{lstlisting}[language=Coq]
......@@ -280,9 +281,9 @@ We also need to define the bounds under which the operation is correct,
allowing us to chain them, guaranteeing us the absence of overflow.
\begin{lemma}
\label{lemma:mult_bounded}
if all the values of the input arrays are constrained between $-2^{26}$ and $2^{26}$,
then the output of \coqe{Low.M} will be constrained between $-38$ and $2^{16} + 38$.
\label{lemma:mult_bounded}
if all the values of the input arrays are constrained between $-2^{26}$ and $2^{26}$,
then the output of \coqe{Low.M} will be constrained between $-38$ and $2^{16} + 38$.
\end{lemma}
And seen in Coq as follows:
\begin{lstlisting}[language=Coq]
......@@ -296,33 +297,28 @@ Lemma M_bound_Zlength :
\end{lstlisting}
Using reflection (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.
\end{lemma}
This statement is formalized as
\begin{lstlisting}[language=Coq]
Corollary Inv25519_Zpow_GF : forall (g:list Z),
length g = 16 ->
Z16.lst (Inv25519 g) :GF =
(pow (Z16.lst g) (2^255-21)) :GF.
\end{lstlisting}
% We prove the functional correctness of the multiplicative inverse over \Zfield,
% formalized as
% \begin{lstlisting}[language=Coq]
% Corollary Inv25519_Zpow_GF : forall (g:list Z),
% length g = 16 ->
% Z16.lst (Inv25519 g) :GF =
% (pow (Z16.lst g) (2^255-21)) :GF.
% \end{lstlisting}
\begin{sloppypar}
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 matches the exact behavior of X25519 in TweetNaCl.
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 matches the exact behavior of X25519 in TweetNaCl.
\end{sloppypar}
\begin{sloppypar}
By proving that each function \coqe{Low.M}; \coqe{Low.A}; \coqe{Low.Sq};
\coqe{Low.Zub}; \coqe{Unpack25519}; \coqe{clamp}; \coqe{Pack25519};
\coqe{Inv25519}; \coqe{car25519} behave over \coqe{list Z} as their equivalent
over \coqe{Z} with \coqe{:GF} (in \Zfield), we prove that given the same inputs
\coqe{Crypto_Scalarmult} performs the same computation as \coqe{RFC}.
By proving that each function \coqe{Low.M}; \coqe{Low.A}; \coqe{Low.Sq};
\coqe{Low.Zub}; \coqe{Unpack25519}; \coqe{clamp}; \coqe{Pack25519};
\coqe{Inv25519}; \coqe{car25519} behave over \coqe{list Z} as their equivalent
over \coqe{Z} with \coqe{:GF} (in \Zfield), we prove that given the same inputs
\coqe{Crypto_Scalarmult} performs the same computation as \coqe{RFC}.
\end{sloppypar}
% This is formalized as follows in Coq:
......
......@@ -94,6 +94,7 @@ Later in our proof we use a simpler description of the ladder
(\coqe{montgomery_rec}) which follows strictly \aref{alg:montgomery-ladder}
and prove those ladder equivalent.
RFC 7748 describes the calculations done in X25519 as follows:
\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
perform the following procedure, which is taken from [curve25519] and
......
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