Holistic Design of Secure Systems on Capability Hardware (HD-Sec)
Lead Research Organisation:
University of Southampton
Department Name: Sch of Electronics and Computer Sci
Abstract
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
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
Planned Impact
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.
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.
Organisations
- University of Southampton (Lead Research Organisation)
- Galois, Inc. (Collaboration)
- Thales Group (Collaboration)
- Altran (Collaboration)
- AdaCore (Collaboration)
- Atomic Weapons Establishment (Collaboration)
- Altran (United Kingdom) (Project Partner)
- Galois (United States) (Project Partner)
- L3Harris (United Kingdom) (Project Partner)
- Atomic Weapons Establishment (Project Partner)
- ARM (United Kingdom) (Project Partner)
- Thales (United Kingdom) (Project Partner)
- Airbus (Germany) (Project Partner)
- Northrop Grumman UK Limited (Project Partner)
Publications
Al-Shareefy H
(2023)
AIC Approach for Intelligent Systems Requirements Elicitation
Asieh Salehi Fathabadi
(2021)
Extensible Record Structures in Event-B
Dana Dghaym
(2021)
Verifying System-level Security of a Smart Ballot Box
Thai Son Hoang
(2021)
The CamilleX Framework for the Rodin Platform
Description | Systematic and rigorous method for identify component level requirements from system level security requirements. Importance of correct design of mechanisms for handling of hardware runtime exceptions to ensure robust behaviour of secure systems. |
Exploitation Route | Could help systems developers to analyse and verify security requirements and design correct and robust secure systems. |
Sectors | Aerospace Defence and Marine Digital/Communication/Information Technologies (including Software) Transport |
URL | https://hd-sec.github.io/posts/ |
Description | The modelling approach being developed in HD-Sec are being used a project with a partner in the aerospace industry to analyse the impact of security vulnerabilities on functional properties of aerospace subsystems. |
First Year Of Impact | 2022 |
Sector | Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software) |
Description | AWE |
Organisation | Atomic Weapons Establishment |
Country | United Kingdom |
Sector | Private |
PI Contribution | Feedback on Information Barrier case study. |
Collaborator Contribution | AWE provided details on the Information Barrier system which is a potential case study for us to apply the techniques and tools we develop to. |
Impact | Outline plans for us to work on Information Barrier case study. |
Start Year | 2020 |
Description | AdaCore |
Organisation | AdaCore |
Country | France |
Sector | Private |
PI Contribution | Expertise and tools for transforming formal models to Spark Ada code. |
Collaborator Contribution | Access to Ada tools, advice on use of tool |
Impact | n/a |
Start Year | 2021 |
Description | Altran |
Organisation | Altran |
Country | United Kingdom |
Sector | Private |
PI Contribution | Formal modelling and analysis of Tokeneer security system. |
Collaborator Contribution | Requirements documents and technical insights into challenges of Tokeneer system |
Impact | Draft paper under development |
Start Year | 2020 |
Description | Galois Inc |
Organisation | Galois, Inc. |
Country | United States |
Sector | Private |
PI Contribution | We developed formal model and analysis of Smart Ballot Box system developed by Galois covering security requirements and analysis of impact of threats on security properties. |
Collaborator Contribution | Galois provided requirements documents and code for the SBB and insights into the security mechanisms used. |
Impact | Formal models and analysis of SBB |
Start Year | 2020 |
Description | Thales |
Organisation | Thales Group |
Department | Thales UK Limited |
Country | United Kingdom |
Sector | Private |
PI Contribution | Thales provided details on the trusted avionics platform which is a potential case study for us to apply the techniques and tools we develop to. |
Collaborator Contribution | Outline plans for us to work on trusted avionics platform case study. |
Impact | N/A |
Start Year | 2020 |
Title | CamilleX |
Description | The CamilleX framework is a plug-in for the Rodin platform for formal modelling and analysis using Event-B. The framework provides a textual representation and persistence for the Event-B modelling constructs. It supports direct extensions to the Event-B syntax such as machine inclusion and record structures, as well as indirect extensions provided by other plugins such as UML-B diagrams. |
Type Of Technology | Webtool/Application |
Year Produced | 2022 |
Open Source License? | Yes |
Impact | The software tool supports greater scaling of Event-B models through support for hierarchical inclusion of modelling components. There is some early adoption by a range of users, including industrial users. |
URL | https://wiki.event-b.org/index.php/CamilleX_User_Guide |
Description | HD-Sec Website |
Form Of Engagement Activity | Engagement focused website, blog or social media channel |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Professional Practitioners |
Results and Impact | Web page for project |
Year(s) Of Engagement Activity | 2020,2021 |
URL | https://hd-sec.github.io |