Abstract
In this talk, we will present a parametric abstract domain for the
static analysis by abstract interpretation of programs which manipulate
complex and dynamically allocated data-structures. We will set up
the foundations for a family of static analyses to compute an
over-approximation of the reachable states of programs using such
structures.
Our domain can be parameterized with a set of inductive definitions
capturing a set of relevant data-structures and by the choice of an
underlying numerical domain. Abstract values can be viewed either as
graphs, or as formulas in a subset of separation logic extended with
inductive definitions. We will describe the abstraction induced by
this domain, and the main static analysis operators. In particular,
we will consider the unfolding operator, which allows to refine in a
local manner an abstract value, so as to allow precise algorithms for
the computation of post-conditions. Then, we will discuss a set of
join and widening operators, so as to guarantee the termination of
our static analyses.
In the second part of the talk, we will consider several applications
of our static analysis. We will show how it can be adapted in order
to treat in a precise way specific features of programs written in
languages which allow low level memory operations, such as the C
language. Then, we will focus on the analysis of programs with
recursive procedures and we will introduce a powerful widening
operator, which is able to infer accurate inductive definitions to
be used to summarize the call-stack of a specific program together
with the memory.
Finally, the last part of this talk will be devoted to perspectives
for extensions of our analysis.
Short bio
Xavier Rival studied at Ecole Normale Superieure (Paris, France) and
prepared his PhD Thesis under the supervision of Patrick Cousot. After
defending his PhD in 2005, he worked as a Post Doctorate researcher at
University of California at Berkeley from 2006 to 2007. Then, he joined
Inria as a Junior Researcher in 2007, as part of the "Abstraction"
project team. He also holds a part time Lecturer position at Ecole
Polytechnique (Paris, France). He has also been a member of the
Astree project since its beginning in 2001.
Xavier Rival also defended his Habilitation Thesis in 2011.
He is interested in static analysis using abstract interpretation
technique. Over the last few years, he has mainly been studying the
static analysis of programs manipulating complex data-structures.
including the best paper award at the USENIX Security Symposium and
the highest ranked paper at the IEEE Symposium on Security and
Privacy.
Resources
This will be shown to users with no Flash or Javascript.
|
