Verifiably Correct Swarm Attestation

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.