Commit c3ea1b1e authored by Benoit Viguier's avatar Benoit Viguier
Browse files

more text

parent 374f9d0d
% \todo{
%
% - Get down to 12 pages: "no more than 12 pages long, excluding the bibliography,
% well-marked appendices, and supplementary material."
%
% - Emphasize:\\
% + the added confidence between in X25519 Correctness\\
% + proof of real world software\\
% }
%
% With respect to the reviews:
%
% \todo{
%
% - Give number of person-hours
%
% - "This did not become very clear, because you mostly describe names
% of tool while leaving out the details of what these tools carry out
% conceptually."\\
% + anotation have to be carried out through the proof to help the smt-solver,
% not in our case as we direct the proof.
%
% - "I was wondering whether you consider the approach in [13] as synthesis or
% verification, because to me, it seemed a mix/neither."\\
% + [13] is "Verified Low-Level Programming Embedded in F*",\\
% + reread [13] and answer in the "our answer part"
%
% - "[18] even uses Coq to verify a large portion of a C implementation of X25519
% fully automatically."\\
% + This is not verification, this is synthesis. The approach is completely different.
%
% - "Still, TweetNaCl is not necessarily the most complex (and certainly not the most
% efficient) implementation of X25519 that has been verified, which makes the
% novelty of this work hard to justify."\\
% + True, but all the other works have been from a spec and generate correct code
% approach, here we go the opposite way. While the code of other libraries are
% different, the montgomery ladder are often similar and the optimizations comes
% mostly from the big number computations.\\
%
% - "This is a well-known problem for formal
% verification papers, and I don’t have great advice except to suggest
% that the authors separate out the code fragments into figures and
% let the text focus on the high-level ideas of the code."\\
% + @PETER: How to address that ?
%
% - "At the end of Section IV, I would have loved to see some high-
% level lessons on what the proof taught you, and what part of this
% proof would be reusable if you decided to verify Ed25519 or X448
% or P-256, for example."\\
% + see second Todo
%
% - "It also appears that the authors do not verify the constant-time
% guarantees of the TweetNaCl code. Could this be done in their
% framework?"
% + Nope => mention in limitation at the end of the paper?
%
% - Clamping and section V.\\
% + The clamping allows to reduce the group to prime elements, we do not provide
% such proofs.\\
% - We prove that for all n the computations on the ladder holds.
%
% - "More importantly, could you claim that your proof of equivalence also provides
% a justification for the implementations of Fiat Crypto or HACL*, hence adding
% value to those other projects in addition to your own?"
% + Peter ?
% }
\todo{
- Get down to 12 pages: "no more than 12 pages long, excluding the bibliography,
well-marked appendices, and supplementary material."
- Emphasize:\\
+ the added confidence between in X25519 Correctness\\
+ proof of real world software\\
}
With respect to the reviews:
\todo{
- Give number of person-hours
ARGUE WHY WE DID NOT
- "This did not become very clear, because you mostly describe names
of tool while leaving out the details of what these tools carry out
conceptually."\\
+ anotation have to be carried out through the proof to help the smt-solver,
not in our case as we direct the proof.
- "I was wondering whether you consider the approach in [13] as synthesis or
verification, because to me, it seemed a mix/neither."\\
+ [13] is "Verified Low-Level Programming Embedded in F*",\\
+ reread [13] and answer in the "our answer part"
- "[18] even uses Coq to verify a large portion of a C implementation of X25519
fully automatically."\\
+ This is not verification, this is synthesis. The approach is completely different.
- "Still, TweetNaCl is not necessarily the most complex (and certainly not the most
efficient) implementation of X25519 that has been verified, which makes the
novelty of this work hard to justify."\\
+ True, but all the other works have been from a spec and generate correct code
approach, here we go the opposite way. While the code of other libraries are
different, the montgomery ladder are often similar and the optimizations comes
mostly from the big number computations.\\
- "It also appears that the authors do not verify the constant-time
guarantees of the TweetNaCl code. Could this be done in their
framework?"
+ Nope => mention in limitation at the end of the paper?
- Clamping and section V.\\
+ The clamping allows to reduce the group to prime elements, we do not provide
such proofs.\\
- We prove that for all n the computations on the ladder holds.
- "More importantly, could you claim that your proof of equivalence also provides
a justification for the implementations of Fiat Crypto or HACL*, hence adding
value to those other projects in addition to your own?"
+ Peter ?
}
......@@ -32,7 +32,7 @@ We discuss the plot twist (\ref{subsec:Zmodp}) of Curve25519 and solve it (\ref{
\subsection{Formalization of elliptic Curves}
\label{subsec:ECC}
\fref{tikz:ProofHighLevel1} presents a intuition of the proof.
\fref{tikz:ProofHighLevel1} presents an intuition of the proof.
\begin{figure}[h]
\centering
\include{tikz/highlevel1}
......
......@@ -93,7 +93,7 @@ level verification similar to \tref{thm:montgomery-ladder-correct}.
The verification \eg X448~\cite{cryptoeprint:2015:625,rfc7748} in C would
require the adaptation of most of the low level arithmetic (mainly the
multiplication, carry propagation and reductions).
multiplication, carry propagation and reduction).
Once the correctness and bounds of the basic operations are established,
reproving the full ladder would make use of our generic definition and lower
the workload.
......
......@@ -96,6 +96,8 @@ description of how verification of for loops are handled and the details of the
proof by reflections.
We described in the Conclusion (\sref{sec:Conclusion}) how our results can be
extended or reused in future works.
We added figures to provide a broader overview of how the proof are linked in
Section V, making it hopefully easier to follow.
\subsection{S\&P 2020 Review \#582B}
......@@ -198,12 +200,30 @@ whether this is careful quantification or not.
\subheading{Our answer}
Clarification in intro: VST has already been used to verify symmetric Cryptographic
primities, as mentioned later by \cite{Beringer2015VerifiedCA} and \cite{2015-Appel}.
primities (\eg SHA), as mentioned later by \cite{Beringer2015VerifiedCA}
and \cite{2015-Appel}.
We have not found errors in the implementation but we removed an undefined
We did not find errors in the implementation but we removed an undefined
behavior by the C standard.
p.1: SMT solvers are need of annotation, often written as parsable comment
in the middle of the C code~\cite{acsl} in order to ``guide'' the proof.
In our case we only need to anotate the beginning of the function and loop
invariants which allows us to get tighter bounds.
p.3: for IEEE we were limited to 18 pages including appendices.
We changed the format to a ``diff -u'' to provide the context of the applied changes.
p.5: We added the requested backward reference.
p.7: We added a clarification of what would be an unnecessary alliasing case.
Such case do not happen in TweetNaCl, it is therefore not required to write a
specification for it.
We removed some sections and added figures in section V to help the reader get a
better picture of the proof.
\todo{Verifiable Low F*}
\subsection{S\&P 2020 Review \#582C}
......@@ -294,3 +314,9 @@ Do you already prove such a property? More generally, what about the proof of
Section V is specific to X25519 and what is generic?
\subheading{Our answer}
In order to improve the reading experience, we removed the section of Reflections
which contained heavy proofs in Coq code. We also added figures in section V to
give a broader view of the High-level proof.
\todo{Reply constant time ? or in Conclusion ? Reply the clamping - reduction}
......@@ -475,3 +475,10 @@
publisher = {ACM},
note = {\url{https://eprint.iacr.org/2017/536.pdf}},
}
@misc{acsl,
title = {{ANSI/ISO C} Specification Language},
author = {Patrick Baudin and Pascal Cuoq and Jean-Christophe Filliâtre and Claude Marché and Benjamin Monate and Yannick Moy and Virgile Prevosto1},
year = {2019},
note = {\url{https://frama-c.com/download/acsl.pdf}}
}
Supports Markdown
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