The Formal Verification and Security group works on the application of formal verification methods to systems and mechanisms of real-world complexity, with special attention to security. For example, we have created rigorous formalizations of feature constructs for programming and specification languages. We were the first to apply formal verification methods to analysing electronic voting systems, and model-checking techniques to access control systems.
Computer security research was expanded and strengthened in 2007 by new appointments. The resulting new research includes approximate-logic based verification of large-scale, open-source software, analysis of anonymous file sharing, and applied cryptography and information security including the development of digital signature schemes. A collaboration with Liqun Chen (HP Labs, Bristol) on fundamentals of verification of voting-protocol security is addressing conflicts between security and privacy in the context of Direct Anonymous Attestation.
Our research interests include:
We are developing formalisms and theories for the modelling of security protocols, as well as methods and software tools for their analysis. The importance of this work lies in the ability to analyse a complex design, before the actual hardware or software component has been manufactured and deployed. The effort spent on deriving a model and analysing it results in an assurance that the end product does indeed satisfy its security objectives. Our current research focuses on privacy properties as found in trusted computing, contract signing and electronic voting protocols.
Access control systems are a pervasive component in modern computer systems, being used to moderate access to resources such as files, mobile devices, databases, and web services. As systems become more sophisticated, the policies which regulate access controls become increasingly dynamic, complex, and prone to errors. Our research develops languages and enforcement mechanisms that enable users to administer access controls based on their requirements of a system's behaviour. Furthermore, we develop formalisms to model access control systems, allowing us to verify their correctness.
Cryptography aims to provide the basic building blocks to achieve security related objectives such as confidentiality, integrity, authentication and non-repudiation. Our work involves the design, analysis and application of cryptographic primitives. Currently, our focus includes digital signatures, fair exchange and authentication. We are also interested in identity privacy, key agreement protocols, public key encryption, pairing-based cryptography, algorithms & implementations, multimedia security and network security.
Software security aims to develop mechanisms to ensure the safe design and execution of software. We are primarily interested in the development of language protection mechanism using formalisms such as Hoare logic and Separation Logic. Recent advances in program logics make it possible to reason rigorously about pointers, the heap and concurrency. This enables us to offer better protection against buffer overflows, format string attacks, race conditions and code injections.
