Commit 294aac6e authored by Benoit Viguier's avatar Benoit Viguier
Browse files

small fixes + add lines numbers

parent 66856523
......@@ -37,9 +37,9 @@ In the second step we prove equivalence of the C implementation of X25519
to our RFC formalization.
This part of the proof uses the Verifiable Software Toolchain (VST)~\cite{2012-Appel}
to establish a link between C and Coq.
VST uses Separation logic~\cite{1969-Hoare,Reynolds02separationlogic}
The VST uses separation logic~\cite{1969-Hoare,Reynolds02separationlogic}
to show that the semantics of the program satisfy a functional specification in Coq.
To the best of our knowledge, this is the first time that
To the best of our knowledge, this is the first time that the
VST is used in the formal proof of correctness of an implementation
of an asymmetric cryptographic primitive.
......@@ -100,7 +100,7 @@ We only need to anotate the specifications and loop invariants.
\subheading{Reproducing the proofs.}
To maximize reusability of our results we placed the code of our formal proof
presented in this paper into the public domain.
It is available at \url{https://cdn-09.anonfile.com/6fp8ta70n9/014c4f8c-1569921449/coq-verif-tweetnacl.tar.gz}
It is available at \todo{FIX ME: https://cdn-09.anonfile.com/6fp8ta70n9/014c4f8c-1569921449/coq-verif-tweetnacl.tar.gz}
with instructions of how to compile and verify our proof.
A description of the content of the code archive is provided in
Appendix~\ref{appendix:proof-folders}.
......
......@@ -39,7 +39,7 @@ Lemma Crypto_Scalarmult_RFC_eq :
\end{lstlisting}
This proves that TweetNaCl's X25519 implementation respect RFC~7748.
\todo{fix ``This''}
%% PREVIOUS TEXT BELOW.
......
......@@ -278,8 +278,9 @@ differential additions and point doublings using projective coordinates.
\subsubsection{Scalar multiplication algorithms}
\label{subsec:ECC-ladder}
By taking \aref{alg:montgomery-ladder} and replacing \texttt{xDBL} and \texttt{xADD}
with their respective formula (\lref{lemma:xADD} and \lref{lemma:xDBL}),
with their respective formulae (\lref{lemma:xADD} and \lref{lemma:xDBL}),
we define a ladder \coqe{opt_montgomery} (in which $\K$ has not been fixed yet),
similar to the one used in
TweetNaCl.
......
......@@ -31,6 +31,7 @@ Lemma f_ext: forall (A B:Type),
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.
\todo{FIXME}
\item \textbf{\texttt{clightgen}}. The tool making the translation from {C} to
{Clight}. It is the first step of the compilation.
VST does not support the direct verification of \texttt{o[i] = a[i] + b[i]}.
......@@ -73,7 +74,7 @@ o[i]&=0xffff;
Aside from the modifications above mentioned, all subsequent alteration
---such as the type change of loop indexes (\TNaCle{int} instead of \TNaCle{i64})---
were required for VST to parse properly the code. We believe those
were required for VST to parse the code properly. We believe those
adjustments do not impact the trust of our proof.
We contacted the authors of TweetNaCl and expect that the changes above
......@@ -87,7 +88,7 @@ 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}), the extension of
the verification effort to Ed25519 would makes directly use of the low level
the verification effort to Ed25519 would make directly use of the low level
arithmetic. The ladder steps formula being different this would require a high
level verification similar to \tref{thm:montgomery-ladder-correct}.
......
\documentclass[format=sigconf, anonymous=false, authordraft=false, screen=true, review=true]{acmart}
\newif\ifusenix
\usenixfalse
\usepackage{setup}
......
% \input{_acmccs}
\newif\ifusenix
\newif\ifpublic
\usenixtrue
\publicfalse
\ifusenix
\input{_usenix}
\else
\input{_acmccs}
\fi
% \begin{acks}
% This work would not have been possible without the assistance of multiple people.
......
......@@ -50,14 +50,16 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[letterpaper,twocolumn,10pt]{article}
\newif\ifusenix
\usenixtrue
\usepackage{usenix2019_v3}
\usepackage{setup}
\input{_macros}
\ifpublic
\else
\linenumbers
\fi
%-------------------------------------------------------------------------------
\begin{document}
......@@ -71,6 +73,7 @@
%for single author (just remove % characters)
\ifpublic
\author{
{\rm Peter Schwabe}
Radboud University,\\
......@@ -87,7 +90,9 @@ The Netherlands
{\rm Freek Wiedijk}
Radboud University,\\
The Netherlands
}
}\else
\author{}
\fi
\maketitle
\input{_abstract}
This diff is collapsed.
......@@ -22,6 +22,11 @@
\usepackage{tikz}
\usetikzlibrary{arrows}
\ifusenix
\usepackage[switch]{lineno}
\renewcommand{\linenumberfont}{\normalfont\footnotesize\color{red}}
\else
\fi
% \definecolor{linkcolor}{rgb}{0.65,0,0}
% \definecolor{citecolor}{rgb}{0,0.45,0}
% \definecolor{urlcolor}{rgb}{0,0,0.65}
......
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