Led by Principal Investigator, Professor Michael Butler, the Holistic Design of Secure
Systems on Capability Hardware (HD-Sec) project will receive funding as part of a £10M
investment in nine projects by the UK government through its ‘Digital Security by Design’ (DSbD)
programme to support the DSbD ecosystem.
The funding is managed by the Engineering and Physical Sciences Research Council (EPSRC).
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.
The HD-Sec project objectives can be summarised
- Develop systematic approaches for elicitation and formal modelling of security requirements and assumptions that incorporate environmental characteristics and vulnerabilities, including the impacts of trusted and untrusted users
- Develop and incorporate reusable formal abstractions of data trust mechanisms into our CxC approach to enable exploitation analysis of their contribution to application-level correctness
- Facilitate exploitation of capability hardware by software developers through the development and incorporation of high-level abstractions of trusted memory operations into our CxC approach
- Establish the soundness of the high-level abstractions wrt the existing formalisation of capability hardware and define mappings from the abstractions to code for use in application code generation
- Enhance the Rodin toolchain to support techniques developed for Objectives 1-4 in ways that make them accessible to software engineers
- Validate the resulting CxC toolchain on industrial-strength cyber security case studies including a functioning prototype application designed using our CxC tools and running on capability hardware
The success of HD-Sec can be measured by how well we deliver the key outcomes:
- 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
Programme & Methodology
To achieve our objectives, our work programme will consist of five workpackages WP1-WP5.
The case studies of WP1 will help us identify more clearly the engineering challenges in designing and verifying secure systems,
guiding the research of WP2-WP4 on modelling and analysis of requirements, trusted data and trusted memory operations respectively.
The research of WP2-WP4 will in turn define requirements on the enhanced toolchain developed in WP5.
We close the loop by validating the CxC toolchain to implement the case studies on capability hardware in WP1. The diagrammatic workplan (provided separately)
shows the coordination of the various workpackage tasks including the phasing of the tasks,
where a first phase develops initial results and a second phase develops enhanced results taking account of feedback from case studies.