Research Areas

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.

Applied Cryptography

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.

Formal Verification

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.

Wireless Technology

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.

Embedded Devices and IoT Security

From consumer devices in our homes to critical national infrastructures, the need for security is becoming increasingly embedded in our society. As more and more of our daily lives is technologically mediated, there is the need to ensure that our devices, systems and information remains secure. Our researchers use both destructive and constructive methods to test current systems and fix security vulnerabilities.

Automotive Security

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.

E-Voting

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 Security

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.

Security and Privacy for Society

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.

Cyber Security Education

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.

Projects

Lock It and Still Lose It - on the (in) Security of Automotive Remote Keyless Entry Systems

Flavio Garcia and David Oswald

While most automotive immobilizer systems have been shown to be insecure in the last few years, the security of remote keyless entry systems (to lock and unlock a car) based on rolling codes has received less attention. In this paper, we close this gap and present vulnerabilities in keyless entry schemes used by major manufacturers. In our first case study, we show that the security of the keyless entry systems of most VW Group vehicles manufactured between 1995 and today relies on a few, global master keys. We show that by recovering the cryptographic algorithms and keys from electronic control units, an adversary is able to clone a VW Group remote control and gain unauthorized access to a vehicle by eavesdropping a single signal sent by the original remote. Secondly, we describe the Hitag2 rolling code scheme (used in vehicles made by Alfa Romeo, Chevrolet, Peugeot, Lancia, Opel, Renault, and Ford among others) in full detail. We present a novel correlation-based attack on Hitag2, which allows recovery of the cryptographic key and thus cloning of the remote control with four to eight rolling codes and a few minutes of computation on a laptop. Our findings affect millions of vehicles worldwide and could explain unsolved insurance cases of theft from allegedly locked vehicles.

View full paper here

This high-profile research received a great deal of attention in international media:

BeleniosRF: A Non-Interactive Receipt-Free Electronic Voting Scheme

David Galindo

Electronic voting protocols should achieve two antagonistic security goals: privacy and veri ability. Additionally, they must be practical, from a usability, operational, and effciency point of view. Privacy can be expressed via several, increasingly demanding security properties:

  • Basic ballot privacy guarantees that no one can learn how a voter voted.
  • Receipt-freeness ensures that a voter cannot prove to anyone how she voted. While privacy protects honest voters, receipt-freeness aims at protecting vote privacy even when voters willingly interact with an attacker.
  • Coercion-resistance should allow an honest voter to cast her vote even if she is, during some time, fully under the control of an attacker. Coercion-resistance typically requires revoting.

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 veri ability. It is receipt-free in a strong sense, meaning that even dishonest voters cannot prove how they voted. We provide a game-based deffnition 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.

View full paper here

Design and Analysis of Cryptographic Protocols

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.

Engineering for Cyber Security and Privacy

Mark Ryan

Devices such as motor cars, thermostats, door locks, traffic lights, trains, power plants, TVs, and dialysis machines are rapidly becoming internet-enabled, resulting in cyber-physical systems that blend the digital and physical worlds. Confidential data will be collected by these devices, and processed on an unprecedented, massive scale, for multiple purposes. This revolution carries risks for all the stakeholders involved. The primary risk is that the devices and data could be appropriated and misused by criminals, for financial or other kinds of gain. Another risk is more subtle, and arises because different stakeholders in the ecosystem may have different requirements or expectations about how the data is used. Data that is collected for broadly legitimate purposes may also be used for other purposes that are not considered legitimate by some of the stakeholders; for example, it might be used for insurance profiling. A third risk arises because users do not usually consider security as their primary goal, but rather as a feature that should accompany whatever it is they are trying to achieve. Security technologies therefore need to be designed to provide intuitive and natural user experiences, not to put obstacles in users' ways. The research consists of three main areas:

IoT services with multiple stakeholders

  • Controlling access to IoT
  • Removing the need for trusted parties
  • Considering multiple stakeholders: industry, government, user

Data and confidentiality middleware in the IoT

  • Controlling access to and processing of data
  • Preserving privacy while opening up big data for societal use
  • Enabling IoT devices and infrastructure to access data securely

IoT connectivity architectures and protocols

  • Ensuring the security of IoT communication
  • Developing new methods of securing devices, services and users
  • Protecting devices and data from internet-based attack

Other areas of concern for the research include authentication and authorisation, distributed ledgers, policy-carrying data, protocol analysis and user experience.

Automated Protocol Learning and Vulnerability Detection for TLS, WPA and the IoT

Tom Chothia, Erik Tews and Flavio Garcia

