Home

This is the home for AppControl and Morello-HAT, two closely related projects which aim to enhance the security of mission-critical Systems-on-Chip (SoC) through the integration of capability hardware and behavioural types. They are a collaboration between the University of Glasgow, the University of Essex and the University of Oxford and are funded by the UKRI Digital Security by Design (DSbD) programme.

The Vision

The idea behind the AppControl project is to use behavioural type systems to formally describe the interfaces and interaction of software components in Systems-on-Chip (SoC) and enforce these specifications at run time through the hardware capabilities provided by the CHERI architecture.

The Morello-HAT project is a companion to AppControl which further narrows down the focus to the development of common APIs that leverage the hardware capabilities implemented by the Morello architecture alongside behavioural types. The primary goal is to support compiler developers and programmers of higher-level languages in obtaining better memory and object type safety properties in their respective languages and programs.

The Morello software stack primarily supports programming through the C and C++ languages. The capability API for these languages is based on a low-level representation of capability pointers which leaves plenty of room for improvement. In contrast, there are many promising modern languages with fast-growing popularity (e.g. Go, Rust, Dart,) that are not pointer-based and support more advanced type systems and memory management strategies. It is therefore important for the success of the Morello platform that it supports such languages. There is a wide gap between the current low-level, C-focused capability API and the needs of higher-level languages, and that is the gap which this project aims to fill.

What can AppControl and Morello-HAT do for you?

In practical terms, AppControl allows a SoC's system architect to create a formal, executable specification that describes the expected behaviour of each software component. Enforcing this specification at run time ensures brings several benefits:

• Security: By enforcing the expected behaviour of software components, we can prevent malicious or unintended actions that could compromise the system's integrity.
• Reliability: Ensuring that software components adhere to their specifications reduces the risk of unexpected behaviour and system failures.
• Maintainability: A formal specification provides a clear contract for each software component, making it easier to understand and maintain the system as a whole.
• Interoperability: By defining clear interfaces and interactions, we can ensure that different software components can work together seamlessly, even if they are developed by different teams or organizations.