Commit 45cc5f8b authored by Benoit Viguier's avatar Benoit Viguier
Browse files

more text

parent 075c3539
......@@ -7,7 +7,7 @@ well-marked appendices, and supplementary material."
+ 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.
- Add section in conclusion 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.\\
......@@ -18,14 +18,10 @@ curve448 (give reference) and X448.\\
+ 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:
......@@ -48,24 +44,15 @@ usually a lot of code details."\\
- "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?
at least, it did not work for me)"\\
+ @PETER ?
- "[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
......@@ -84,7 +71,7 @@ mostly from the big number computations.\\
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 ?
+ @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
......
......@@ -123,7 +123,7 @@ Finally in \sref{sec:Conclusion} we discuss the trusted code base of our proofs.
\end{figure}
\todoln{NEW}
In this figure, {\color{doc@lstfunctions}.V} represent the Coq files.
In this figure, {\color{doc@lstfunctions}.V} represent Coq files.
% Five years ago:
% \url{https://www.imperialviolet.org/2014/09/11/moveprovers.html}
......
......@@ -90,9 +90,9 @@ their respective bounds: arrays of 32 bytes.
The correctness of this specification is formally proven in Coq with
\coqe{Theorem body_crypto_scalarmult}.
\begin{sloppypar}
This specification (proven with VST) shows that \TNaCle{crypto_scalarmult} in C
\end{sloppypar}
% \begin{sloppypar}
% This specification (proven with VST) shows that \TNaCle{crypto_scalarmult} in C.
% \end{sloppypar}
% The Verifiable Software Toolchain uses a strongest postcondition strategy.
% The user must first write a formal specification of the function he wants to verify in Coq.
......@@ -143,5 +143,5 @@ we define an additional parameter $k$ with values in $\{0,1,2,3\}$:
\item else there is no aliasing.
\end{itemize}
In the proof of our specification, we do a case analysis over $k$ when needed.
This solution does not cover all cases (\eg all arguments are aliased) but it
is enough for our needs.
This solution does not generate all the possible cases of aliasing over 3 pointers
(\eg \texttt{o} = \texttt{a} = \texttt{b}) but it is enough to cover our needs.
......@@ -40,6 +40,16 @@ Lemma Crypto_Scalarmult_RFC_eq :
This proves that TweetNaCl's X25519 implementation respect RFC~7748.
\todo{add what can be reused here ?}
%% PREVIOUS TEXT BELOW.
% \subsection{Reflections, inversions and packing}
% \label{subsec:inversions-reflections}
%
......
......@@ -3,7 +3,7 @@
\subheading{Verified C Code} We provide below the code we verified.
\lstinputlisting[linerange={2-5,8-9,266-320,336-386,399-444},language=Ctweetnacl]{../proofs/vst/c/tweetnaclVerifiableC.c}
\lstinputlisting[linerange={2-5,8-9,266-317,333-380,393-438},language=Ctweetnacl]{../proofs/vst/c/tweetnaclVerifiableC.c}
\subheading{Diff from TweetNaCl} We provide below the diff between the original code of TweetNaCl and the code we verified.
......
......@@ -85,19 +85,14 @@
sv M(gf o,const gf a,const gf b)
{
@@ For-loop indexes have to be int.
@@ introduce an auxiliary variable to
@@ simplify verification (loop invariants).
- i64 i,j,t[31];
- FOR(i,31) t[i]=0;
- FOR(i,16) FOR(j,16) t[i+j]+=a[i]*b[j];
- FOR(i,15) t[i]+=38*t[i+16];
+ int i,j;
+ i64 t[31], aux;
+ i64 t[31];
+ FOR(i,31) t[i]= 0;
+ FOR(i,16) {
+ aux = a[i];
+ FOR(j,16) t[i+j]+=aux*b[j];
+ }
FOR(i,16) FOR(j,16) t[i+j]+=a[i]*b[j];
@@ Force the casting.
- FOR(i,15) t[i]+=38*t[i+16];
+ FOR(i,15) t[i]+=(i64)38*t[i+16];
FOR(i,16) o[i]=t[i];
car25519(o);
......
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