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

Cybersecurity threats are causing damage to business and wider society and, if left unchecked, these threats will continue to grow. A key objective of the UK Government National Cyber Security Strategy is the continued growth of the UK cyber security industry, underpinned by world-leading scientific research and development. Our project will apply UK research excellence in cyber security and Correctness-by-Construction (CxC) software design and to pursue the Government's cyber strategy and improve industrial standards, thus contributing to future UK cyber security and economic success.

Our CxC approach will facilitate the contributions of relevant stakeholders to the specification and design process and will provide holistic analysis of the trust dependencies across users, data, software and capability hardware. The impact of this will be to reduce overall software development costs, while increasing trustworthiness, of security-critical systems. This in turn will increase cyber security for businesses, government and the wider public and economy and increase societal trust in security-critical applications.

Key end users of our results will be industrial engineering organisations responsible for delivery of high assurance security-critical systems. Several leading UK and international companies (Airbus, Arm, Altran, AWE, Galois, L3Harris, Northrop Grumman, Thales) view our proposal as being of direct relevance to their engineering needs and see themselves as exploiting our research results in the future. The case study prototype security applications running on capability hardware will provide convincing demonstrators of the practicality of the developed CxC approach and will ease the path to greater industrial impact.

The CxC tools developed in this project will be made available as open source plug-ins to Rodin (www.event-b.org). An advantage of basing our developments on Rodin is that it already has a strong and growing user base. Rodin has users and developers in industry and academia (100s of academic users, e.g., UK, France, Germany, Austria, Spain, Finland, USA, Canada, Australia, New Zealand, China, India, Japan, Saudia Arabia, Malaysia, >15 industrial organisations) who actively follow advances in the technology and they will provide a strong basis for dissemination and exploitation of results.

Upskilling the workforce is a key challenge for many engineering companies. We will create a Professional Development course on CxC security design, exploiting case study material from HD-Sec, and look to offering these courses to the industrial The results of HD-Sec will provide us with new opportunities for consultancy for industry. Although the core tools will be open source, the business model is based on providing what we term an 'adoption support service' in the form of training, deployment support and development of bespoke tool features.

Our commercialisation path will also benefit from a unique University of Southampton initiative called Future Worlds (futureworlds.com) which is a vibrant network for connecting academic researchers with external collaborators and investors. Future Worlds will help us deliver impact from our research through a dedicated support team, video studio, web platform and a fast growing network of investors, mentors and entrepreneurs. The result of this wide-ranging support will be to maximize the likelihood of economic impact through consultancy and startup creation based on provision of secure software design support and adoption services, and increase social impact through events and high-quality web content.

We will participate in public engagement (PE) programmes such as the University of Southampton Science and Engineering Day to inspire young people to take up science. We will develop PE activities on formal modelling and verification of secure software aimed at primary school children.