Relational properties for specification and verification of C programs in Frama-C

PhD Thesis

Author(s):Lionel Blatter
School:Université Paris-Saclay
Number:2019SACLC065
Year:2019
PDF:
URL:https://tel.archives-ouvertes.fr/tel-02401884

Abstract

Deductive verification techniques provide powerful methods for formal verification of properties expressed in Hoare Logic. In this formalization, also known as axiomatic semantics, a program is seen as a predicate transformer, where each program c executed on a state verifying a property P leads to a state verifying another property Q.
Relational properties, on the other hand, link n programs to two properties. More precisely, a relational property is a property about n programs c₁, ..., cₙ stating that if each program cᵢ starts in a state sᵢ and ends in a state s0ᵢ such that P(s₁, ..., sₙ) holds, then Q(s0₁, ..., s0ₙ) holds. Thus, relational properties invoke any finite number of executions of possibly dissimilar programs.
Such properties cannot be expressed directly in the traditional setting of modular deductive verification, as axiomatic semantics cannot refer to two distinct executions of a program c, or different programs c₁ and c₂.
This thesis brings two solutions to the deductive verification of relationalproperties. Both of them make it possible to prove a relational property and to use it as a hypothesis in the subsequent verifications. We model our solutions using a small imperative language containing procedure calls.
Both solutions are implemented in the context of the C programming language, the FRAMA-C platform, the ACSL specification language and the deductive verification plugin WP. The new tool, called RPP, allows one to specify a relational property, to prove it using classic deductive verification, and to use it as hypothesis in the proof of other properties. The tool is evaluated over a set of illustrative examples.
Experiments have also been made on runtime checking of relational properties and counterexample generation when a property cannot be proved.

BibTeX

@phdthesis{blatter19,
  title     = {Relational properties for specification and verification
               of {C} programs in {Frama-C}},
  author    = {Lionel Blatter},
  url       = {https://tel.archives-ouvertes.fr/tel-02401884},
  number    = {2019SACLC065},
  school    = {{Universit{\'e} Paris-Saclay}},
  year      = {2019},
  month     = sep,
  pdf       = {https://tel.archives-ouvertes.fr/tel-02401884/file/74175_BLATTER_2019_diffusion.pdf},
  hal_id    = {tel-02401884},
  abstract  = {Deductive verification techniques provide powerful methods for formal verification of
               properties expressed in Hoare Logic. In this formalization, also
               known as axiomatic semantics, a program is seen as a predicate transformer, where each
               program \emph{c} executed on a state verifying a property P leads to a state verifying
               another property \emph{Q}.
               \newline

               Relational properties, on the other hand, link \emph{n} programs to two properties.
               More precisely, a relational property is a property about \emph{n} programs
               \emph{c₁}, ..., \emph{cₙ} stating that if each program \emph{cᵢ} starts in a state
               \emph{sᵢ} and ends in a state \emph{s0ᵢ} such that \emph{P(s₁, ..., sₙ)} holds, then
               \emph{Q(s0₁, ..., s0ₙ)} holds. Thus, relational properties invoke any finite number of
               executions of possibly dissimilar programs.
               \newline

               Such properties cannot be expressed directly in the traditional setting of modular
               deductive verification, as axiomatic semantics cannot refer to two distinct executions
               of a program \emph{c}, or different programs \emph{c₁} and \emph{c₂}.
               \newline

               This thesis brings two solutions to the deductive verification of relationalproperties.
               Both of them make it possible to prove a relational property and to use it as a hypothesis
               in the subsequent verifications. We model our solutions using a small imperative language
               containing procedure calls.
               \newline

               Both solutions are implemented in the context of the C programming language, the
               {FRAMA-C} platform, the {ACSL} specification language and the deductive verification
               plugin {WP}. The new tool, called {RPP}, allows one to specify a relational property,
               to prove it using classic deductive verification, and to use it as hypothesis in the
               proof of other properties. The tool is evaluated over a set of illustrative examples.
               \newline

               Experiments have also been made on runtime checking of relational properties and
               counterexample generation when a property cannot be proved.}
}