Commit 70243d3b authored by Benoit Viguier's avatar Benoit Viguier
Browse files

Add X448 extention text in Conclusion

parent 45cc5f8b
......@@ -7,17 +7,6 @@ well-marked appendices, and supplementary material."
+ the added confidence between in X25519 Correctness\\
+ proof of real world software\\
- 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.\\
+ 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.\\
- Changed made to TweetNaCl:\\
+ we contacted the authors.\\
+ only change made are the one required by VST\\
......
......@@ -29,5 +29,4 @@ 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
used in some of our more complex proofs (\ref{subsec:inversions-reflections}).
% Then, we describe efficient techniques used in some of our more complex proofs (\ref{subsec:inversions-reflections}).
\subsection{Number representation and C implementation}
\label{subsec:num-repr-rfc}
\todo{Do we completely rewrite this section?}
As described in \sref{subsec:Number-TweetNaCl}, numbers in \TNaCle{gf} are represented
in base $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,
......
......@@ -40,10 +40,6 @@ 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.
......
......@@ -26,16 +26,10 @@ Lemma f_ext: forall (A B:Type),
specification.
\item \textbf{CompCert}.
% The formally proven compiler.
% We trust that the CompCert Clight semantics in Coq
% correctly captures the C17 standard.
When compiling with CompCert we only need to trust CompCert's {assembly} semantics, because it has been formally proven correct.
However, when compiling with other C compilers like Clang or GCC, we need to trust that the CompCert's Clight semantics matches the C17 standard.
% as well as
% that the compiler will compile the TweetNaCl code according to that standard.
% Our proof also assumes that the TweetNaCl code will behave as expected if
% compiled under CompCert.
% We do not provide guarantees for other C compilers such as Clang or GCC.
When compiling with CompCert we only need to trust CompCert's {assembly}
semantics, because it has been formally proven correct.
However, when compiling with other C compilers like Clang or GCC, we need to
trust that the CompCert's Clight semantics matches the C17 standard.
\item \textbf{\texttt{clightgen}}. The tool making the translation from {C} to
{Clight}. It is the first step of the compilation.
......@@ -52,9 +46,7 @@ o[i] = aux1 + aux2;
factors out function calls and assignments from inside subexpressions.
The changes required for C code to make it verifiable are now minimal.
\item Finally,
% Last but not the least,
we must trust the \textbf{Coq kernel} and its
\item Finally, we must trust the \textbf{Coq kernel} and its
associated libraries; the \textbf{Ocaml compiler} on which we compiled Coq;
the \textbf{Ocaml Runtime} and the \textbf{CPU}. Those are common to all proofs
done with this architecture \cite{2015-Appel,coq-faq}.
......@@ -79,8 +71,25 @@ and thus solved this problem.
o[i]&=0xffff;
\end{lstlisting}
We believe that the type change of the loop index (\TNaCle{int} instead of \TNaCle{i64})
does not impact the trust of our proof.
We believe that type changes of loop indexes (\TNaCle{int} instead of \TNaCle{i64})
do not impact the trust of our proof.
We contacted the authors of TweetNaCl and believe that the changes above
mentionned will soon be integrated in a new version of the library.
\subheading{Extending our work.}
The high-level definition (\sref{sec:maths}) can easily be ported to any
other Montgomery curves and with it the proof of the ladder's correctness
assuming the same forumlas are used.
In addition to the curve equation, the field \F{p} would need to be redefined
as $p=2^{255}-19$ is hard-coded in order to speed up some proofs.
With respect to the C code verification (\sref{sec:C-Coq}),
\eg X448~\cite{cryptoeprint:2015:625,rfc7748} would require the adaptation most of the
low level arithmetic (mainly the multiplication, carry propagations and reductions).
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.
\subheading{A complete proof.}
We provide a mechanized formal proof of the correctness of the X25519
......
......@@ -361,6 +361,15 @@
note = {\url{https://coq.inria.fr/faq}},
}
@misc{cryptoeprint:2015:625,
author = {Mike Hamburg},
title = {Ed448-Goldilocks, a new elliptic curve},
howpublished = {Cryptology ePrint Archive, Report 2015/625},
year = {2015},
note = {\url{https://eprint.iacr.org/2015/625}},
}
@article{cryptoeprint:2017:212,
author = {Craig Costello and
Benjamin Smith},
......
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