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

今天的安全系统--带有超连接设备--可以任意跨越多个并发执行。因此，我们需要可靠的验证技术来捕获它们的无限大小。这种强大的方法已经被完善，以验证安全属性。但这些成熟的方法(例如，基于进程代数)不能在任意大的系统中健壮地检查丰富的隐私属性，例如用户的匿名性和与操作的不可链接性。随着我们周围对隐私的担忧不断升级，这个问题变得更加尖锐，业界也感受到了这一点。例如，在汽车领域，对联网汽车和有根有据的工具进行私人认证以检查其健壮性是至关重要的。我们的行业顾问VectorGB有限公司在他们的支持信中说：“一种正式的基于方法的方法来解决这些问题[……]有可能成为我们客户的‘游戏规则改变者’。”为了在隐私分析方面实现阶段性的改变，AutoPaSS“跳出了框框”。AutoPaSS将创造新的技术来验证安全系统，通过利用人工智能和分析自主系统中传统的逻辑。此外，这些受人工智能启发的逻辑最近在安全/隐私验证方面也显示出了希望。因此，我们的新方法将依赖于这些逻辑的可表现性，并允许我们在无限大小的安全系统的自动验证过程中检查丰富的隐私要求，如匿名性和不可追踪性。简而言之，AutoPaSS将研究和开发新的、强大的基本方法和软件工具，用于对任意规模的现代计算机和通信系统中的安全，特别是隐私进行自动、正式的分析。而且，AutoPaSS将在这些方面成为游戏规则的改变者，因为它将：(I)能够自动检查更丰富的隐私属性的“现实生活”表达；(Ii)在无限大的系统中做到这一点；(Iii)将增强的威胁模型正式化并使用增强的威胁模型，这些模型超越了通常使用的系统级攻击，并忠实地考虑了网络/通信的细节，所有这些都没有目前可能的那么严格。AutoPaSS将建立在成熟的系统验证方法基础上，并将使用应用的非经典逻辑。让我们来解决更多与AutoPaSS相关的问题。--英国的战略强调了对5G发展的大力支持。但是，不同的5G通信原语或不断变化的5G网络拓扑是否会影响5G系统的安全和隐私，或者它们的分析？当前的安全验证方法通常抽象出网络方面，使用的模型只考虑劫持抽象连接的应用层攻击者。相反，通过利用基于逻辑的分析(即参数化模型检查)中的技术，AutoPaSS将开发出对手模型，这些模型不仅忠实地考虑应用程序威胁，而且还考虑到各种通信环境，包括5G中新出现的通信环境。这将为现代通信系统中的安全和隐私需求提供变革性的方法，特别是在5G、IoT和V2X(车辆到车辆+车辆到基础设施通信)系统中，在这些系统中，AutoPaSS有其行业支持的用例。--最后，AutoPaSS如何尽快实施必要的安全变化？多学科伙伴关系。AutoPaSS联合了GCHQ认可的萨里网络安全中心和萨里的5G创新中心，并得到了英国和海外的资深学者以及两家工程巨头泰利斯和VectorGB的积极建议。我们的合作伙伴还提供和支持我们在5G、物联网和V2X方面的实际使用案例。AutoPass将向我们的顾问附属机构和相关标准化机构提出建议：针对5G的3GPP、针对物联网的LoraAlliance和针对V的ISO小组

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