Static Program Analysis.

Our main methodological approach towards the investigation of resource is to use static program analysis techniques. Much of the literature on static analysis concerns itself with qualitative properties of programs, e.g. ``Does this variable always contain the same constant value when the program execution reaches this point?'', ``Can this process reach a deadlock state?'' or ``Does this variable always point to an acyclic structure at this point?''. When we focus on resources it becomes more natural to ask quantitative questions, e.g.: ``How much resource on average does the program use?'' or ``What is the probability that an attacker is able to infer information about our secret data?'' or ``How much information can the attacker infer?''.

Quantitative approaches to static analysis of programs are relatively new and have mainly focused on probabilistic questions. The investigators started their collaboration under a previous EPSRC contract (GR/M58740) where they begun work on using probabilistic techniques for security. The main results from this previous project concerned the development of the framework of Probabilistic Abstract Interpretation [22,21] and the notion of Approximate Confinement [23,27]. Our work on confinement was based on the notion of I/O observables of processes. Since the end of the grant, we have developed a much more general framework based on probabilistic transition systems where we have characterised various process equivalences (including bisimulation) via Probabilistic Abstract Interpretation [29].

The aim of the current project proposal (as a continuation of the work started previously) is to generalise the framework and to overcome some of its current shortcomings. In particular we will address the following issues: (i) development of an extension of the probabilistic setting in order to deal with other quantitative aspects of program semantics (e.g. time, memory, information), (ii) research into a more ``calculational'' approach towards the formulation of quantitative analyses; this would address one problem with the program analyses we have developed in the previous project which were essentially ``handcrafted'', and (iii) the extension of our analysis framework to distributed computing and coordination models.