EPSRC logo

Details of Grant 

EPSRC Reference: EP/V038915/1
Title: Verifiably Correct Swarm Attestation
Principal Investigator: Dongol, Professor B
Other Investigators:
Treharne, Professor H Dash, Dr SK Chen, Professor L
Researcher Co-Investigators:
Project Partners:
ARM Ltd Nanyang Technological University SRI International Inc
Thales Ltd
Department: Computing Science
Organisation: University of Surrey
Scheme: Standard Research
Starts: 04 October 2021 Ends: 03 October 2024 Value (£): 514,155
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Aerospace, Defence and Marine Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
10 Feb 2021 Cross-RI PaCCS 2020 prioritisation panel Announced
Summary on Grant Application Form
Attacks such as Stuxnet have shown that malware can cause widespread damage in critical devices, industrial control systems and national infrastructure. The 2019 global cost of cyber-crime is estimated to be over $500 billion; 30% of these are estimated to be malware-based attacks. As digital devices become more complex, connected and commonplace, the frequency and ferocity of such attacks is only likely to increase.

What can be done to protect from such attacks? One solution is the use of attestation services, which provides a mechanism for establishing a trust relationship between a verifier and prover. Attestation is used in a wide range of commercial deployments (e.g., Android Key Attestation, Azure Cloud Attestation, Samsung Knox, Windows Server etc), where devices are required to authenticate their identity, ensure the integrity and trust of the system software, and certify that they are running a trusted code base.

There are many forms of attestation providing services ranging from static (e.g., boot time) to dynamic (e.g., run-time) guarantees. We are interested in remote attestation, where a verifier checks the internal state of a prover on a different machine across a network. Remote attestation has many applications in future systems involving SMART, internet of things (IoT) and other embedded devices, however, also suffers from scalability issues. Therefore, researchers have developed swarm attestation services that are designed attest a large number of medium/low-end devices. Here, protocol designers must address issues such as device heterogeneity, allowing seamless integration and security across different types of hardware (e.g., smart sensors, car navigation systems, routers, etc).

Given a particular implementation of a protocol, how can one ensure that the system is correct, i.e., works as intended by the protocol designer? Our work will consider formal verification of the attestation protocols, which allows one to prove correctness using formal logic and mathematically rigorous arguments. Formal verification will be applied to top-level swarm attestation protocols, and we use a correct-by-construction methodology to develop executable implementations. Then simulation will be used to show applicability of the swarm attestation protocols across real-world applications; our case studies include a vehicular simulation involving intelligent transport systems and a industrial control system developed in collaboration with our project partners.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:  
Further Information:  
Organisation Website: http://www.surrey.ac.uk