Holistic Design of Secure Systems on Capability Hardware (HD-Sec)

网络安全威胁正在对企业和更广泛的社会造成损害，如果不加以控制，这些威胁将继续增长。设计糟糕的软件是网络安全漏洞的一个重要来源。当前的软件开发实践严重依赖于迭代构建-测试-修复软件正确性的方法，虽然软件测试是必要的，但它非常耗时，而且通常是不完整的。迭代构建-测试-修复方法的另一个弱点是，它经常导致设计错误在开发生命周期中引入很久之后才被发现——一旦发现，修复它们就非常昂贵。形式化方法是一组基于数学的技术，用于软件的设计和验证，它比构建-测试-修复更严格、更系统，从而导致更好的软件设计，减少错误和漏洞。我们的愿景是将安全系统开发从容易出错的、迭代的构建-测试-修复方法转变为构建正确性（CxC）方法，在这种方法中，正式的方法指导软件设计，使其通过构建满足其规范。其影响将是降低总体开发成本，同时提高安全关键系统的可信度。系统是由人设计并由人使用的。对于许多软件开发人员来说，使用形式化的方法是具有挑战性的，我们将开发减少部署障碍的工具。我们的工具将支持开发人员与更广泛的涉众接触，以引出并验证需求。许多安全系统依赖于对可信用户和不可信用户的行为的假设，但这些假设通常不被清楚地理解或定义。我们的研究将纳入对用户数据和行为的正式约束，以及在建模和验证中由用户行为导致的数据完整性漏洞。即使软件被证实是正确的，它也很可能运行在容易受到网络攻击的硬件上，因为内存保护不佳。今天的开放连接计算平台允许大规模地利用硬件漏洞，功能硬件已被提出作为减少硬件漏洞的一种方法。功能硬件（如CHERI体系结构）提供了一系列内存保护特性，以强制执行安全的数据操作并避免对数据的错误或恶意操作。当使用形式化方法时，我们开发软件来执行安全的数据操作，因此，原则上，不需要额外的硬件执行。然而，安全开发的软件仍然可能在其他代码可能意外或恶意违反数据访问规则的环境中执行，这可能会破坏安全开发的代码。通过使用功能硬件，我们可以在其他代码上执行安全的数据操作，从而避免了担心我们无法控制的代码的干扰。我们的项目将通过开发高级设计抽象来将功能硬件特性合并到正式的设计方法中，这些抽象捕获适合在更高抽象级别上进行设计和验证的数据操作的属性。我们的研究将得到一系列安全关键工业案例研究的指导和验证，并得到我们的工业合作伙伴（空客、Arm、Altran、AWE、伽罗瓦、L3Harris、诺斯罗普·格鲁曼、泰雷兹）的支持。HD-Sec的主要成果将是：支持CxC方法设计安全系统的集成工具链。健全的高级抽象，有助于在软件设计中利用功能硬件。使用我们的CxC工具设计并运行在功能硬件上的功能原型应用程序

Cybersecurity threats are causing damage to business and wider society and, if left unchecked, these threats will continue to grow. Poorly designed software is a significant source of cyber security vulnerabilities. Current software development practice relies heavily on an iterative build-test-fix approach to software correctness and, while testing of software is essential, it is very time-consuming and usually incomplete. A further weakness of the iterative build-test-fix approach is that it often results in design faults being discovered long after they were introduced in the development lifecycle - making them very expensive to fix once discovered. Formal methods are a body of mathematically-based techniques for design and verification of software that are more rigorous and systematic than build-test-fix, leading to better software designs with reduced bugs and vulnerabilities. Our vision is the transformation of security system development from an error-prone, iterative build-test-fix approach to a correctness-by-construction (CxC) approach whereby formal methods guide the design of software in such a way that it satisfies its specification by construction. The impact of this will be to reduce overall development costs, while increasing trustworthiness, of security-critical systems. Systems are designed by humans and used by humans. Formal methods are challenging to use for many software developers we will developed tools that reduce barriers to their deployment. Our tools will support developers to engage with wider stakeholders to elicit and validate requirements. Many secure systems rely on assumptions about the behaviour of trusted and untrusted users but often these assumptions are not clearly understood or defined. Our research will incorporate formal constraints on user data and actions and vulnerabilities in data integrity resulting from user behaviour in modelling and verification. Even if software has been verified correct, it is likely to be running on hardware that is vulnerable to cyber-attack because of poor memory protection. Today's open connected computing platforms allow hardware vulnerabilities to be exploited at scale and capability hardware has been proposed as an approach to reducing hardware vulnerabilities. Capability hardware, such as the CHERI architecture, provides a range of memory protection features, to enforce secure data operations and avoid incorrect or malicious manipulations of data. When using formal methods, we develop software that enforces secure data operations and thus, in principle, additional hardware enforcement is not required. However, securely-developed software is still likely to be executing in a context in which other code may be accidently or maliciously violating data access disciplines which would undermine the securely-developed code. By using capability hardware, we get enforcement of secure data operations on other code, avoiding the need to worry about interference by code over which we have no control. Our project will incorporate capability hardware features in to the formal design approach by developing high level design abstractions that capture properties of data operations appropriate for designing and verifying at higher abstraction levels. Our research will be guided and validated by a range of security-critical industrial case studies with support from our industrial partners (Airbus, Arm, Altran, AWE, Galois, L3Harris, Northrop Grumman, Thales). Key outcomes of HD-Sec will be:. An integrated toolchain to support the CxC approach for design of security systems. Sound high-level abstractions that facilitate exploitation of capability hardware in software design. A functioning prototype application designed using our CxC tools and running on capability hardware