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

网络安全威胁正在对企业和更广泛的社会造成损害，如果不加以遏制，这些威胁将继续增长。设计不佳的软件是网络安全漏洞的一个重要来源。当前的软件开发实践在很大程度上依赖于迭代的构建-测试-修复方法来确保软件的正确性，虽然软件测试是必不可少的，但它非常耗时，而且通常是不完整的。迭代构建-测试-修复方法的另一个缺点是，它经常导致在开发生命周期中引入设计错误很久之后才发现它们--一旦发现它们，修复它们的成本就非常高。正式方法是一系列基于数学的软件设计和验证技术，比构建-测试-修复更严格和系统，从而实现更好的软件设计，减少错误和漏洞。我们的愿景是将安全系统开发从容易出错的迭代构建-测试-修复方法转变为按构建正确性(CXC)方法，在这种方法中，形式化方法指导软件的设计，使其通过构建满足其规范。这样做的影响将是降低安全关键系统的总体开发成本，同时增加可信度。系统是由人类设计并由人类使用的。对于许多软件开发人员来说，使用正式的方法是具有挑战性的，我们将开发工具来减少他们部署的障碍。我们的工具将支持开发人员与更广泛的利益相关者接触，以得出并验证需求。许多安全系统依赖于对受信任和不受信任用户的行为的假设，但这些假设往往没有被清楚地理解或定义。我们的研究将纳入对用户数据和操作的正式约束，以及用户在建模和验证中的行为导致的数据完整性漏洞。即使软件已经被验证正确，它也很可能运行在容易受到网络攻击的硬件上，因为内存保护不力。当今的开放互联计算平台允许大规模地利用硬件漏洞，而功能硬件已被提出作为减少硬件漏洞的一种方法。诸如Cheri架构之类的功能硬件提供了一系列内存保护功能，以实施安全的数据操作并避免不正确或恶意的数据操作。在使用正式方法时，我们开发实施安全数据操作的软件，因此，原则上不需要额外的硬件实施。然而，安全开发的软件仍然可能在其他代码可能意外地或恶意地违反数据访问规则的环境中执行，这将破坏安全开发的代码。通过使用功能硬件，我们可以在其他代码上强制执行安全的数据操作，从而避免担心我们无法控制的代码的干扰。我们的项目将通过开发高级设计抽象来将功能硬件功能合并到正式设计方法中，这些抽象捕获适合于在更高抽象级别进行设计和验证的数据操作的属性。我们的研究将以一系列安全关键行业案例研究为指导和验证，并得到我们的行业合作伙伴(空中客车、ARM、Altran、AWE、Galois、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