Secure Software Development
Software development can be approached as an engineering discipline, whereby a software product is constructed to satisfy a customer's specification in a rigorous manner. Formal methods are mathematically-based techniques which can be applied in software development projects to provide a high level of assurance that software products are correct by construction with respect to a specification consisting of functionality requirements.
Today, more than ever, software engineers need effective tools and techniques to help them build software products that are secure when connected to worldwide communication networks. The desire to build systems that are secure by design motivates the judicious application of formal methods in software developments: for example, it is widely recognised that formalisation is essential for designing robust cryptographic protocols. Our work involves devising novel techniques for integrating security concerns into formal methods and other rigorous approaches for software development.
Contact Jeremy Jacob or Michael Banks for more information.
Current and Recent Projects
Formal Methods and Information Flow Security
Even minor faults in the design or implementation of a system may be exploited by a determined adversary to acquire confidential (sensitive or valuable) data stored within the system. It is therefore imperative that software systems that handle confidential data are designed to prevent (or minimise) the leakage of this data to the environment. While formal methods have a role to play in the development of secure systems, there is currently no well-established approach for using formal methods with techniques for modelling the flow of confidential information to the environment.
This research project aims to produce a mathematical framework (and related tools) for designing software products that are guaranteed to uphold a specification of confidentiality and functionality requirements. The underlying semantic model of the framework is Hoare and He's Unifying Theories of Programming (UTP). Furthermore, this project is investigating how notions of information flow can be integrated with Circus (a specification language that combines Z and CSP to model the state and behavioural aspects of concurrent systems) to produce a platform for deriving secure implementations of systems by stepwise refinement.
Resolving Type Flaws in Cryptographic Protocols
A cryptographic protocol is said to contain a type flaw if an adversary can substitute parts of the raw data of an encrypted protocol message in transit to cause the recipient of the message to potentially misinterpret its contents. Type flaws have been discovered in a handful of published protocols. Provided that certain conditions hold for the implementations of these protocols, an adversary may apply a type flaw attack to compromise the security of protocol runs.
This work developed an algorithm for finding a class of type flaws in protocol descriptions. This algorithm may be applied to remove type flaws from protocols, by identifying a safe reordering of the fields within each encrypted message, without recourse to augmenting messages with contextual information.
The source code of the implementation of this algorithm is available.
