Cyber security and privacy are issues that concern everyone living in this technologically dependent world. The work within our Security and Privacy Research Group is underpinned by considering critical issues for industry, government and society. For a list of academic papers by researcher or research area, see publications.
Cryptography is the study of mathematical techniques that secure and protect information in a digital format. It is used in securely sending and receiving messages. The security aspects include confidentiality, integrity, authentication and nonrepudiation. The protocols that apply cryptographic methods are called cryptographic or security protocols. Applications of cryptography include electronic voting, e-passports and RFIDs etc.
Security protocols are notoriously difficult to design and extremely error-prone. Therefore, formal verification is crucial to assess their security. This involves analysing systems with respect to a formal specification using mathematics. This helps to identify flaws within electronic systems and develop solutions for those problems.
Technologies today are increasingly operating wirelessly, enabling communication to occur further, faster and more flexibly. Our research covers a broad range of wireless devices, protocols and systems, from mobile phone networks to embedded devices communicating with one another or even vast systems of clouds, servers, products and users. With applications in conjunction with our other areas of expertise, this research topic focuses on ensuring wireless communication can occur securely while maintaining the functionality necessary for individuals and organisations to operate effectively.
From immobilisers and key fobs to sat-nav and self-driving cars, automotive vehicles are becoming increasingly wireless. This trend, that is only increasing in pace and extent, brings ubiquitous computing to our roads. To ensure security, privacy and safety, our researchers are testing the digital systems embedded in modern cars, in order to identify weaknesses and suggest solutions for manufacturers and users.
Electronic voting has boomed in the past decade, and more than a dozen countries have already used it for political binding elections, including Switzerland, Estonia, USA and Australia. Electronic voting has also become a choice more and more usual for elections in professional colleges or boards. The potential benefits of its use are the ease of voting for citizens living abroad, shortening the duration of the counting procedure, providing a more exact count of the votes or decreasing the number errors with respect to paper voting. The disadvantages are also important, including the risks of computer attacks, the possibility of coercion related to the fact that the act of voting will not be conducted in a public place, or the lack of voters' confidence in the system because of its complexity. Usually it is distinguished between remote voting, meaning that the voting device can potentially be any smart device with an Internet connection; and polling-site voting, meaning that the voters are authenticated in a polling station, but they use an electronic voting machine to cast their votes.
Cloud computing means entrusting data to information systems that are managed by external parties on remote servers, collectively known as the cloud. Cloud security raises privacy and confidentiality concerns, because the service provider has access to all the data and could accidentally or deliberately disclose it.
All aspects of our research are underpinned by a commitment to tackling challenging issues that are important to society. Amidst our theoretical and technical outputs with impact across a range of sectors in industry and governments we maintain an awareness of the variety of stakeholders and perspectives concerning social issues the consequences of which we cannot yet fully predict. Working between the need for security and individuals' right to privacy, our research consistently displays a sensitivity to its social impact, particularly when dealing with the often controversial issues in cyber security for current and future society.
The Security and Privacy group maintains a firm commitment to high quality research and education in cyber security. This includes not only pursuing each strand of intellectual endeavour separately, but ensuring that teaching is informed by up-to-date research and that research responds to the needs to raise the profile of security issues in computer science education. To achieve this, our researchers undertake work investigating the direct application of cyber security and privacy issues in teaching environments. For more information about our range of specific programmes, see education.
Connected and autonomous vehicles are set to revolutionise our transportation and re-shape our cities. They will prevent accidents, reduce parking space requirements, lower congestion and pollution. But in order to achieve this, they need several sensors and wireless interfaces which connect them with other vehicles, consumer devices, infrastructure and the Internet. This connectivity adds great functionality but it also introduces a myriad of security and privacy threats. Safety critical functionality in the vehicle is controlled by a multitude of Electronic Control Units (ECUs) which are fully programmable. As vehicles become more programmable, complex and interconnected, they also become more vulnerable to cyber attacks.
The main goal of this fellowship is to secure connected and autonomous vehicles, making them resilient to this type of attacks. We will achieve this goal by developing techniques to secure each component of the vehicle's electronic architecture: ensuring that each ECU only executes code that is suitably authenticated; using model learning techniques to develop a framework for automated security testing of ECUs in a way that it scales; securing the vehicle's sensors such as radar, lidar and optical cameras against signal spoofing, tampering and denial of service attacks which would cause them to output inaccurate readings; and improving the communication protocols between vehicles and between the vehicles and the infrastructure in order to provide authenticity, non-repudiation and privacy while complying with stringent real-time constraints.
This project is funded by an EPSRC Fellowship.
Many modern processors are equipped with hardware extensions that enable some kind of Trusted Execution Environment (TEE). This allows programs to run securely - protected from other programs or operating system software running on the processor. By establishing a secure interface between the user and the hardware-anchor, we can make user platforms and devices more resilient to malware and other types of cyber attacks.
One of the main goals of this project is to promote and facilitate the adoption of TEE as the main trust anchor for our security architectures. As such, the security of the TEEs themselves is of paramount importance. We will perform a thorough evaluation of the security features of different TEE implementations to determine their suitability as trust anchors. This includes assessing cryptographic protocols, side-channel vulnerabilities, and implementation weaknesses.
Hardware supported TEEs aim to ensure that code can execute securely. However, user interface devices (for example, a keyboard, display or touch screen) are usually not connected directly to the secure hardware, which means that the user cannot interact securely with the TEE. We will address the limitations of users interacting directly with TEEs through analysing use cases and developing secure interfaces using auxiliary devices and dedicated features.
Authentication today is largely based on user supplied information like passwords or biometrics. These approaches often use information that is easy to steal or brute force. The industry has been moving towards multi-factor authentication as a means of spreading risk, but these approaches impose usability challenges while still relying on weak factors. We will investigate opportunities to leverage strong hardware-based security mechanisms to improve both the strength and usability of authentication. We will also build an architecture for designing protocols and user experiences that leverage these hardware security primitives to enhance the security, manageability, and usability of user authentication over existing approaches.The analysis and applications of our research findings will be demonstrated and implemented on suitable platforms including secure hardware, smart devices and integration with authentication tokens.
This project is funded by the EPSRC as part of the new £5million UK Research Institute in Secure Hardware and Embedded Systems (RISE) led by CSIT at Queen's University Belfast and including the University of Cambridge and the University of Bristol.
The goal of FutureTPM is to design a quantum-resistant (QR) Trusted Platform Module (TPM) by designing and developing QR algorithms suitable for integration in a TPM. The algorithm design will be accompanied with implementations and performance and security evaluations, as well as formal security analyses in the full range of TPM environments: hardware, software and virtual. The lead users will be in the online banking, activity tracking and device management domains, which will provide environments and applications to validate the FutureTPM framework.
Security, privacy and trust in a computing system are usually achieved using tamper-resistant devices to provide core cryptographic and security functions. The TPM is one such device and provides the system with a root-of-trust and cryptographic engine. However, to sustain enhanced security posture, it is crucial that the crypto functions in the TPM are not merely secure for today but will also remain secure in the long-term against quantum attacks.
FutureTPM will address this challenge by providing a new generation of TPM solutions, incorporating robust and provably-secure QR algorithms. Research on QC has drawn enormous attention from governments and industry; if, as predicted, a large-scale quantum computer becomes a reality within the next 15 years, existing public-key algorithms will be open to attack. Therefore, a smooth transition to QR cryptography is required, since history shows that any significant change takes time and requires theoretical and practical research before adoption. A key strategic objective of FutureTPM is to contribute to standardization efforts at EU level within TCG, ISO and ETSI. The consortium consists of high caliber industrial and academic partners from across Europe combining QR crypto researchers with TPM developers. Because the TPM shares many functions in common with other widely-used devices--such as HSMs or TEEs--the FutureTPM solution is expected to benefit them as well.
Project partners include:
The University of Birmingham will be contributing research into security requirements and properties, post-quantum cryptography, security verificationa and analysis, and run-time vulnerability analysis.
The FutureTPM project has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 779391.
StatVerif is an automated verifier for security protocols which extends ProVerif with constructions which may used to model security protocols with global mutable state. In particular, the kind of security properties which may be verified is the same as ProVerif, and the syntax of StatVerif processes is an extension of the syntax for ProVerif processes with constructs for modelling states.
Employers often want to verify an applicant's academic credentials. Currently, this requires manual processes by institutions to trace records and verify degrees. This approach is slow, subject to individual institutions' record-keeping, and exposes graduates to a lack of privacy concerning when and by whom their credentials are being authenticated. Blockchain offers one solution to this problem. As an "append-only whiteboard in the sky", the blockchain ledger is a verifiable source for cryptographically proving the existence of official documents. Employers can be given an access code by a graduate that enables them to authenticate credentials without having to involve the awarding institution. Similarly, the institutions need only add their records to the Blockchain, saving time and resources. While a blockchain system is designed for transparency, this system also adds a component of privacy for graduates, as their former institution need not be made aware that potential employers are making a request to validate their certificates. For sensitive applications, and for enhancing privacy in general while also improving functionality, the blockchain approach is an effective solution to the problem of credential authentication.
As part of an international collaborative effort, our researchers are running a pilot scheme at the University of Birmingham to demonstrate the potential of this application of Blockchain technology. If it proves successful, it is hoped that more institutions and employers will embrace the system, increasing the verifiability of credentials between institutions, between countries, and potentially beyond academic achievement to other areas that may need credentials to be authenticated in an accessible and automated way.
Electronic voting protocols should achieve two antagonistic security goals: privacy and verifiability. Additionally, they must be practical, from a usability, operational, and effciency point of view. Privacy can be expressed via several, increasingly demanding security properties:
Building on the Helios scheme, and its variant Belenios, we propose a new voting scheme, BeleniosRF, that offers both receipt-freeness and end-to-end verifiability. It is receipt-free in a strong sense, meaning that even dishonest voters cannot prove how they voted. We provide a game-based definition of receipt-freeness for voting protocols with non-interactive ballot casting, which we name strong receipt-freeness (sRF). To our knowledge, sRF is the first game-based definition of receipt-freeness in the literature, and it has the merit of being particularly concise and simple. Built upon the Helios protocol, BeleniosRF inherits its simplicity and does not require any anti-coercion strategy from the voters. We implement BeleniosRF and show its feasibility on a number of platforms, including desktop computers and smartphones.
This research was presented at ACM CCS 2016.
Generally speaking, a cryptographic protocol is an algorithmic procedure that enables to perform a certain task under certain requirements, while assuring that malicious attempts to abuse the performance of this task are unsuccessful. For instance, an encryption scheme allows two parties to communicate over a public channel while attaining privacy; a digital signature scheme provides authenticity, integrity and non-repudiation for digital documents.
To devise a way to prove formally that a given cryptographic protocol is secure has required (and it is still requiring) a lot of effort from researchers. A fundamental set of techniques developed to solve this question have led to the so-called provable security or reductionistic security paradigm. This paradigm can be explained as follows: take some cryptographic goal, like achieving privacy via encryption. The first step is to make a formal adversarial model and define what it means for a scheme to be secure, i.e. which are the functionalities that the scheme should provide when it is fairly used, and on the other hand, which are the functionalities that illegitimate users should not be able to perform. Then, a particular scheme, is shown to be sound via a reduction. Such a reduction implies that the only way to defeat the protocol in that model is to break an underlying atomic and more simple primitive. The latter problem should be known or be generally regarded as infeasible to break.
Modern automotive vehicles have several wireless interfaces, and are interconnected with various devices and with the internet. This connectivity adds great functionality but it also introduces a number of security and privacy threats. This project focuses on improving the security of the next generation electronic vehicles. Working in conjunction with Jaguar Land Rover, the research is developing optimized implementations of cryptographic primitives and protocols for time critical automotive applications.
From the point of view of computer security, there are several criteria that any electronic voting protocol should ideally meet. With regards to the integrity of the ballot casting process, we have individual verifiability, which allows voters to check whether his vote has been cast as intended and contributes to the announced results; and universal verifiability, which ensures that the outcome of the election was correctly calculated from the individual votes, and that this is verifiable by any observer.
Another desirable property is that of vote confidentiality, i.e. that it should be impossible in practice to learn how a particular voter voted, unless this is revealed by the result (e.g. if the vote is unanimous).
An advanced anonymity property is called receipt-freeness, and guarantees that a voter cannot prove how she voted even if she reveals her secret materials to an adversary, including randomness and credentials. These properties shall help achieving the goal of coercion-resistance, whereby powerful attackers are prevented from controlling and deciding how voters under coercion vote.
Electronic voting - especially remote voting over the internet - is very challenging to secure. Yet there is a growing call for internet voting to enable and encourage broader participation. However, such systems must ensure both privacy and verifiability to ensure that elections are legitimate and protected from corruption.
Du-Vote is a step towards tackling the problem of internet voting on user machines that are likely to have malware. Du-Vote is a new remote electronic voting protocol that eliminates the often-required assumption that voters trust general-purpose computers. This will enable secure internet voting on untrusted or even compromised hardware.
PRINCESS is part of a DARPA funded project, working in conjunction with the US R&D company Charles River Analytics. The research is developing techniques for adaptive software operating in uncertain environments, such as UUV control software. With the complex and constantly evolving technical ecosystems of contemporary software, adaptations need to verifiably correct in the context of repairing security, logical and performance-related vulnerabilities. These methods involve inferring the impact of evolution on application behaviour and performance, automatically triggering transformations that beneficially exploit these changes, and validating such transformations. The project aims to realise foundational advances in the design and implementation of complex software systems with increased robustness, agility and longevity.
Confidentiality from the Cloud Provider is an ongoing research project aimed at developing ways in which SME cloud service users can obtain the benefits of cloud computing without having to divulge their data to the cloud provider. So far the project has produced two systems:
ProVerif is a tool for automatically verifying cryptographic protocols to prove secrecy, authentication and equivalences. However, ProVerif over-approximates the adversary's power to enable verification of processes under replication. Unfortunately, this results in ProVerif reporting false attacks. This problem is particularly common in protocols whereby a participant commits to a particular value and later reveals their value. By using a compiler that inserts phase statements into a process, researchers in the Security and Privacy group introduced a method to avoid false attacks when analysing secrecy.
The paper and examples can be found here.
The monitoring of peer to peer file sharing: This work was the first to analyse the direct monitoring of illegal file sharing. Our findings include:
The full report, which includes an ethical consideration of the research, can be found here.
Since 1999, the University of Birmingham has been leading the development of the PRISM probabilisitic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilisitic behaviour. This tool can be used to analyse security protocols, as well as communication/multimedia protocols, randomised distributed algorithms, biological systems and others.
This collection of projects explores the Security and Privacy group's interest in how mutual infomration can be estimated and how information leakage can be measured in real systems. This includes:
Tools and software to support these projects can be found here.
We are surrounded by computerised systems, upon whose secure and reliable operation we are increasingly dependent. Yet flaws in these systems are common, from power plants to travel cards, and these come at high costs for individuals, companies and governments alike. So, rigorous, mathematically-sound techniques to check the security of computerised systems are essential. Security, though, is not absolute: we may only be able to guarantee that an attack on a system is possible with low probability, rather than impossible. Furthermore, system designs often need to trade off the degree of security or privacy offered against other practical concerns such as response time or power consumption. So, effective methods for the analysis of security also need to take these quantitative aspects into account.
This project developed fully-automated techniques to formally verify the correctness of security systems, to identify flaws in their operation, and to fix or optimise aspects of their design. This was achieved by bringing together techniques from several different areas:
Building upon recent advances in these fields, and upon existing efforts to create efficient and scalable verification methods, this project developed novel techniques to verify security systems, implement them in freely-available software tools and apply them to a variety of security applications, from electronic voting schemes to anonymous communication networks.
By learning about penetrating security systems, students can gain a practical knowledge of how they work as well as insights into attacks from an attacker's perspective. Our researchers have developed a virtual machine (VM) framework for cyber security education, which is used for courses offered at the University of Birmingham. This VM includes several capture the flag (CTF) style exercises that students can complete to support their learning:
More information - including the virtual machine, exercises and documentation - can be found here.