Having many small and embedded systems connected to the Internet that interact with each other is an upcoming technology trend that will increase in the near future. Such devices might be integrated in today’s household items, integrated in a smart city, manage logistics and transport or record medical or environmental data around their respective owner. Many of those devices will acquire, store, forward, process or display sensitive data or control critical infrastructure. Security of those devices needs to be addressed accordingly.

The mobility and diversity of Internet-of-Things (IoT) devices makes it hard to know exactly what implementations of security protocols are being used and to what extent these are actually secure. Today, the security of these devices is evaluated by highly trained analysts in a manual and very time consuming process. Due to the large variety of devices that will be used in the near future, this process is infeasible to conduct for every device that may be deployed in an organisation.

This proposal is based on the premise that there are so many, highly mobile, IoT devices that tracking and testing all devices on a network by hand will quickly become infeasible for most organisations. Therefore, we urgently need automated methods of identifying devices with known security vulnerabilities and discovering new vulnerabilities in the protocols these devices use.

To succeed, a common building ground for security analysis is required. Many devices that are used today use the WPA or WPA2 protocol to secure their network access when they areWi-Fi enabled. The TLS protocol is often used to secure the communication link to other devices, cloud services and mobile apps. When a Wi-Fi device is used in an enterprise environment, WPA and TLS are often used in conjunction in the WPA-Enterprise protocol suite. Additionally, IoT devices may use their own ad-hoc protocols. Any solution in this area must be able to deal with all of these possible alternatives.

This project will include the following technical approach:

  • Learning broadcast protocols
  • Large scale analysis of IoT devices and mobile apps
  • Security analysis of Wi-Fi protocols.
  • Fingerprinting, learning and monitoring devices on a network

Checking the Security of All the Things

Tom Chothia and Flavio Garcia

The mobility and diversity of Internet-of-Things (IoT) devices makes it hard to know exactly what implementations of security protocols are being used and to what extent these are actually secure. This is particularly true of TLS, WPA and Bluetooth, the protocols most commonly used in IoT to set up secure connections. The proliferation of devices also makes it hard for experts to check and keep track of every device that is used within an organisation.

We are developing a framework that will automatically check the security of IoT devices that use TLS, WPA or Bluetooth. This framework will build on our past research on TLS, in which we have discovered major vulnerabilities in the way TLS is used in banking apps, and separately we found serious vulnerabilities in major TLS libraries (e.g. CVE-2014-6593).

Our framework will offer Wi-Fi and Bluetooth connections, and when a device tries to connect, the framework will run a range of tests to check if certificates and keys are handled correctly. It will then use automated learning techniques to determine exactly how the protocols are implemented, and look for flaws in how the implementation handles, for instance, messages out of order, or badly formed messages.

This method goes beyond basic fuzzing of the device because we learn the entire “state machine” of the protocol allowing us to learn how the device reacts to any combination of commands. Our previous work using these methods has found serious vulnerabilities in major TLS libraries. Due to the black-box testing nature of our framework no special access is required to the device or its source code, and any device using one of the supported protocols can be tested.

The embedded nature of IoT devices also makes it difficult to check which libraries are used. So, for instance, if a vulnerability is found in OpenSSL 1.0.1g, organisations currently have no easy way to say which of its IoT devices are using this implementation. Our work makes it possible to fingerprint the implementation and version of the protocols being used on a device.

Therefore, as well as looking for flaws, our framework will make it possible for organisations to keep track of the particular implementations of protocols used on the devices on their network. This information can then be used to quickly determine which devices might be affected when new vulnerabilities are reported in the future. The types of devices we are testing include:

  • IoT home hubs
  • Thermostats
  • Smart water meters
  • Internet doorlocks
  • Video doorbells
  • Home alarm systems
  • Baby monitors
  • Fitness trackers
  • Online shopping tools

BaDSeED: Backdoor Detection Systems for Embedded Devices

Flavio Garcia and Tom Chothia

We live surrounded by an increasing number of embedded devices with computing and (wireless) networking capabilities. We rely on these embedded devices for many critical applications and infrastructure. In most cases, the manufacturing and programming of microcontrollers and field programmable gate arrays (FPGAs) used in embedded devices is outsourced. Indeed, most of these devices are made in factories on the other side of the planet - well beyond our control. But can we trust them?

A key problem is that detecting the presence of a backdoor on a chip is an extremely challenging, expensive and time-consuming task. This project addresses the problem of detecting backdoors in embedded devices. Specifically, building on methods recently developed by the Security and Privacy group to extract the firmware from embedded devices, our researchers are developing novel techniques to test the software and firmware of embedded devices for the presence of backdoors.

