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 modelling and verification tools guide the design of software in such a way that it satisfies its specification by construction. The 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. By trust dependencies we mean the way in which satisfaction of the application-level security requirements depends on characteristics of the system environment, including the users, and on properties of the underlying data, software and hardware. We will adopt the existing formal foundations of the Event-B CxC method and the existing Rodin open source toolset for Event-B.

Our RESEARCH HYPOTHESIS is that the methods and tools required for a CxC design approach to cyber security systems can be achieved by enriching the existing generic CxC approach provided by Event-B/Rodin with security-specific capabilities.

Key RESEARCH QUESTIONS that need to be addresses in order to achieve this are:

1. What domain structures will help to bridge the gap between informal security requirements and formal models?
2. What kinds of properties of user behaviours need to be incorporated into formal modelling?
3. What are the right formal models of data trust mechanisms that allow for easy reuse of design and verification effort in the design of secure applications?
4. What are the right design abstractions for hardware security features that will make it easier to design and verify applications running on capability hardware as opposed to unprotected hardware?

This leads to the following OBJECTIVES for the HD-Sec project:

1. 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
2. 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
3. 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
4. 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
5. Enhance the Rodin toolchain to support techniques developed for Objectives 1-4 in ways that make them accessible to software engineers
6. 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