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

点击翻译按钮获取中文摘要

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