For more information on the technical approach of the research, see here.

Protecting Contactless EMV Cards from Replay Attacks

Tom Chothia and Flavio Garcia

Our research shows that its possible to use NFC mobile phones to relay the signals from a Visa payWave or Mastercard PayPass bank card to a payment terminal. This can be done even if the card is inside a wallet or a purse, so making it possible to wirelessly pick pocket someone and charge purchases to their bank cards without their knowledge.

The designs of the current payment protocols make it hard to stop this kinds of attack; all of the message can either be cashed by the relay or take an unpredictable amount of time. In fact, with the current protocol we can relay the signals over any distance and we have relayed a signal from a card in New York and Puerto Rico to a payment terminal in Birmingham UK and made a successful transaction.

We propose a very small change to the payment protocol that will stop these kinds of attacks. By moving two of the message payloads, we can add a message to the protocol that cannot be cached and takes a very predictable amount of time. So this message can be timed to stop relay attacks which use cheap, easily available equipment, such as mobile phones.

To demonstrate the speed of the relay app we developed, we relayed the signals from a bank card from New York to a payment terminal in Birmingham, as shown in the video above (the card in the video has now been cancelled). We also demonstrated the relay live on stage at the Financial Cryptography Conference 2015 in Puerto Rico by relaying the card signals to Birmingham. We suggest protocol changes that will make successfully relaying the card signals using a mobile phone impossible over any distance.

Details of the traces can be found here.

The formal protocol models used in the research can be found here.

The research paper can be found here.

Real-World Implementation Attacks and Side-Channel Analysis

David Oswald

With the increasing reliance on embedded devices arises the need to thoroughly examine the related security mechanisms. Malicious adversaries can cause severe financial losses, e.g., due to IP counterfeit, industrial espionage, or fraudulent payment transactions, but also endanger material and even human lives, e.g., in case of vehicles, medical devices, or industrial machinery. Hence, many embedded devices incorporate protection mechanisms, often involving cryptographic functionality. To evaluate the security level of such implementations, a purely mathematical point of view is not sufficient.

Classical cryptanalysis considers an algorithm as an ideal black-box construct, however, for real-world devices, this assumption does not hold. The actual hardware or software realization of a cryptographic primitive is subject to implementation attacks that utilise physical properties to break analytically secure schemes like AES, 3DES, or RSA. Active fault injection techniques allow to extract secret information by disturbing the cryptographic computation, e.g., exposing the device to over and undervoltages or UV-C light. In contrast, passive side-channel analysis is based on monitoring the behavior of the target device, e.g., by measuring the power consumption or EM emanation.

This "destructive" research project examines real-world situations by staging attacks on the hardware level (physical "side channels"). By testing and breaking real-world devices, security vulnerabilities can be identified that informs "constructive" research into designing more secure systems. Devices that were hacked include:

  • DESFire RFID smartcard
  • Electronic locking systems
  • Yubikey login token
  • Maxim anti-counterfeit ICs
  • Altera FPGAs
  • Automotive key fobs

Following testing via implementation attacks, security vulnerabilities can be identified, reported to the manufacturer and fixed. This leads to the "constructive" side of the research in developing new ways of designing secure devices.

Industrial Control Systems: SCEPTICS

Tom Chothia, Mark Ryan, Mihai Ordean

Industrial Control Systems underpin almost all aspects of everyday life, from power networks to transport systems. Our research works with national organisations in energy and railways to perform a detailed security analysis of their systems. We are looking for possible points of cyber attack and building a better understanding of the impact of possible failures. This will lead to better security for these systems of critical infrastructure. Based on this research, we work alongside industrial partners to generalise our methods into business processes that other owners of industrial control systems can use to help ensure their systems are safe from cyber attacks.

In A SystematiC Evaluation Process for Threats to Industrial Control Systems, our researchers are collaborating with colleagues in Electrical, Electronic and Computer Engineering at the University of Birmingham, as well as with the Rail Safety and Standards Board, National Grid, L-3 TRL and Parsons Brinckerhoff, to:

  • Create new frameworks for systematically analysing Industrial Control Systems
  • Performing detailed analyses of UK rail and energy networks
  • Identify possible modes of attack
  • Improve our understanding of the impact of weaknesses in critical infrastructures
  • Develop busineess solutions to security problems in these important systems

Embedded Security/Cryptography for Next Generation Vehicles

Flavio Garcia

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.

Immobilizer vulnerabilities

Flavio Garcia

