Summary:  Consider the idea of interference, the capacity of one part of a system to affect the behaviour of another part. Non-interference, i.e. absence of interference, is often used in proving that a software system is well-behaved, whereas interference can lead to obscure (mis-)behaviours. However the misbehaviour in presence of interference will generally happen  only when there is enough  interference. Think in terms of electric current: non-interference between  X and Y is the absence of a circuit involving X and Y; interference is the existence of a circuit; this however doesn't imply that there is enough ``current'' in the circuit to adversely affect the behaviour of the system. In previous work we have had considerable success in estimating interference for simple programming languages using Shannon's Information Theory. We aim to widen the current scope of our methods of reasoning and analysis so that we can consider more sophisticated security attacks, such as timing attacks and statistical attacks, and reason about more complex systems that may be reactive, Object Oriented, or incorporate probabilistic aspects. We plan to improve the  quality  of our analyses by calculating tighter bounds on the amounts of information that flows. We have identified the following threads of investigation as being key to these aims: expressivity (extension of our work to a wider class of languages),  time (extension to reasoning about  time), and  partial equivalence relations (using relations as a reasoning tool). A successful outcome of our proposed research in the above three threads will provide conceptual tools for quantitative analyses of information flow in a typed higher-order object-oriented multi-threaded language .  Such research would be sufficient for the analysis of software applications like password protected systems and spyware.

David Clark

• City University London
• Queen Mary University of London

This project was funded by the EPSRC.