AutoPaSS: Automatic Verification of Complex Privacy Requirements in Unbounded-Size Secure Systems

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

Concerns around non-trivial privacy properties, which subsume anonymity, non-traceability of users/actions, un-linkability of users to their actions or "digital footprint", are frequent today, as personal-details in different shapes and contexts are used by a plethora of devices and applications.

AutoPaSS investigates, develops, and demonstrates new, transformational techniques and software-tools for the automatic, systematic and formal analysis of security and complex privacy requirements in ICT systems of arbitrarily-large size. To do this, it relies on applied, non-classical logics. AutoPaSS will be a game-changer in the landscape of automatic privacy-verification, in two ways: (a) by opening for robust analysis of "real-life", rich-expressions of privacy properties; (b) by doing this, in unbounded-size systems, in ways less restrictive than currently possible.

Moreover, the techniques intrinsic to AutoPaSS will open for transformational paradigms in threat-modelling for ICT systems. AutoPaSS will develop enhanced models of cyber-adversaries which faithfully account not just for the application-levels threats, but also the new and varied communication/network settings, e.g., reconfigurable networks as the upcoming 5G (5th generation networks) promises.

So, AutoPass will ultimately improve the dependability and privacy-preservation guarantees of rising and upcoming ICT. This will have direct benefit to the end users, resulting in better cyber-protection, as well as in increased confidence in the trustworthiness of these systems.

Of its broad applicability, we selected prominent ICT verticals for our use-cases: 5G, IoT (Internet-of-Things) and V2X (vehicle-to-vehicle + vehicle-to-infrastructure communication) systems. Thus, AutoPass analyses will contribute to faster and wider adoption of these emerging ICT, benefiting hardware manufacturers, service providers and many other businesses around these growing markets.

AutoPaSS ensures relevance and impact of technology through continuous engagement with industrial partners (Vector and Thales), spanning co-creation of use cases and exploitation. For instance, the verification-tool to be built in AutoPaSS will support technologies widely employed by Vector: the Communication Access Programming Language for V2X, and "AUTOSAR" - a standardisation initiative by leading automotive manufacturers and suppliers.

The avenues for industrial engagement is facilitated by our Advisory Board (AB), a stakeholders' consultation and dissemination workshop (which we will hold in Month 28), and our partners' networks. For instance, we will engage with: SAE's J30611 and ISO's working group 21432 - standardisation efforts addressing (automotive) cybersecurity; LoRa Alliance, -- owner of specifications for IoT; 3GPP - organisation standardising 5G. As such, planned outcomes of the project include the development of standardisation recommendations, to push the state of the art and the industry-standards in the areas of 5G, IoT and V2X.

For further commercial exploitation and technology-transfer, AutoPaSS will be active within the European Institute of Innovation and Technology (EIT) network, of which Surrey is a member.

We are also committed to public engagement. To this end, in Month 33, we will hold an outreach event to engage the public in AutoPaSS' findings. And, we will partake in public and corporate events devoted (among others) to cybersecurity, automotive technologies and smart networked things. Through Surrey's participation in the network of UK's Academic Centres of Excellence in Cyber Security Research and through our liaisons facilitated by the AB, AutoPass will deliver vertical impact to the 5G, V2X, IoT and cybersecurity sectors.

Academic impact will be delivered through targeting top-tier international journal and conferences in: cybersecurity (e.g., IEEE S&P), networks (e.g, IEEE IoT, INFOCOM), and distributed computing (e.g., DISC).