Overview
My main area of research is semantics-based program analysis. This is a collection of techniques that may be used to infer dynamic properties of program behavior without running the program. The properties are approximated by simulating the program execution using simplified domains of values and techniques to ensure termination. Traditionally such techniques have been used in optimising compilers. The advantage of semantics-based techniques is that the analyses can be proved correct; in this context correctness is often called safety and guarantees that if the analysis infers a property then the program does really have that property.
Over the last few years it has become apparent that the same program analysis techniques can be used to certify programs against security criteria. We have worked on information flow analysis. We have also developed a new notion of approximate confinement which, recognising that perfect security may be unattainable, aims to quantify how vulnerable a system is.
My early work was based on qualitative approaches to program analysis using lattice and domain theory as a basis. Recently, together with Di Pierro and Wiklicky, I have been developing a framework for the quantitative analysis of programs and systems.
Collaborators
Pasquale Malacaria, Queen Mary University of London, Game Theory and Cyber Security, 2011
Alessandra Di Pierro, University of Pisa, Program Analysis
Herbert Wiklicky, Department of Computing, Imperial College, Program Analysis
Flemming Nielson, Danish Technical University, Program Analysis
Hanne Riis Nielson, Danish Technical University, Program Analysis
Research Staff
Fielder,A
Le Matelot,E
Li,T
Simmie,D
Vigliotti,MG
Research Student Supervision
Caplin,T, Quantitative Analysis
Greenhough,H, Tracking in Information Space
Gudgeon,J, Looking towards the future: The changing nature of intrusive surveillance and technical attacks against high-profile targets
Nanz,S, Security Analysis of Mobile Wireless Networks