We are concerned with getting computer systems and components right, and justifying why they are right. This is essential for safety and security-critical systems, whose failure can put lives, the environment or enterprises at risk. Our approach uses logical modelling of systems to be able to express precisely (mathematically) how they are required to behave, and using formal analysis techniques for proving that they indeed behave in the right way. We are developing formal techniques for distributed control systems and for security mechanisms and systems.

Our particular emphasis is on applying and reusing existing techniques in new ways, and on new application areas. We have developed a combination of the B-Method and Event-B with CSP, allowing us to combine different viewpoints on a system in a well-founded way, and enabling the combining of the mature verification technology each of them separately provide. We also provide ways of applying this approach to widely-used development methods such as UML (for software) and VHDL (for hardware) by supporting translation to and from our framework.

Our security work has previously focussed on security protocols, which use cryptographic mechanisms to provide secure ways for agents to interact over an insecure network. Such protocols are notoriously difficult to get right, and can contain subtle flaws which could be exploited by an attacker. By formal modelling and analysis, we can discover attacks in vulnerable protocols, and can verify that sound protocols do not contain this kind of logical flaw.

Our security activity is currently working on the design and development of a particular security application: trustworthy voting systems. As well as the underlying theoretical justification for the design decisions and the security assurances, this activity also contains the challenge of creating a usable and practical system, involving socio-technical issues concerned with processes and the way voters and election officials will make use of the system. The challenge here is not only for experts to establish the security of the system, but also to achieve public comprehension of the security justification in order to engender trust.