VOTEE: Voting on Trusted Execution Environments

Lead Research Organisation: University of Surrey
Department Name: Computing Science

Abstract

Bring your own device (BYOD) technologies, such as the Trusted Execution Environment (TEE) enabled by ARM's TrustZone, can isolate sensitive corporate software from personal applications on employee owned devices. These technologies are expected to feature widely in future Thales security products and in systems where BYOD may be offered as a user terminal option. This iCASE provides an opportunity to investigate and evaluate in depth the protection provided by TEE/TrustZone technologies using the example of eVoting.

Publications

10 25 50

Studentship Projects

Project Reference Relationship Related To Start End Student Name
EP/N509383/1 01/10/2015 30/09/2020
1652008 Studentship EP/N509383/1 01/10/2015 30/09/2019 Jorden Daniel Whitefield
 
Description Identified limitations in current standards specifications for the deployment of future connect transportation systems, e.g. Vehicle-2-anything (V2X) communication. To partially address the discovered limitations we have utilised trusted computing within vehicles, and enabled a shift of trust from the architecture to inside vehicles. An additional, finding has also been formal analysis on academic security protocols used for vehicle revocation. Revocation is the process of removing a bad/misbehaving vehicle from the network, thus ensures safe and healthy operation of the transportation system. From performing formal analysis on these protocols, we discovered an attack on authentication that would allow a vehicle to remain connected to the network as a legitimate entity.

Identified an attack in Direct Anonymous Attestation (DAA) through the use of formal analysis. DAA is a standardised set of operations originally developed for the Trusted Platform Module (TPM), and specified in ISO/IEC 20008 & ISO/IEC 11889. The analysis revealed that if the integrity of one TPM is compromised, then the security of all TPMs cannot be guaranteed.

More broadly, this research plays a role in future security of networks in the Internet of Things (IoT), and in particular vehicular networks. Notably our research contributes to the growing body of work in theformal analysis of security protocols, and standardised security schemes.
Exploitation Route The research is not limited to vehicular architectures, and the techniques are applicable to any device and secure communications.
Sectors Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software),Transport

 
Description IAA
Amount £47,961 (GBP)
Funding ID 15220193 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Academic/University
Country United Kingdom
Start 02/2018 
End 12/2018
 
Description IEEE Euro S&P 
Organisation ETH Zurich
Country Switzerland 
Sector Academic/University 
PI Contribution Formal modelling, generation of collaborative research ideas
Collaborator Contribution Domain expertise in formal verification of security protocols
Impact Produced paper "A Symbolic Analysis of ECC-based Direct Anonymous Attestation" IEEE Euro S&P
Start Year 2018
 
Description STM17 
Organisation Aalto University
Department Department of Computer Science
Country Finland 
Sector Academic/University 
PI Contribution Formal modelling, generation of collaborative research ideas
Collaborator Contribution Domain expertise in vehicular technology and Hardware systems
Impact Produced paper Formal Analysis of V2X Revocation Protocols presented at STM 2017
Start Year 2016
 
Description STM17 
Organisation University of Ulm
Department Faculty of Engineering, Computer Science and Psychology
PI Contribution Formal modelling, generation of collaborative research ideas
Collaborator Contribution Domain expertise in vehicular technology and Hardware systems
Impact Produced paper Formal Analysis of V2X Revocation Protocols presented at STM 2017
Start Year 2016
 
Description iFM16 
Organisation Heinrich Heine University Düsseldorf
Department Department of Computer Science
PI Contribution Expertise in CSP||B
Collaborator Contribution Expertise in tooling support
Impact Publication at Symbolic Reachability Analysis of B through ProB and LTSmin at iFM 2016
Start Year 2015
 
Description iFM16 
Organisation University of Twente
Department Faculty of Science and Technology
Country Netherlands 
Sector Academic/University 
PI Contribution Expertise in CSP||B
Collaborator Contribution Expertise in tooling support
Impact Publication at Symbolic Reachability Analysis of B through ProB and LTSmin at iFM 2016
Start Year 2015