An electronic vehicle immobilizer is an anti-theft device which prevents the engine of the vehicle from starting unless the corresponding transponder is present. Such a transponder is a passive RFID tag which is embedded in the car key and wirelessly authenticates to the vehicle. It prevents a perpetrator from hot-wiring the vehicle or starting the car by forcing the mechanical lock. Having such an immobilizer is required by law in several countries. This research has revealed several weaknesses across different immobilizers that would enable car-theives to override the immobilizer, often using only wireless communication.

Hitag2, introduced in 1996, is currently the most widely used transponder in the car immobilizer industry. It is used by at least 34 car makes and fitted in more than 200 different car models. Hitag2 uses a proprietary stream cipher with 48-bit keys for authentication and confidentiality. During our experiments we managed to recover the secret key and start the engine of many vehicles from various makes using a transponder emulating device, revealing several implementation weaknesses in the immobilizer units. The most serious attack recovers the secret key from a car in less than six minutes using ordinary hardware:

  • Stage one: read 136 authentication attempts by the car - 1 minute
  • Stage two: cryptanalytic computation - 5 minutes
  • Total attack time: 6 minutes
  • Gone in 360 seconds!

Megamos Crypto is a key fob used in one of the most widely deployed automotive electronic immobilizers. Our research reverse-engineered all proprietary security mechanisms of the key fob and found several weaknesses in its cipher as well as its usage and configuration. We developed three different methods of practical attacks that exploited the weaknesses to recover the key fob's 96-bit secret key:

  • Trivial denial of service attack: disable the secret key by flipping one bit
  • Partial key-update attack: guess and determine technique to overwrite one block at a time until the secret key is found
  • Weak-key attack: exploit the low entropy of the secret key, including the first 32 bits all being 0 and manufacturer-specific patterns

This research led to suggestions for mitigating some of the possible attacks, which knowledgable users can do themselves, including testing for and removing attackers' write access, as well as advice for car manufacturers in generating secret keys.

Security issues in electronic voting

Mark Ryan and David Galindo

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.

DuVote: Devices that are Untrusted used to Vote

Mark Ryan

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.

OpenHaven: an Open Hardware Authentication Token

Mark Ryan and Flavio Garcia

Highly available information networks are an increasingly essential component of the modern society. Targeted attacks are a key threat to the availability of these networks. These attacks exploit weak components in network infrastructure and attack them, triggering side-effects that harm the ultimate victim. Targeted attacks are carried out using highly distributed attacker networks called botnets comprising between thousands and hundreds of thousands of compromised computers. A key feature is that botnets are programmable allowing the attacker to adapt to evolve and adapt to defences developed by infrastructure providers. However current network infrastructure is largely static and hence cannot adapt to a fast evolving attacker.

In today's reality most general purpose computers and mobile devices are infected with malware. This project aims to develop techniques to mitigate or tolerate such infection: a considerable challenge. Malware on your computer means that everything you ever type or store in your computer is, in the worst case, immediately given to an adversary. The challenge in malware mitigation is to be able to perform secure computations under such stringent assumptions.

Several attempts as malware mitigation have been proposed for the restricted case of user-authentication to remote services. These proposals include two-factor authentication, where the user performs some computation on another device, such as a smartphone, and then types the response into the browser of the authenticating computer. However, as smartphones and computers become more integrated and synchronised, this solution is vulnerable to a situation in which coordinated malware infects both the phone and the computer.

Existing secure tokens are limited to user-authentication and very simple data-signing scenarios. They don't solve more general data authentication problems found in contract and document signing, e-voting, e-commerce and decryption. They are also proprietary and closed-source, making their security hard to evaluate, have significant usability, and are prohibitively costly to individuals and small companies.

Technical Approach

The OpenHaven project has four strands of research:

  1. Develop the hardware architecture and the basic software.
  2. Implement more complex protocols and build a basic prototype.
  3. Perform formal analysis in a rigorously defined attacker model.
  4. Implement countermeasures against side-channel attacks and rigorous testing.

The aim of Open Haven is to design, develop and produce a dedicated hardware authentication token that is:

  • open-design
  • open-source
  • cost-effective
  • user-friendly
  • reprogrammable
  • verified

The OpenHaven token can be used for authenticating users to web services, but also for authenticating data in applications like signing documents, signing mandates and instructions, e-commerce, and electronic voting. This will open up a range of possibilities for SMEs and individuals to develop cheap and immediately deployable solutions for a wide variety of user- and data-authentication problems.

CRYPTACUS: Cryptanalysis of ubiquitous computing systems

Flavio Garcia

