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

今天的安全系统——使用超连接设备——可以任意地跨越许多并发执行。因此，我们需要可靠的验证技术来捕获它们的无界大小。这种强大的方法已经完善，以验证安全属性。但是，这些行之有效的方法（例如，基于过程代数的方法）在任意大的系统中无法健壮地检查丰富的隐私属性，例如匿名性和用户与操作的不可链接性。随着我们对隐私的担忧不断升级，这个问题变得更加严重，整个行业都感受到了。例如，在汽车领域，联网汽车的私有认证和完善的工具来检查其稳健性是至关重要的。我们的工业顾问，矢量GB有限公司，在他们的支持信中指出：“一个正式的基于方法的方法来解决这些问题……有可能成为我们客户的‘游戏规则改变者’。”为了实现其在隐私分析方面的阶段性改变，AutoPaSS“跳出框框思考”。自动驾驶系统将通过利用人工智能和分析自主系统中的传统逻辑，创造新的技术来验证安全系统。此外，这些人工智能启发的逻辑最近在安全/隐私验证方面也显示出了希望。因此，我们的新方法将依赖于这些逻辑的表达性，并允许我们在自动验证无限制大小的安全系统期间检查丰富的隐私需求，例如匿名性和不可追溯性。简而言之，AutoPaSS将研究和开发新的、强大的基础方法和软件工具，用于对任意大小的现代计算机和通信系统的安全性，特别是隐私进行自动、形式化分析。而且，AutoPaSS将在这些方面改变游戏规则，因为它将：(1)能够自动检查更丰富的、“现实生活中的”隐私属性表达；（II）在无边界大小的系统中这样做；（III）形式化和使用增强的威胁模型，超越通常使用的系统级攻击，忠实地考虑网络/通信的细节，所有这些都比目前可能的限制更少。AutoPaSS将建立在完善的系统验证方法上，作为基础，它将使用应用的、非经典的逻辑。让我们再回答一些与自动驾驶ass有关的问题。——英国战略强调大力支持5G发展。但是，不同的5G通信原语或不断变化的5G网络拓扑是否会影响5G系统的安全性和隐私性，或者影响它们的分析？当前的安全验证方法通常抽象了网络方面，使用的模型只考虑劫持抽象连接的应用层攻击者。相比之下，通过利用基于逻辑的分析技术（即参数化模型检查），AutoPaSS将开发对手模型，这些模型不仅忠实地考虑应用程序威胁，而且还考虑各种通信设置，包括5G中新兴的通信设置。这将为现代通信系统(特别是5G、物联网和V2X（车对车+车对基础设施通信）系统中的安全和隐私需求的工具辅助分析提供转型方法，在这些系统中，AutoPaSS拥有其行业支持的用例。——最后，自动驾驶ass如何尽快实施必要的安全更改？我们建立了跨领域的战略伙伴关系。AutoPaSS联合了政府通信总部认可的萨里网络安全中心和萨里5G创新中心，并得到了英国和国外高级学者以及泰雷兹和Vector GB两家工程巨头的积极建议。我们的合作伙伴还为我们在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