Holistic Design of Secure Systems on Capability Hardware

HD-Sec: Holistic Design of Secure Systems on Capability Hardware

The HD-Sec project will address engineering challenges in establishing and formally verifying the relationship between application-level security requirements and secure software implementations running on capability hardware.

Even if software has been verified as secure, it is likely to be running on hardware that is vulnerable to cyber-attack because of poor memory protection. Capability hardware, such as the CHERI architecture, provides a range of memory protection features to reduce hardware vulnerabilities. Software verification needs to make assumptions about hardware such as atomicity, separation and permission in memory operations, especially in the context of concurrent software; capability hardware should allow for simplification of these assumptions so there is a need to understand how verification can be simplified while retaining soundness.

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

Related News