T2: Quantitative program analysis for security
Quantitative Program Analysis and Applications to Computer Security
Alessandra Di Pierro
Herbert Wiklicky
(Univ. of Pisa, Italy and Imperial College, UK)
Duration: 180 minutes
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.
Web Maintenance Person.