EPSRC logo

Details of Grant 

EPSRC Reference: EP/S024565/1
Title: AutoPaSS: Automatic Verification of Complex Privacy Requirements in Unbounded-Size Secure Systems
Principal Investigator: Boureanu, Dr IC
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Thales Ltd Vector
Department: Computing Science
Organisation: University of Surrey
Scheme: New Investigator Award
Starts: 01 July 2019 Ends: 30 June 2022 Value (£): 303,951
EPSRC Research Topic Classifications:
Networks & Distributed Systems Software Engineering
EPSRC Industrial Sector Classifications:
Communications Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
17 Jan 2019 EPSRC ICT Prioritisation Panel January 2019 Announced
Summary on Grant Application Form
Today's secure-systems --with hyper-connected devices-- span arbitrarily-many concurrent executions. So, we need reliable verification techniques that can capture their unbounded sizes. Such powerful methods have been perfected to verify security properties. But these well-established methods (e.g., based on process-algebra) fall short of robustly checking rich privacy properties, such as anonymity and un-linkability of users to actions, in arbitrarily-large systems. As privacy concerns escalate around us, this problem becomes more acute and it is felt by industry. For instance, in the automotive domain, private authentication of connected cars and well-founded tools to check its robustness is paramount. Our industrial advisor, Vector GB Ltd, in their support letter, states: "A formal methods-based approach addressing these [...] has the possibility to be a "game changer" for our customers."

To deliver its step-change in privacy-analysis, AutoPaSS "thinks outside the box". AutoPaSS will create new techniques for verifying secure-systems, by levering logics which are traditional in AI and in the analysis autonomous systems. Moreover, these AI-inspired logics have recently shown promise in security/privacy verification as well. So, our new methodologies will hinge upon these logics' expressivity and allow us to check rich privacy requirements such as anonymity and non-traceability during the automatic verification of unbounded-size secure systems.

In brief, AutoPaSS will investigate and develop new, robust foundational methodologies and software-tools for the automatic, formal analysis of security and, especially, privacy in modern computer and communication systems of arbitrary size. And, AutoPaSS will be a game-changer in these, in that it will:

(I) be able to automatically check richer, "real-life" expressions of privacy properties;

(II) do this in unbounded-size systems;

(III) formalise and use enhanced threat models, that go beyond the normally-used, system-level attacks and account faithfully for network/communications' specifics,

all these in ways less restrictive than currently possible.

AutoPaSS will build on well-established system-verification methodologies and, as foundations, it will use applied, non-classical logics.

Let us address some more questions relevant to AutoPaSS.

-- The UK's strategies underline significant support for the 5G development. But, do the different 5G communication-primitives or the changing 5G-network topologies impact the security and privacy of 5G systems, or their analysis?

Current approaches to security-verification generally abstract away the networking aspects, using models that only consider application-layer attackers who hijack abstract connections.

In contrast, by leveraging techniques from logic-based analysis (i.e, parameterised model checking), AutoPaSS will develop models of adversaries which faithfully account not just for application threats, but also for varied communication settings, including the new, emerging ones in 5G.

This would deliver transformational methodologies for the tool-assisted analysis of security and privacy requirements in modern communication systems, notably in 5G, IoT and V2X (vehicle-to-vehicle + vehicle-to-infrastructure communication) systems, in which AutoPaSS has its industry-backed use-cases.

-- Finally, how can AutoPaSS implement the necessary security changes as soon as possible?

We formed strategic, multi-disciplinary partnerships. AutoPaSS unites GCHQ-recognised Surrey Centre for Cyber Security and Surrey's 5G Innovation Centre, and it is actively advised by senior academics in the UK and abroad, as well as two engineering giants, Thales and Vector GB. Our partners also provide and support our real-life use-cases in 5G, IoT and V2X. AutoPass will make recommendations to our advisors' affiliates and relevant standardisation bodies: 3GPP for 5G, LoraAlliance for IoT, and ISO groups for V

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
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Summary
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