Compositional Verification of
Control-Flow Properties
of Programs with Procedures
1. Introduction
CVPP is an informal
collaborative project aiming at the development of techniques for the
algorithmic verification of
control flow based properties of programs with procedures, with focus
on
compositionality.
2. Participants
At present, the people involved in the collaboration are:
3. Summary of the Approach
We develop methods for the algorithmic verification of open systems,
that is, systems where some components (termed concrete) are available through
their
implementation as Java bytecode, while other components (termed abstract) are given
through their specifications,
that is, a formal description of their essential properties. Such
systems arise naturally when the implementation of certain components
is not yet available, such as in the context of mobile code.
Open systems also arise in the context of modular design,
where for verification purposes the specification of components is used
rather than their implementation, since the implementation is allowed
to change
over time (say, be optimised for performance) but not the
specification. The
main problem that arises when verifying open systems is how to
relativise the verification on specifications of components. The
technique we explore is based on the notion of maximal model
for a given specification, that is a model that represents all
models satisfying the specification, in the sense that it possesses
exactly those properties shared by all these models. In effect, this
allows abstract components to be replaced by concrete ones, in this way
reducing the verification problem to standard model checking.
Our program
model abstracts from the data, thus focusing on (and
over-approximating) program control
flow. The structure of programs is given by means of flow graphs,
while program behaviour is given by means of pushdown automata
(PDAs), induced canonically from the flow graphs, and capturing
the passing of control during method calls and returns.
We consider properties
of the structure as well as the behaviour of programs. Both types of
properties are specified in a fragment of the modal mu-calculus
with box modalities and greatest fixed points only, interpreted over
flow graphs and flow graph behaviours, respectively.
4. Verification Method
Our algorithmic verification
method for open systems deals (a) with components, namely how a
component implementation relates to its specification, as well as (b)
with systems, namely how system properties relate to component
properties.
A. Model checking of a concrete
component
against a property (specification) consists of the following steps:
- Extract flow graph of component from Java bytecode [Program
Analyser]
- If needed, inline private methods [Inliner]
- For structural properties:
- cast flow graph as finite automaton, e.g. as CCS term [Model
Generator], then
- apply standard, finite–state model checking [CWB]
- For behavioural properties:
- cast flow graph as pushdown automaton [Model Generator], then
- apply PDA model checking [NikMC]
B. Model checking of an open system
against a property consists of the following steps:
- For every concrete component, proceed as explained in A.1
- For every abstract component, from specification:
- if structural, compute maximal flow graph [Maximal Model
Constructor]
- if behavioural, first translate to equivalent set of structural
properties [Property Translator], then construct the corresponding set
of maximal flow graphs
- Compose extracted with constructed flow graphs to obtain the flow
graph of the open system
- Model check resulting flow graph against global property, as
explained in A.2
5. Tool Support
We provide tool support for our verification method in the form of a tool set
consisting of the following individual tools:
- Program Analyser:
Extracts flow graphs (with the help of Sawja)
- Inliner: Abstracts flow
graph from private methods
- Property Translator: Translates
behavioural to structural properties
- Maximal Model Constructor:
Produces maximal flow graphs
- Model Generator: Casts
flow graphs as FAs or PDAs for model checking
- Model Checkers: For
verifying structural and behavioural properties
6. Publications
- ProMoVer: Modular Verification of Temporal Safety Properties
Siavash Soleimanifard, Dilian Gurov, and Marieke Huisman
To appear in Proceedings of: SEFM'11
Lecture Notes in Computer Science, vol. ????, pp. ??-??,
2011
- Compositional Algorithmic Verification of Software Product Lines
Ina Schaefer, Dilian Gurov, and Siavash Soleimanifard
To appear in Post-proceedings of: FMCO'10
Lecture Notes in Computer Science, vol. ????, pp. ??-??,
2011
- CVPP: A Tool Set for Compositonal Verification of Control-Flow Safety Properties
Marieke Huisman, and Dilian Gurov
To appear in Proceedings of: FoVeOOS'10,
2010
- Procedure-Modular Verification of Control Flow Safety Properties
Siavash Soleimanifard, Dilian Gurov, and Marieke Huisman
To appear in Proceedings of: FTfJP'10,
2010
- Reducing Behavioural to
Structural
Properties of Programs with Procedures
Dilian Gurov and
Marieke Huisman
In Proceedings of: VMCAI'09
Lecture Notes in Computer Science,
vol. 5403, pp. 136-150,
2009 (tool web-interface) (slides)
Full version
available as: Technical Report TRITA-CSC-TCS 2007:3,
December 2007
- Program Models for Compositional
Verification
Marieke Huisman, Irem Aktug, and
Dilian Gurov
In Proceedings of: ICFEM'08
Lecture Notes in Computer Science, vol. 5256, pp. 147-166,
2008
- Compositional
Verification of Sequential Programs with Procedures
Dilian Gurov, Marieke Huisman, and
Christoph Sprenger
Journal
of Information and Computation, vol.
206, no. 7, pp. 840-868, 2008
- Composing
Modal
Properties of Programs with Procedures
Marieke Huisman, and Dilian Gurov
In Proceedings of: FESCA'07
Electronic Notes in Theoretical Computer Science, vol. 203,
issue 7, pp. 87-101, 2009 (slides)
- Interface
Abstraction for
Compositional
Verification
Dilian Gurov, and Marieke Huisman
In Proceedings of: SEFM'05
IEEE Computer Society, pp. 414-423, 2005 (slides)
- Compositional
Verification for Secure Loading of Smart Card Applets
Christoph Sprenger, Dilian Gurov, and Marieke Huisman
In Proceedings of: Memocode'04
IEEE Formal Methods and Models for Co-Design, pp. 211-222,
2004
- Checking
Absence of Illicit Applet Interactions: A Case Study
Marieke Huisman, Dilian Gurov, Christoph Sprenger, and Gennady Chugunov
In Proceedings of: FASE'04 [337]
Lecture Notes in Computer Science, vol. 2984, pp. 84-98
Winner of the EASST
award for Best Software Science Paper,
2004 (slides)
- Simulation
Logic, Applets and Compositional Verification
Christoph Sprenger, Dilian Gurov, and Marieke Huisman
INRIA Technical Report RR-4890,
2003
- Model
Checking of Multi-Applet JavaCard Applications
Gennady Chugunov, Lars-Åke Fredlund, and Dilian Gurov
In Proceedings of: CARDIS'02 [534]
USENIX Publications, pp. 87-95,
2002 (slides)
- Compositional
Verification of Secure Applet Interactions
Gilles Barthe, Dilian Gurov, and Marieke Huisman
In Proceedings of: FASE'02 [337]
Lecture Notes in Computer Science, vol. 2306, pp. 15-32,
2002 (slides)
- Compositional
Specification and Verification of Control Flow
Based
Security Properties of Multi-Application Programs
Gilles Barthe, Dilian Gurov, and Marieke Huisman
In Proceedings of: FTfJP'01,
2001