Commit 23b1d007 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

forward

parent 82f2b86e
......@@ -42,3 +42,21 @@ We extend the work of Bartzia and Strub \cite{DBLP:conf/itp/BartziaS14} to
support Montgomery curves.
With this formalization, we prove the correctness of a generic Montgomery ladder
and show that our specification can be seen as an instance of it.
% Five years ago:
% \url{https://www.imperialviolet.org/2014/09/11/moveprovers.html}
% \url{https://www.imperialviolet.org/2014/09/07/provers.html}
% \section{Related Works}
%
% \begin{itemize}
% \item HACL*
% \item Proving SHA-256 and HMAC
% \item \url{http://www.iis.sinica.edu.tw/~bywang/papers/ccs17.pdf}
% \item \url{http://www.iis.sinica.edu.tw/~bywang/papers/ccs14.pdf}
% \item \url{https://cryptojedi.org/crypto/#gfverif}
% \item \url{https://cryptojedi.org/crypto/#verify25519}
% \item Fiat Crypto : synthesis
% \end{itemize}
%
% Add comparison with Fiat-crypto
\section{Linking C and Reflections}
\section{Representation and Reflections}
In this section we describe techniques used to prove the equivalence between the
Clight description of TweetNaCl and Coq functions producing similar behaviors.
......@@ -184,6 +184,9 @@ Definition f_inv_denote (t : formula_inv) : Prop :=
| Eq_inv x y => e_inv_denote x = e_inv_denote y
end.
\end{lstlisting}
All denote functions also take as an argument the environment containing the variables.
We do not show it here for the sake of readability.
Given that an environment, \Coqe{term_denote} returns the appropriate variable.
With such Domain Specific Language we have the equality between:
\begin{lstlisting}[backgroundcolor=\color{white}]
f_inv_denote
......@@ -191,6 +194,9 @@ f_inv_denote
(P_inv R_inv 3))
= (x * x^2 = x^3)
\end{lstlisting}
On the right side, \Coqe{(x * x^2 = x^3)} depends on $x$. On the left side,
\texttt{(Eq\_inv (M\_inv R\_inv (S\_inv R\_inv)) (P\_inv R\_inv 3))} does not depend on $x$.
This allows us to use computations in our decision precedure.
We define \Coqe{step_inv} and \Coqe{pow_inv} to mirror the behavior of
\Coqe{step_pow_Z} and respectively \Coqe{pow_fn_rev_Z} over our DSL and
......
\section{Related Works}
\todo[inline]{Write write write}
\begin{itemize}
\item HACL*
\item Proving SHA-256 and HMAC
\item \url{http://www.iis.sinica.edu.tw/~bywang/papers/ccs17.pdf}
\item \url{http://www.iis.sinica.edu.tw/~bywang/papers/ccs14.pdf}
\item \url{https://cryptojedi.org/crypto/#gfverif}
\item \url{https://cryptojedi.org/crypto/#verify25519}
\item Fiat Crypto : synthesis
\end{itemize}
Add comparison with Fiat-crypto
\section{Using VST}
\subsection{The Trusted Base}
Any formal system relies on a trusted base. In this section we describe our
chain of trust bringing up to light some tripping points a user may encounter
when using VST.
\todo[inline]{blablabla needs to be rewritten}
\subsection{The Trusted Base}
The soundness of our proof relies on a trusted base
, i.e. a foundation of specifications and implementations
that must stay correct with respect to the specifications.
Our proof relies on a trusted base , i.e. a foundation of specifications
and implementations that must stay correct with respect to their specifications.
One should not be able to prove a false statement in that system e.g. by proving
an inconsistency.
In our case we rely on:
\begin{itemize}
\item \textbf{Calculus of Inductive Construction} : The intuitionistic logic
used by Coq must be consistent in order to trust the proofs. We assumed that
the functional extensionality was also consistent with that logic.
$
\begin{array}{c}
\forall A\ B (f\ g : A \to B ),\\
( \forall x : A , f(x) = g(x) ) \implies f = g
\end{array}
$
\item \textbf{CompCert} Clight model
\item \textbf{\texttt{clightgen}} translation from \textbf{C} to
\textbf{Clight}.
VST does not support the verification of
\texttt{o[i] = a[i] + b[i]}, the \texttt{forward} tactic will simply not work.
This required us to rewrite the lines into:\\
\texttt{aux1 = a[i];\\
aux2 = b[i];\\
o[i] = aux1 + aux2;}. This rewriting is done
\item \textbf{Calculus of Inductive Construction}. The intuitionistic logic
used by Coq must be consistent in order to trust the proofs. As an axiom,
we assumed that the functional extensionality, which is also consistent with that logic.
$$\forall x, f(x) = g(x) ) \implies f = g$$
\begin{lstlisting}[language=Coq]
Lemma f_ext: forall (A B:Types),
forall (f g: A -> B),
(forall x, f(x) = g(x)) -> f = g.
\end{lstlisting}
\item \textbf{Verifiable Software Toolchain}. This framework developped at
Princeton allows a user to prove that a \texttt{CLight} code matches pure Coq
specification. However one must trust that the framework properly captures and
map the CLight behavior to the basic pure Coq functions. At the begining of
the project we found inconsistency and reported them to the authors.
\item \textbf{CompCert}. The formally proven compiler. We trust that the Clight
model captures correctly the C standard. (VERIFY THIS, WHICH STANDARD ?).
Our proof also assumes that the TweetNaCl code will behave as expected if
compiled under CompCert. We do not provide garantees for other C compilers
such as Clang or GCC.
\item \textbf{\texttt{clightgen}}. The tool making the translation from \textbf{C} to
\textbf{Clight}. It is the first step of the compilation.
VST does not support the direct verification of \texttt{o[i] = a[i] + b[i]}.
This required us to rewrite the lines into:
\begin{lstlisting}[language=C]
aux1 = a[i];
aux2 = b[i];
o[i] = aux1 + aux2;
\end{lstlisting}
The trust of the proof relied on the trust of a correct translation from the
initial version of \textit{TweetNaCl} to \textit{TweetNaclVerificable}.
While this problem is still present, the Compcert developpers provided us with
the \texttt{-normalize} option for \texttt{clightgen} which takes care of
generating auxiliary variables in order to automatically derive these steps.
The changes required for a C-code to make it Verifiable are now minimals.
The changes required for a C-code to make it Verifiable are now minimal.
\item The \textbf{Coq kernel}, the \textbf{Ocaml compiler},
the \textbf{Ocaml Runtime} and the \textbf{CPU}. These are common to all proofs
\item Last but not the least, 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}.
\end{itemize}
\subsection{Aliasing and Memory collision}
Necessity to go back into your specification multiple times to refine your model.
e.g. prove \texttt{M(o,a,b)} later notice that you can have aliasing, need to redefine
your theorem to prove \texttt{M(o,a,a)} (\textit{squaring}) and other variants such as:
\texttt{M(a,a,b)} and \texttt{M(b,a,b)}.
\subsection{Using the Verifiable Software Toolchain}
Proving a few lines of code with VST requires to have a good knowledge of what
each line of code will do when executed. A user will want to specify a pure Coq
implementations which will be close to a 1:1 mapping with the C implementation.
This will simplify the proof and help with stepping throught the program.
We call this step a Low level specification. A user will then have an easier
time to prove that his low level specification matches a simpler higher level one.
In order to further speed-up the verification process, it should be know that
in order to prove \VSTe{crypto_scalarmult}, a user only need the specification
of e.g. \VSTe{M}. This provide with multiple advantages: the verification by the
kernel can be done in parallel and multiple users can work on proving different
functions at the same time. For the sake of completeness we proved all intermediate
functions.
Memory aliasing is the next point a user should pay attention to. The way VST
deals with the separation logic is similar to a consumer producer problem.
A naive specification of \texttt{M(o,a,b)} will assume three distinct memory share.
When called with three memory share (\texttt{o, a, b}), the three of them will be consumed.
However when \texttt{M(o,a,a)} is called (squaring), the first two memory shares (\texttt{o, a})
are consumed and VST will expect a third memory share where the last \texttt{a} is pointing at.
This forces the user to define multiple specifications for a single function.
Example of such cases are summarized in Fig \ref{tk:MemSame}.
\begin{figure}[h]
\include{tikz/memory_same_sh}
\caption{Aliasing and Separation Logic}
\label{tk:MemSame}
\end{figure}
Prove \texttt{M(o,a,b)} where o is a \texttt{list $\Z$} and then realize that
\texttt{o} can be a list of \textit{undefined} (\texttt{list val}). Thus needs
to reprove the above theorem again.
% \begin{figure}[h]
% \include{tikz/memory_diff_sh}
% \caption{Memory Share and Separation Logic}
% \label{tk:MemSame}
% \end{figure}
\subsection{How to be efficient with VST?}
This approach is \textbf{slow}, \textbf{tedious} and \textbf{frustrating}.
The time cost way to big for such a proof and definitively not applicable for a
cryptographic engineer.
Necessity to prove everything at least 3 to 4 times (high level, low level, C-link).
The \texttt{forward} and \texttt{entailer} tactics are slow.
Specification and proofs does not need to be in the same file (as initially \textit{implied}
by the examples provided by the VST repository). Putting the specification of each
functions in separate file reduce the amount of dependencies. One does not need
to wait for the proof of correctness of \texttt{M(o,a,b)} to compile the proof of \texttt{crypto\_scalarmult(q,n,p)}.
This separation allows a high degree of parallelism during compilation \texttt{make -j},
greatly reducing the amount of time required.
Three years ago:
\url{https://www.imperialviolet.org/2014/09/11/moveprovers.html}
\url{https://www.imperialviolet.org/2014/09/07/provers.html}
\subsection{Pointers arithmetic, arrays and types}
It is to be noted that the \texttt{clightgen} tool has not been formally verified.
\texttt{clightgen -normalize}
% Not true since VST 2.0
%
% Assuming that \texttt{b} is of type \texttt{long long}, the following expression
% will not be type-checked by VST.
%
% \texttt{b = 1 - b;}
%
% \texttt{1} is interpreted by cligthgen as \texttt{Vint} (\textit{Value of int})
% while \texttt{b} is interpreted as \texttt{Vlong} (\textit{Value of long}),
% resulting in an error. To solve this, we need to prefix \texttt{1} by an
% explicit cast in C into the correct type. As a result, any constants used in this
% implementation had to be casted to the correct type
% (in \textit{TweetNaclVerificable}) to pass typecheck.
\subsection{Verifiying for loops: head and tail recursion}
\subsection{Verifiying \texttt{for} loops: head and tail recursion}
While the final state of a For loops can be computed by a simple recursive function,
we must define invariants that are true for each step of the iteration.
......@@ -137,10 +117,11 @@ Lemma Tail_Head_equiv :
rec_fn n s = rec_fn_rev n s.
\end{Coq}
In order to prove the for loops, we must define invariants.
Those have to be
\todo[inline]{How many lines of specification ?}
\todo[inline]{How many lines of proofs ?}
\todo[inline]{How long did it take ?}
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