|My research is
about Analysis and
Verification: understanding software and specifications,
reasoning about them, proving that they satisfy desirable properties, showing that they behave correctly.
Common themes in my research are:
Security, Safety, Use of Information Theory, and Dependence Analysis
My current research interests include the following applications:
I am a member of CREST
I am a member of the EPSRC College (since 2006 until the present day)
Security and Code Free one day workshop 6 April 2011
Formal Methods and UML
I am currently looking for good quality PhD students. Funding is available for students of sufficiently high quality. Areas of interest include:
Secure Information Flow
A lot effort in making software secure goes into a kind of fire-fighting, i.e. discovering and closing vulnerabilities in code. However, even if all vulnerabilities have been eliminated, code still may not be secure. It may contain covert channels that allow attacks on confidentiality of information, integrity of information, and the privacy and anonymity of the user. Such covert channels leaking information may be within the logic of the program or be so-called side channels such as measuring execution times or heat dissipation over different runs. The challenge of constructing security critical code for contemporary software is enormous. Semantics based program analysis and type systems have a large role to play in guaranteeing end-to-end information security for networked systems.
Semantic Analysis of Found Code
Found code is code that the analyser did not write. It may be source code or binaries. The task is to understand what it does and the (common) motivation is defence against malicious behaviours. Techniques include reverse engineering, program analysis, testing, and use of SMT solvers. There are a whole range of problem domains in this area, for example malware classification and techniques for combatting packing, encryption and rewriting engines.
Testing Information Transformers
The hypothesis for this research is that the answers to some long standing questions in the theory of testing programs can be found or at least improved by viewing programs as transformers of information and using techniques from information theory and the measurement of information flow in programs to build an information theoretic theory of testing which answers questions such as the following. How do I select the test suite? When is it adequate? What does adequate mean in terms of information? How do I order the tests? There is a security aspect to this research. An improvement in testing generally will improve the fire fighting of vulnerabilities and exploits, particularly when harnessed with information about attack vector templates.
Last modified: Wed Apr 24 15:44:19 BST 2013