Commit 0ad87b8c authored by Benoit Viguier's avatar Benoit Viguier
Browse files

sed 's/the VST/VST/g' :)

parent f710e68c
......@@ -39,7 +39,7 @@ This part of the proof uses the Verifiable Software Toolchain (VST)~\cite{2012-A
to establish a link between C and Coq.
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 the VST
To the best of our knowledge, this is the first time that VST
is used in the formal proof of correctness of an implementation
of an asymmetric cryptographic primitive.
......
......@@ -14,7 +14,7 @@ typedef long long i64;
TweetNaCl functions take pointers as arguments. By convention the first one
points to the output array \texttt{o}. It is then followed by the input arguments.
Due to some limitations of the VST, indexes used in \TNaCle{for} loops have to be
Due to some limitations of VST, indexes used in \TNaCle{for} loops have to be
of type \TNaCle{int} instead of \TNaCle{i64}. We changed the code to allow our
proofs to carry through. We believe this does not affect the correctness of the
original code. A complete diff of our modifications to TweetNaCl can be found in
......
\subsection{Coq, separation logic, and the VST}
\subsection{Coq, separation logic, and VST}
\label{subsec:Coq-VST}
Coq~\cite{coq-faq} is an interactive theorem prover based on type theory. It
......@@ -39,6 +39,6 @@ The first step consists of translating the source code into Clight,
an intermediate representation used by CompCert.
For such purpose one uses the parser of CompCert called \texttt{clightgen}.
In a second step one defines the Hoare triple representing the specification of
the piece of software one wants to prove. Then using the VST, one uses a strongest
the piece of software one wants to prove. Then using VST, one uses a strongest
postcondition approach to prove the correctness of the triple.
This can be seen as a forward symbolic execution of the program.
......@@ -26,7 +26,7 @@ Theorem body_crypto_scalarmult:
% We first describe the global structure of our proof (\ref{subsec:proof-structure}).
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}).
triple before proving its correctness with 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}).
......@@ -116,12 +116,12 @@ In other words,
we only prove correctness of \TNaCle{crypto_scalarmult} when it is called without aliasing.
But for other TweetNaCl functions, like the multiplication function \texttt{M(o,a,b)}, we cannot ignore aliasing, as it is called in the ladder in an aliased manner.
In the VST, a simple specification of this function will assume that the pointer arguments
In VST, a simple specification of this function will assume that the pointer arguments
point to non-overlapping space in memory.
When called with three memory fragments (\texttt{o, a, b}),
the three of them will be consumed. However assuming this naive specification
when \texttt{M(o,a,a)} is called (squaring), the first two memory areas (\texttt{o, a})
are consumed and the VST will expect a third memory section (\texttt{a}) which does not \emph{exist} anymore.
are consumed and VST will expect a third memory section (\texttt{a}) which does not \emph{exist} anymore.
Examples of such cases are illustrated in \fref{tikz:MemSame}.
\begin{figure}[h]%
\centering%
......
......@@ -32,7 +32,7 @@ Lemma f_ext: forall (A B:Type),
\item \textbf{\texttt{clightgen}}. The tool making the translation from {C} to
{Clight}, the first step of the CompCert compilation.
The VST does not support the direct verification of \texttt{o[i] = a[i] + b[i]}.
VST does not support the direct verification of \texttt{o[i] = a[i] + b[i]}.
This needs to be rewritten into:
\begin{lstlisting}[language=Ctweetnacl,stepnumber=0,belowskip=-0.5 \baselineskip]
aux1 = a[i]; aux2 = b[i];
......@@ -83,7 +83,7 @@ above will soon be integrated in a new version of the library.
% \subheading{Verification Effort.}
% In addition to the time required to get familiar with
% research software, we faced a few bugs which we reported
% to the developers of the VST to get them fixed.
% to the developers of VST to get them fixed.
% It is very hard to work with a tool without being involved
% in the development loop. Additionally newer versions often
% broke some of our proofs and it was often needed to adapt
......
......@@ -12,12 +12,12 @@
As follow, we provide the explanations of the above changes to TweetNaCl's code.
\begin{itemize}
\item lines 7-8: We tell the VST that \TNaCle{long long} are
\item lines 7-8: We tell VST that \TNaCle{long long} are
aligned on 8 bytes.
\item lines 16-23: We remove the the undefined behavior as explained in \sref{sec:Conclusion}.
\item lines 29-31; lines 60-62: The VST does not support \TNaCle{for} loops over \TNaCle{i64}, we convert it into an \TNaCle{int}.
\item lines 29-31; lines 60-62: VST does not support \TNaCle{for} loops over \TNaCle{i64}, we convert it into an \TNaCle{int}.
\item lines 39 \& 41: We Initialize \TNaCle{m} with \TNaCle{0}.
This change allows us to prove the functional correctness of \TNaCle{pack25519} without having to deal with an array containing
......@@ -26,13 +26,13 @@ As follow, we provide the explanations of the above changes to TweetNaCl's code.
\item lines 40 \& 42; lines 70 \& 71: We replace the \TNaCle{FOR} loop by \TNaCle{set25519}. The code is the same once the function is inlined. This small change is purely cosmetic but stays in the spirit of tweetnacl: keeping a small code size while being auditable.
\item lines 50-52: the VST does not allow computation in the argument before a function call. Additionally \texttt{clightgen} does not extract the computation either. We add this small step to allow the VST to carry through the proof.
\item lines 50-52: VST does not allow computation in the argument before a function call. Additionally \texttt{clightgen} does not extract the computation either. We add this small step to allow VST to carry through the proof.
% \item lines 60-62: The VST does not support \TNaCle{for} loops over \TNaCle{i64}, we convert it into an \TNaCle{int}.
% \item lines 60-62: VST does not support \TNaCle{for} loops over \TNaCle{i64}, we convert it into an \TNaCle{int}.
% \item lines 70-71: We replace \TNaCle{FOR(a,16) c[a]=i[a];} by \TNaCle{set25519(c,i);}. The semantic of operation done is the same once \TNaCle{set25519} is inlined. This small change is purely cosmetic but stays in the spirit of tweetnacl: keeping a small code size while being auditable.
\item lines 79-82: The VST does not support \TNaCle{for} loops over \TNaCle{i64}, we convert it into an \TNaCle{int}.\\
\item lines 79-82: VST does not support \TNaCle{for} loops over \TNaCle{i64}, we convert it into an \TNaCle{int}.\\
In the function calls of \TNaCle{sel25519}, the specifications requires the use of \TNaCle{int}, the value of \TNaCle{r} being either \TNaCle{0} or \TNaCle{1}, we consider this change safe.
\item Lines 90-101: The \TNaCle{for} loop does not add any benefits to the code. By removing it we simplify the source and the verification steps as we do not need to deal with pointer arithmetic. As a result, \TNaCle{x} can be limited to only 16 \TNaCle{i64}, \ie \TNaCle{gf}.
......
......@@ -94,7 +94,7 @@ become stronger.
\begin{answer}{EEEEEE}
The switch from \TNaCle{i64} to \TNaCle{int} in \texttt{for} loops and the
extraction of the computation outside of the function call in
\TNaCle{pack25519} are required by the VST but we believe those
\TNaCle{pack25519} are required by VST but we believe those
change have no impact on the verification effort.
The only modification which made the verification easier
......@@ -110,7 +110,7 @@ effort: person month etc.
\begin{answer}{EEEEEE}
In addition to the time required to get familiar with
research software, we faced a few bugs which we reported
to the developers of the VST to get them fixed.
to the developers of VST to get them fixed.
It is very hard to work with a tool without being involved
in the development loop. Additionally newer versions often
broke some of our proofs and it was often needed to adapt
......@@ -343,7 +343,7 @@ and our approach.
\begin{figure}[H]
\centering
\include{tikz/low}
\caption{The VST vs Low*}
\caption{VST vs Low*}
\label{tikz:LowVST}
\end{figure}
......@@ -351,10 +351,10 @@ Low* generates C code, thus this is synthesis. We generate
Clight from C code, thus this is verification. Because Low*
also has a verification step with respect to some high-level
specifications, we consider their process to be a mix of the
two methods. Also to be noted that both the VST and Low*
two methods. Also to be noted that both VST and Low*
allow the verification of memory safety.
% However Low* provides
% sidechannel securities while the VST allow verification
% sidechannel securities while VST allow verification
% of concurent programs.
\end{answer}
......@@ -368,7 +368,7 @@ for symmetric cryptographic primitives before? From the text,
I wasn’t sure whether this is careful quantification or not.
\begin{answer}{EEEEEE}
This is indeed careful quantification. The VST has already
This is indeed careful quantification. VST has already
been used to verify symmetric Cryptographic primitives
(\eg SHA), as mentioned later by \cite{Beringer2015VerifiedCA} and \cite{2015-Appel}.
\end{answer}
......@@ -486,7 +486,7 @@ to share proof effort across multiple curves.
\begin{answer}{EEEEEE}
We added insights in \sref{subsec:with-VST} of how to improve
working with the VST verification framework. In section \sref{sec:Conclusion},
working with VST. In section \sref{sec:Conclusion},
we described in further details how our work can
be extended to other curves. The TweetNaCl ed25519
implementation makes use of the same low level arithmetic
......@@ -505,7 +505,7 @@ guarantees of the TweetNaCl code. Could this be done
in their framework?
\begin{answer}{EEEEEE}
Constant-timeness is not a property verifiable with the VST.
Constant-timeness is not a property verifiable with VST.
This is not verifiable with our framework.
% Related on CompCert: https://eprint.iacr.org/2019/926.pdf
\end{answer}
......
......@@ -42,7 +42,7 @@
% We define a mid-level specification by instantiating the ladder over $\Zfield$.
% Additionally we also provide a low-level specification close to the \texttt{C} code
% (over lists of $\Z$). We show this specification to be equivalent to the
% \emph{semantic version} of C (Clight) using the VST.
% \emph{semantic version} of C (Clight) using VST.
% This low level specification gives us the soundness assurance.
%
% RFC~7748's X25519 formalization (\sref{sec:Coq-RFC}) takes as input list of $\Z$.
......
......@@ -76,7 +76,7 @@
% We define a mid-level specification by instantiating the ladder over $\Zfield$.
% Additionally we also provide a low-level specification close to the \texttt{C} code
% (over lists of $\Z$). We show this specification to be equivalent to the
% \emph{semantic version} of C (Clight) using the VST.
% \emph{semantic version} of C (Clight) using VST.
% This low level specification gives us the soundness assurance.
%
% RFC~7748's X25519 formalization (\sref{sec:Coq-RFC}) takes as input list of $\Z$.
......@@ -209,7 +209,7 @@
% % % this does not exists anymore
% % The location of the proof of this Hoare triple can be found in Appendix~\ref{appendix:proof-files}.
%
% % We now bring the attention of the reader to details of verifications using the VST.
% % We now bring the attention of the reader to details of verifications using VST.
%
% %% BLABLA about VST. Does not belong here.
%
......@@ -229,7 +229,7 @@
% % For the sake of completeness we proved all intermediate functions.
%
% \subheading{Memory aliasing.}
% In the VST, a simple specification of \texttt{M(o,a,b)} will assume three
% In VST, a simple specification of \texttt{M(o,a,b)} will assume three
% distinct memory share. When called with three memory shares (\texttt{o, a, b}),
% the three of them will be consumed. However assuming this naive specification
% when \texttt{M(o,a,a)} is called (squaring), the first two memory shares (\texttt{o, a})
......
Markdown is supported
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