Commit 50866c6b authored by Benoit Viguier's avatar Benoit Viguier
Browse files

add todos

parent 4c0a09fc
\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\\
- Add section to describe what would need to be done to adapt the code for e.g.
curve448 (give reference) and X448.\\
+ we can reuse the code of the elliptic abstraction.\\
+ the ladder would need few adaptation with respect to the bound propagations.\\
+ the ladder is generic so can be easily instanciated over \F{2^{448} - 2^{224}
- 1}.\\
+ the Addition and subtraction are simple and bounds carries easily.\\
+ Multiplication needs to be redefined.\\
+ Squaring can be easily ported.\\
+ Inversion is easily ported with the use of reflections, idem for the packing.\\
- Remove reflection section.\\
+ simplify writting.\\
+ Still mention reflection but don't describe more than that.\\
- Changed made to TweetNaCl:\\
+ we contacted the authors.\\
+ only change made are the one required by VST\\
+ Should have a look at the Multiplication}
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.
- "In particular,
the Figure seems to used a nice abstraction of properties that is not
used elsewhere in the paper. I.e., elsewhere in the paper, there is
usually a lot of code details."\\
+ I don't know what to do on that one.
- "the discussion of the computation of n’ was completely unclear to me."\\
+ describe the process of clamping better.
- "Instead, Appendix A just contains a Diff, and as a reader, I
would need to perform the extraction of insights myself."\\
+ => changed the Appendix A format to diff -u to give more context
- "Maybe use a backward reference to p.3 where
CSWAP was defined, since in between, there was a lot of content,
and relying on the reader’s memory does not really work here (or
at least, it did not work for me)"
- "all cases of what? And why is this distinction sufficient for
the task at hand?"\\
+ remove the sentence or show by example which aliasing case is not needed?
- "[13], the order of authors is different than in the original publication."\\
- "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*",\\
+ \strikethrough{fixed authors order}.\\
+ 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."\\
+ 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 ?
}
......@@ -122,6 +122,8 @@ Finally in \sref{sec:Conclusion} we discuss the trusted code base of our proofs.
\label{tikz:ProofOverview}
\end{figure}
\todoln{NEW}
In this figure, {\color{doc@lstfunctions}.V} represent the Coq files.
% Five years ago:
% \url{https://www.imperialviolet.org/2014/09/11/moveprovers.html}
......
......@@ -28,13 +28,16 @@ Theorem body_crypto_scalarmult:
Using our formalization of RFC~7748 (\sref{sec:Coq-RFC}) we specify the Hoare
triple before proving its correctness with the VST (\ref{subsec:with-VST}).
We provide an example of equivalence of operations over different number
representations (\ref{subsec:num-repr-rfc}). Then, we describe efficient techniques
representations (\ref{subsec:num-repr-rfc}).
Then, we describe efficient techniques
used in some of our more complex proofs (\ref{subsec:inversions-reflections}).
\subsection{Applying the Verifiable Software Toolchain}
\label{subsec:with-VST}
\todo{Fix bleeding}
We now turn our focus to the formal specification of \TNaCle{crypto_scalarmult}.
We use our definition of X25519 from the RFC in the Hoare triple and prove
its correctness.
......@@ -122,6 +125,8 @@ their respective bounds: arrays of 32 bytes.
The correctness of this specification is formally proven in Coq with
\coqe{Theorem body_crypto_scalarmult}.
\todo{Fix bleeding}
This specification (proven with VST) shows that \TNaCle{crypto_scalarmult} in C
% The Verifiable Software Toolchain uses a strongest postcondition strategy.
......
%XXX-Peter: shouldn't verifying fixed-length for loops be rather standard?
%XXX Benoit: it is simple if the argument is increasing or if the "recursive call"
% is made before the computations.
% This is not the case here: you compute idx 255 before 254...
% Can we shorten the next paragraph?
\subheading{Verifying \texttt{for} loops.}
Final states of \texttt{for} loops are usually computed by simple recursive functions.
However, we must define invariants which are true for each iteration step.
Assume that we want to prove a decreasing loop where indexes go from 3 to 0.
Define a function $g : \N \rightarrow State \rightarrow State $ which takes as
input an integer for the index and a state, then returns a state.
It simulates the body of the \texttt{for} loop.
Define the recursion: $f : \N \rightarrow State \rightarrow State $ which
iteratively applies $g$ with decreasing index:
\begin{equation*}
f ( i , s ) =
\begin{cases}
s & \text{if } s = 0 \\
f( i - 1 , g ( i - 1 , s )) & \text{otherwise}
\end{cases}
\end{equation*}
Then we have:
\begin{align*}
f(4,s) &= g(0,g(1,g(2,g(3,s))))
\end{align*}
To prove the correctness of $f(4,s)$, we need to prove that intermediate steps
$g(3,s)$; $g(2,g(3,s))$; $g(1,g(2,g(3,s)))$; $g(0,g(1,g(2,g(3,s))))$ are correct.
Due to the computation order of recursive function, our loop invariant for
$i\in\{0,1,2,3,4\}$ cannot use $f(i)$.
To solve this, we define an auxiliary function with an accumulator such that
given $i\in\{0,1,2,3,4\}$, it will compute the first $i$ steps of the loop.
We then prove for the complete number of steps, the function with the accumulator
and without returns the same result.
We formalized this result in a generic way in Appendix~\ref{subsubsec:for}.
Using this formalization, we prove that the 255 steps of the Montgomery ladder
in C provide the same computations as in \coqe{RFC}.
% %
% %XXX-Peter: shouldn't verifying fixed-length for loops be rather standard?
% %XXX Benoit: it is simple if the argument is increasing or if the "recursive call"
% % is made before the computations.
% % This is not the case here: you compute idx 255 before 254...
%
% % Can we shorten the next paragraph?
% \subheading{Verifying \texttt{for} loops.}
% Final states of \texttt{for} loops are usually computed by simple recursive functions.
% However, we must define invariants which are true for each iteration step.
%
% Assume that we want to prove a decreasing loop where indexes go from 3 to 0.
% Define a function $g : \N \rightarrow State \rightarrow State $ which takes as
% input an integer for the index and a state, then returns a state.
% It simulates the body of the \texttt{for} loop.
% Define the recursion: $f : \N \rightarrow State \rightarrow State $ which
% iteratively applies $g$ with decreasing index:
% \begin{equation*}
% f ( i , s ) =
% \begin{cases}
% s & \text{if } s = 0 \\
% f( i - 1 , g ( i - 1 , s )) & \text{otherwise}
% \end{cases}
% \end{equation*}
% Then we have:
% \begin{align*}
% f(4,s) &= g(0,g(1,g(2,g(3,s))))
% \end{align*}
% To prove the correctness of $f(4,s)$, we need to prove that intermediate steps
% $g(3,s)$; $g(2,g(3,s))$; $g(1,g(2,g(3,s)))$; $g(0,g(1,g(2,g(3,s))))$ are correct.
% Due to the computation order of recursive function, our loop invariant for
% $i\in\{0,1,2,3,4\}$ cannot use $f(i)$.
% To solve this, we define an auxiliary function with an accumulator such that
% given $i\in\{0,1,2,3,4\}$, it will compute the first $i$ steps of the loop.
%
% We then prove for the complete number of steps, the function with the accumulator
% and without returns the same result.
% We formalized this result in a generic way in Appendix~\ref{subsubsec:for}.
%
% Using this formalization, we prove that the 255 steps of the Montgomery ladder
% in C provide the same computations as in \coqe{RFC}.
% % %
......@@ -276,62 +276,9 @@ TweetNaCl.
This definition is closely related to \coqe{montgomery_rec} that was used
in the definition of \coqe{RFC}, and is easily proved to correspond to it.
In Coq this correspondence proof is hidden in the proof of \coqe{RFC_Correct} shown above.
%\ref to the def of montgomery_rec? relevant lemma(s) that show(s) these are "the same"?
We prove its correctness for any point whose \xcoord is not 0.
% By taking \aref{alg:montgomery-ladder} and replacing \texttt{xDBL} and \texttt{xADD}
% with their respective formula (\lref{lemma:xADD} and \lref{lemma:xDBL}),
% we can define a ladder similar to the one used in TweetNaCl (See \aref{alg:montgomery-double-add}).
%
% \begin{algorithm}
% \caption{Montgomery ladder for scalar multiplication on $M_{a,b}(\K)$ with optimizations}
% \label{alg:montgomery-double-add}
% \begin{algorithmic}
% \REQUIRE{$x \in \K\backslash \{0\}$, scalars $n$ and $m$, $n < 2^m$}
% \ENSURE{$a/c = \chi_0(n \cdot P)$ for any $P$ such that $\chi_0(P) = x$}
% \STATE $(a,c) \leftarrow (1,0)$ ~~~~~~~~~~~~~~~{\color{gray}\textit{$\chi_0(\Oinf) = (1:0)$}}
% \STATE $(b,d) \leftarrow (x,1)$ ~~~~~~~~~~~~~~~{\color{gray}\textit{$\chi_0(P) = (x:1)$}}
% \FOR{$k$ := $m$ \textbf{downto} $1$}
% \IF{$k^{\text{th}}$ bit of $n$ is $1$}
% \STATE $(a,b) \leftarrow (b,a)$
% \STATE $(c,d) \leftarrow (d,c)$
% \ENDIF
% \STATE $e \leftarrow a + c$
% \STATE $a \leftarrow a - c$
% \STATE $c \leftarrow b + d$
% \STATE $b \leftarrow b - d$
% \STATE $d \leftarrow e^2$
% \STATE $f \leftarrow a^2$
% \STATE $a \leftarrow c \times a$
% \STATE $c \leftarrow b \times e$
% \STATE $e \leftarrow a + c$
% \STATE $a \leftarrow a - c$
% \STATE $b \leftarrow a^2$
% \STATE $c \leftarrow d-f$
% \STATE $a \leftarrow c\times\frac{A - 2}{4}$
% \STATE $a \leftarrow a + d$
% \STATE $c \leftarrow c \times a$
% \STATE $a \leftarrow d \times f$
% \STATE $d \leftarrow b \times x$
% \STATE $b \leftarrow e^2$
% \IF{$k^{\text{th}}$ bit of $n$ is $1$}
% \STATE $(a,b) \leftarrow (b,a)$
% \STATE $(c,d) \leftarrow (d,c)$
% \ENDIF
% \ENDFOR
% \end{algorithmic}
% \end{algorithm}
%
% \begin{lemma}
% \label{lemma:montgomery-double-add}
% \aref{alg:montgomery-double-add} is correct, \ie it respects its output
% conditions given the input conditions.
% \end{lemma}
% We formalized \lref{lemma:montgomery-double-add} as follows:
\begin{lstlisting}[language=Coq]
Lemma opt_montgomery_x :
forall (n m : nat) (x : K),
......@@ -345,8 +292,6 @@ Lemma opt_montgomery_0:
forall (n m : nat), opt_montgomery n m 0 = 0.
\end{lstlisting}
Also \Oinf\ is the neutral element of $M_{a,b}(\K)$.
%$$\forall P, P + \Oinf\ = P$$
%thus we derive the following lemma.
\begin{lstlisting}[language=Coq]
Lemma p_x0_0_eq_0 : forall (n : nat) (p : mc M),
p #x0 = 0%:R -> (p *+ n) #x0 = 0%R.
......@@ -373,8 +318,10 @@ There always exists $x \in \F{p^2}$ such that $x^2 = a^2-4$,
preventing the use \tref{thm:montgomery-ladder-correct}
with $\K = \F{p^2}$.
We first study Curve25519 and one of its quadratic twists Twist25519, both defined
over \F{p}.
\todo{Fix bleeding}
We first study Curve25519 and one of its quadratic twists Twist25519,
both defined over \F{p}.
\subsubsection{Curves and twists}
\label{subsec:Zmodp}
......
......@@ -81,7 +81,7 @@ On page 9: "each functions" => no s
\subheading{Our answer}
XXX:TODO
\todoln{New stuff}
We corrected the typos. There are no new proof techniques in the case of this
verification. We used reflections techniques to generically solve some of our
goals such as the proof of inversion.
......@@ -184,9 +184,11 @@ whether this is careful quantification or not.
\subheading{Our answer}
\todoln{New stuff}
Clarification in intro: VST has already been used to verify symmetric Cryptographic
primities, as mentioned later by \cite{Beringer2015VerifiedCA} and \cite{2015-Appel}.
\subsection{S\&P 2020 Review \#582C}
Overall merit: 3. Weak reject - The paper has flaws, but I will not argue against it.
......@@ -273,3 +275,7 @@ proofs in any way? Is there a stronger property you could prove because of the
clamping (e.g. membership in the prime-order group)?
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}
\todoln{New stuff}
@STRING{LNCS = {LNCS}}
@STRING{SV = {Springer}}
@article{1969-Hoare,
author = {C. A. R. Hoare},
title = {An Axiomatic Basis for Computer Programming},
journal = {Commun. ACM},
publisher = {ACM},
year = {1969},
volume = {12},
number = {10},
year = {1969},
pages = {576-580},
note = {\url{http://doi.acm.org/10.1145/363235.363259}},
_publisher = {ACM},
}
@article{2007-Blazy-C-chronique,
author = {Sandrine Blazy},
title = {Comment gagner confiance en {C} ?},
journal = {Technique et Science Informatiques},
publisher = {Lavoisier},
year = {2007},
volume = {26},
number = {9},
year = {2007},
pages = {1195-1200},
note = {\url{http://hal.inria.fr/inria-00292049/}},
_publisher = {Lavoisier},
}
@inproceedings{2012-Appel,
author = {Andrew W. Appel},
title = {Verified Software Toolchain},
booktitle = {{NASA} Formal Methods - 4th International Symposium, {NFM} 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings},
year = {2012},
editor = {Alwyn Goodloe and Suzette Person},
publisher = SV,
series = LNCS,
volume = {7226},
year = {2012},
series = LNCS,
pages = {2},
publisher = SV,
note = {\url{https://doi.org/10.1007/978-3-642-28891-3_2}},
}
......@@ -43,51 +47,63 @@
author = {Andrew W. Appel},
title = {Verification of a Cryptographic Primitive: {SHA-256}},
journal = {{ACM} Transactions on Programming Languages and Systems},
publisher = {ACM},
year = {2015},
volume = {37},
number = {2},
year = {2015},
pages = {7:1--7:31},
note = {\url{http://doi.acm.org/10.1145/2701415}},
_publisher = {ACM},
}
@inproceedings{BGJ+15,
author = {Daniel J. Bernstein and Bernard van Gastel and Wesley Janssen and Tanja Lange and
Peter Schwabe and Sjaak Smetsers},
author = {Daniel J. Bernstein and
Bernard van Gastel and
Wesley Janssen and
Tanja Lange and
Peter Schwabe and
Sjaak Smetsers},
title = {{TweetNaCl}: A crypto library in 100 tweets},
booktitle = {Progress in Cryptology -- {LATINCRYPT 2014}},
year = {2015},
editor = {Diego Aranha and Alfred Menezes},
publisher = SV,
series = LNCS,
volume = {8895},
year = {2015},
series = LNCS,
pages = {64--83},
publisher = SV,
note = {\url{http://cryptojedi.org/papers/\#tweetnacl}},
}
@inproceedings{BLS12,
author = {Daniel J. Bernstein and Tanja Lange and Peter Schwabe},
author = {Daniel J. Bernstein and
Tanja Lange and
Peter Schwabe},
title = {The security impact of a new cryptographic library},
booktitle = {Progress in Cryptology -- {LATINCRYPT 2012}},
year = {2012},
editor = {Alejandro Hevia and Gregory Neven},
publisher = SV,
series = LNCS,
volume = {7533},
year = {2012},
series = LNCS,
pages = {159--176},
publisher = SV,
note = {\url{http://cryptojedi.org/papers/\#coolnacl}},
}
@inproceedings{BartziaS14,
author = {Evmorfia-Iro Bartzia and Pierre-Yves Strub},
author = {Evmorfia-Iro Bartzia and
Pierre-Yves Strub},
title = {A Formal Library for Elliptic Curves in the {Coq} Proof Assistant},
booktitle = {Interactive Theorem Proving},
year = {2014},
editor = {Gerwin Klein and Ruben Gamboa},
publisher = SV,
series = LNCS,
volume = {8558},
year = {2014},
series = LNCS,
pages = {77--92},
publisher = SV,
note = {\url{https://hal.inria.fr/hal-01102288}},
}
......@@ -95,16 +111,18 @@
author = {Daniel J. Bernstein},
title = {Curve25519: new {D}iffie-{H}ellman speed records},
booktitle = {Public Key Cryptography -- {PKC 2006}},
year = {2006},
editor = {Moti Yung and Yevgeniy Dodis and Aggelos Kiayias and Tal Malkin},
publisher = SV,
series = LNCS,
volume = {3958},
year = {2006},
series = LNCS,
pages = {207--228},
publisher = SV,
note = {\url{http://cr.yp.to/papers.html\#curve25519}},
}
@misc{Ber14,
author = {Daniel J. Bernstein},
title = {25519 naming},
howpublished = {Posting to the CFRG mailing list},
......@@ -114,35 +132,49 @@
}
@inproceedings{Beringer2015VerifiedCA,
author = {Lennart Beringer and Adam Petcher and Katherine Q. Ye and Andrew W. Appel},
author = {Lennart Beringer and
Adam Petcher and
Katherine Q. Ye and
Andrew W. Appel},
title = {Verified Correctness and Security of {OpenSSL} {HMAC}},
booktitle = {Proceedings of the 24th {USENIX} Security Symposium},
publisher = {{USENIX} Association},
year = {2015},
pages = {207--221},
publisher = {{USENIX} Association},
note = {\url{https://www.cs.cmu.edu/~kqy/resources/verified-hmac.pdf}},
}
@article{Blazy-Leroy-Clight-09,
author = {Sandrine Blazy and Xavier Leroy},
author = {Sandrine Blazy and
Xavier Leroy},
title = {Mechanized semantics for the {Clight} subset of the {C} language},
journal = {Journal of Automated Reasoning},
publisher = SV,
year = {2009},
volume = {43},
number = {3},
year = {2009},
pages = {263-288},
note = {\url{http://gallium.inria.fr/~xleroy/publi/Clight.pdf}},
_publisher = SV,
}
@inproceedings{Chen2014VerifyingCS,
author = {Yu-Fang Chen and Chang-Hong Hsu and Hsin-Hung Lin and Peter Schwabe and
Ming-Hsien Tsai and Bow-Yaw Wang and Bo-Yin Yang and Shang-Yi Yang},
author = {Yu-Fang Chen and
Chang-Hong Hsu and
Hsin-Hung Lin and
Peter Schwabe and
Ming-Hsien Tsai and
Bow-Yaw Wang and
Bo-Yin Yang and
Shang-Yi Yang},
title = {Verifying {Curve25519} Software},
booktitle = {Proceedings of the 2014 {ACM} {SIGSAC} Conference on Computer and Communications Security},
publisher = {ACM},
year = {2014},
pages = {299--309},
publisher = {ACM},
note = {\url{https://cryptojedi.org/papers/\#verify25519.pdf}},
}
......@@ -150,32 +182,56 @@
author = {Adam Chlipala},
title = {An Introduction to Programming and Proving with Dependent Types in {Coq}},
journal = {Journal of Formalized Reasoning},
publisher = {University of Bologna},
year = {2010},
volume = {3(2)},
pages = {1-93},
note = {\url{http://adam.chlipala.net/papers/CpdtJFR/}},
_publisher = {University of Bologna},
}
@inproceedings{DBLP:journals/corr/BhargavanDFHPRR17,
author = {Karthikeyan Bhargavan and Antoine Delignat{-}Lavaud and C{\'{e}}dric Fournet and Catalin Hritcu and
Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and
Peng Wang and Santiago Zanella B{\'{e}}guelin and Jean Karim Zinzindohou{\'{e}}},
author = {Jonathan Protzenko and
Jean-Karim Zinzindohou{\'{e}} and
Aseem Rastogi and
Tahina Ramananandro and
Peng Wang and
Santiago Zanella-B{\'{e}}guelin and
Antoine Delignat{-}Lavaud and
Catalin Hritcu and
Karthikeyan Bhargavan and
C{\'{e}}dric Fournet and
Nikhil Swamy},
title = {Verified Low-Level Programming Embedded in {F*}},
booktitle = {Proceedings of the {ACM} on Programming Languages},
publisher = {ACM},
year = {2017},
volume = {1},
number = {ICFP},
year = {2017},
pages = {17},
publisher = {ACM},
note = {\url{http://arxiv.org/abs/1703.00053}},
}
@misc{Erbsen2016SystematicSO,
author = {Andres Erbsen and
Jade Philipoom and
Jason Gross and
Rober Sloan and
Adam Chlipala},
title = {Systematic Synthesis of Elliptic Curve Cryptography Implementations},
year = {2016},
note = {\url{https://people.csail.mit.edu/jgross/personal-website/papers/2017-fiat-crypto-pldi-draft.pdf}},
}
@mastersthesis{Erbsen2017CraftingCE,
author = {Andres Erbsen},
title = {Crafting certified elliptic curve cryptography implementations in {Coq}},
school = {Massachusetts Institute of Technology},
year = {2017},
note = {\url{http://adam.chlipala.net/theses/andreser_meng.pdf}},
}
......@@ -183,14 +239,16 @@
author = {W. A. Howard},
title = {The Formul\ae-as-Types Notion of Construction},
booktitle = {The Curry-Howard Isomorphism},
editor = {Philippe De Groote},
publisher = {Academia},
year = {1995},
editor = {Philippe De Groote},
note = {\url{https://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf}},
}
@manual{ISO:C17,
title = {ISO C Standard 2017},
author = {ISO},
year = {2018},
note = {\url{https://www.iso.org/standard/74528.html}},
......@@ -198,6 +256,7 @@
@manual{ISO:C99,
title = {ISO C Standard 1999},
author = {ISO},