| |
| Quantitative Program Analysis and Applications to Computer Security |
Alessandra Di Pierro
Herbert Wiklicky
(Univ. of Pisa, Italy and Imperial College, UK)
|
| Duration: 180 minutes |
ABSTRACT:
Program analysis provides semantics based compile-time techniques for
statically predicting safe and computable approximations to the set of
behaviours arising dynamically when executing a program on a computer.
Quantitative program analysis aims at developing techniques which
provide approximate answers with some numerical estimate of the
precision of the approximation.
One useful source of numerical information for a quantitative program
analysis is a probabilistic semantics and in particular the use of
vector space or linear algebraic structures for modelling the
computational domain. By exploiting the probabilistic information
resulting from a probabilistic program analysis one can quantify
the precision of the analysis and obtain as a result answers which are
for example "approximate up to 35%".
We will illustrate such a quantitative approach in the framework of
Probabilistic Abstract Interpretation which provides a
general methodology for constructing quantitative analyses.
We will then demonstrate this technique by presenting some
applications in computer security. We will concentrate on the problem
of preventing unauthorised users from reading sensitive information,
aka confidentiality, and show how a quantitative program analysis of
confidentiality can be defined which gives a measure for the
confinement of a system. We will also illustrate applications to
the analysis of other security aspects which are crucial in
a distributed setting, namely firewalls and network vulnerability.
| |