Verifiably Correct Swarm Attestation
Lead Research Organisation:
University of Surrey
Department Name: Computing Science
Abstract
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.
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.
Publications
Dongol B.
(2022)
Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement
in Leibniz International Proceedings in Informatics, LIPIcs
Le-Papin J
(2023)
Verifying List Swarm Attestation Protocols
Dalvandi S
(2021)
Verifying C11-style weak memory libraries
Doherty S
(2022)
Unifying Operational Weak Memory Verification: An Axiomatic Approach
in ACM Transactions on Computational Logic
Ahmadi S
(2022)
Proving Memory Access Violations in Isabelle/HOL
Semenyuk M
(2023)
Ownership-Based Owicki-Gries Reasoning
Title | Isabelle/HOL files for "Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies" |
Description | Isabelle/HOL files for the paper "Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies". Tested for Isabelle 2022. |
Type Of Technology | Software |
Year Produced | 2022 |
Impact | None to report. The artifact is a mechanised proof. |
URL | https://figshare.com/articles/software/Isabelle_HOL_files_for_Mechanised_Operational_Reasoning_for_C... |
Title | Isabelle/HOL files for "Ownership-Based Owicki-Gries Reasoning" |
Description | Isabelle/HOL files for "Ownership-Based Owicki-Gries Reasoning" accepted to SAC 2023. The theories have been tested on Isabelle 2022. |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
URL | https://figshare.com/articles/software/Isabelle_HOL_files_for_Ownership-Based_Owicki-Gries_Reasoning... |
Title | Isabelle/HOL files for "Unifying Operational Weak Memory Verification: An Axiomatic Approach" |
Description | Isabelle/HOL files for "Unifying Operational Weak Memory Verification: An Axiomatic Approach" to appear in ACM Transactions on Computational Logic. The proofs require Isabelle/HOL 2020. |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
URL | https://figshare.com/articles/software/Isabelle_HOL_files_for_Unifying_Operational_Weak_Memory_Verif... |
Title | Tamarin Models for "Verifying List Swarm Attestation Protocols" |
Description | Tamarin models and proofs of SIMPLE+ and its variations for the paper "Verifying List Swarm Attestation Protocols" to appear in WiSEC 2023. https://doi.org/10.1145/3558482.3581778 The proofs have been tested with Tamarin 1.6.1. |
Type Of Technology | Software |
Year Produced | 2023 |
Impact | None to report. The artifact is a mechanised proof. |
URL | https://figshare.com/articles/software/Tamarin_Models_for_Verifying_List_Swarm_Attestation_Protocols... |
Description | FDR models for the SEFM 2021 paper "Checking Opacity and Durable Opacity with FDR" |
Type Of Technology | Software |
Year Produced | 2021 |
Impact | None to report. The artifact is a mechanised proof. |
URL | https://figshare.com/articles/software/FDR_models_for_Checking_Opacity_and_Durable_Opacity_with_FDR_... |
Description | Isabelle/HOL files for "View-Based Owicki-Gries Reasoning for Persistent x86-TSO" published in ESOP 2022. |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
URL | https://figshare.com/articles/software/Isabelle_files_for_View-Based_Owicki-Gries_Reasoning_for_Pers... |