Verification of software: 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, Information Theory, Program Analysis
My current research interests include:
I am a member of CREST
Together with Earl Barr I founded the Theory Tendency of the SSE
I am a member of the EPSRC College (since 2006 until the present day)
COW on Information Theory and Testing Software January 2018
TAROT Summer School on Software Testing July 2018
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, discovering and patching vulnerabilities in code. However, even if all patchable vulnerabilities have been eliminated, code still may not be secure. It may contain covert channels that allow attacks on confidentiality and integrity of information, or 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 either source code or binaries. If we want to use such code or discover it on our systems we want to understand what it does and one (common) scenario is defence against malicious behaviours. Techniques employed to aid understanding and analysis may include reverse engineering, static and dynamic program analysis, software testing, and the use of tools that employ SMT solvers such as Klee and CBMC. There are a range of problem domains in this area, for example malware classification and techniques for combatting packing, encryption and rewriting and obfuscation 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: 31 August 2017