The Security and Privacy group is contributing its expertise to the international CRYPTACUS project.

This project responds to the irrevocable change to the classical picture of computing systems in the wake of recent technological advances in hardware and software, in particular the pervasive and ubiquitous quality of an ever increasing range of devices. The objective of this Action is to improve and adapt the existent cryptanalysis metholodologies and tools to the ubiquitous computing framework. This covers four areas of cryptanalysis:

  1. cryptographic models
  2. cryptanalysis of building blocks
  3. hardware and software security engineering
  4. security assessment of real-world systems

The CRYPTACUS project establishes a network of complementary skills across areas of cryptanalysis, information security, privacy and embedded systems, allowing researchers to work together to produce outcomes that will directly help both industry stakeholders and regulatory bodies to increase security and privacy in ubiquitous computing systems, and thereby improve the protection of citizens in their everyday lives. For more information, see the CRYPTACUS pages on the European Cooperation in Science and Technology (COST) website.

PRINCESS - BRASS: Building Resource Adaptive Software Systems

Dave Parker

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

Mark Ryan

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:

  • ConfiChair is a cloud-based reviewing system for papers or proposals, allowing a variety of roles (call chair, author, reviewer, referee) to interact through a cloud-based system. In contrast with existing systems like EasyChair, EDAS, and Je-S, in ConfiChair the cloud service provider sees only encrypted text. It is not able to read the content of any of the documents or reviews or scores. Moreover, it is not able to link participants that are related; for example, it is not able to see that a given reviewer reviewed a proposal by a given author. We have already used automatic verification tools to verify the security of ConfiChair protocols.
  • Certificate Issuance and Revocation Transparency (CIRT) is a technique for managing public key certificates in a way which removes the requirement to trust certificate authorities. It provides a secure, usable and fully automatisable way for clients to obtain authentic copies of other clients' public keys. CIRT works by allowing certificate managers to provide cryptographic proofs of their correct behaviour. We are currently developing applications around secure messaging. We have begun using the automatic prover Tamarin to verify the security of CIRT protocols, but have hit a problem of insufficient memory. The Tamarin developers recommend a server with 32Gb.

Stopping false attacks in ProVerif

Tom Chothia

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.

Monitoring of peer to peer file sharing

Tom Chothia

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:

  • Massive scale monitoring of all of the most popular illegal downloads from the PirateBay has been taking place since 2009.
  • On average an illegal file sharer, using BitTorrent to download the most popular content, will be connected to and have there IP address logged within 3 hours of starting a download.
  • Poor collection methods mean the evidence of illegal file sharing collected by monitors may not stand up in court.

The full report, which includes an ethical consideration of the research, can be found here.

PRISM: Probabilistic Model Checker

Dave Parker

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.

More information, including tools, documentation and publications, can be found on the PRISM site:

Estimation of Information Leakage

Tom Chothia and Dave Parker

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:

  • Creating tools for estimating information leakage
  • Information leakage in Java programs
  • Probabilistic and statistical methods

Tools and software to support these projects can be found here.

Automated Game-Theoretic Verification of Security Systems

Dave Parker

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:

  • game-theoretic methods, to reason about the interactions between a security system and its potential attackers
  • automated verification and synthesis techniques, with a particular emphasis on quantitative aspects such as probability or resources usage.
  • Probabilistic and statistical methods

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.

e-Passport Security

Tom Chothia, Eike Ritter and Mark Ryan

The Basic Access Control (BAC) protocol, as used in e-Passports, is flawed. There is quite an elegant traceability attack against the protocol as implemented on French e-passports and a side-channel traceability attack against all other passports we looked at. Research in this area included:

  • Using destructive methods, a traceabilitiy attack that exposed a vulnerability in e-Passport RFID that would enable attackers to track a person's movements.
  • Formal analysis of the traceability attacks, including developing a framework for analysing unlinkability and anonymity as well as a detailed analysis the the French e-passport systems that preserve anonymity but not unlinkability, thus allowing a carrier of a French e-passport to be physically traced.
  • Linking to the group's work on information leakage, a statistical test for time-based information leakage in e-passports.

An Offline Capture The Flag-Style Virtual Machine for Cyber Security Education

Tom Chothia

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:

  • Students are set specific exercises to complete
  • On successfully completing a task, students obtain a flag or token
  • Students can submit these tokens to a dedicated website
  • Each student receives a different token
  • The website checks that the flag is genuine and has been submitted for the correct questions
  • The tokens can then be used for automatic marking or to assist the marking of written answers.

More information - including the virtual machine, exercises and documentation - can be found here.