Commit 08a1d6d3 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

more rewrite

parent f14b2cb1
......@@ -272,13 +272,21 @@ note = {\url{https://books.google.nl/books?id=T_ShHENlqBAC&lpg=PR4&pg=PP1#v=o
}
@incollection{Howard1995-HOWTFN,
title = {The Formul\ae-as-Types Notion of Construction},
author = {W. A. Howard},
booktitle = {The Curry-Howard Isomorphism},
year = {1995},
editor = {Philippe De Groote},
publisher = {Academia},
note = {\url{https://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf}}
title = {The Formul\ae-as-Types Notion of Construction},
author = {W. A. Howard},
booktitle = {The Curry-Howard Isomorphism},
year = {1995},
editor = {Philippe De Groote},
publisher = {Academia},
note = {\url{https://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf}}
}
@techreport{ISO:C99,
title = {ISO C Standard 1999},
author = {ISO},
editor = {WG14},
note = {\url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1124.pdf}},
year = {1999}
}
@article{Leroy-backend,
......
......@@ -10,7 +10,7 @@ In this section we prove the following theorem:
The implementation in TweetNaCl matches the Coq definition of \TNaCle{crypto_scalarmult}
\end{theorem}
In this section we first describe the global structure of our proof.
We first describe the global structure of our proof.
Then we discuss techniques used to prove the equivalence between the
Clight description of TweetNaCl and Coq functions producing similar behaviors.
......
......@@ -331,7 +331,12 @@ int crypto_scalarmult(u8 *q,
Coq~\cite{coq-faq} is an interactive theorem prover. It provides an expressive
formal language to write mathematical definitions, algorithms and theorems coupled
with their proofs. As opposed to other systems such as F*~\cite{DBLP:journals/corr/BhargavanDFHPRR17},
with their proofs. It has been used in the proof the four-color theorem~\cite{gonthier2008formal}.
The CompCert C compiler~\cite{Leroy-backend} was implemented with it and provides
the guarante that the behaviour of the machine code is the same as the one
semantically defined in C (ISO C99~\cite{ISO:C99}).
As opposed to other systems such as F*~\cite{DBLP:journals/corr/BhargavanDFHPRR17},
Coq does not rely on an SMT solver in its trusted code base.
It uses its type system to verify the applications of hypotheses,
lemmas, and theorems~\cite{Howard1995-HOWTFN}.
......@@ -354,9 +359,14 @@ For example, here is the rule for sequential composition:
\end{prooftree}
Separation logic is an extension of Hoare logic which allows reasoning about
pointers and memory manipulation. This logic enforces strict conditions on the
memory shared such as being disjoint. We discuss this limitation further in Section~\ref{using-VST}.
The Verified Software Toolchain (VST)~\cite{cao2018vst-floyd} is a framework which uses
Separation logic to prove the functional correctness of C programs.
It can be seen as a forward symbolic execution of the program.
\todo{Mention CLight somewhere here.}
Its uses a strongest postcondition approach to prove that a program matches its specification.
memory shared such as being disjoint.
We discuss this limitation further in Section~\ref{using-VST}.
The Verified Software Toolchain (VST)~\cite{cao2018vst-floyd} is a framework
which uses Separation logic to prove the functional correctness of C programs.
The first step consists of translating the source code into CLight,
an intermediate representation used by CompCert.
For such purpose we use the parser CompCert: \texttt{clightgen}.
In second step we define the Hoare triple encapsulating the specification of the
piece of software we want to prove. Then using VST, we uses a strongest
postcondition approach to prove the correctness of the triple.
This approach can be seen as a forward symbolic execution of the program.
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