About

The AppControl project enhances Digital Security By Design (DSbD) for mission-critical Systems-on-Chip. It uses the capabilities provided by the CHERI architecture to enable Design-by-Specification: the Systems-on-Chip has a formal, executable specification (typically created by the system architect), and every software component of the SoC is forced to adhere to this specification. Programs with incompatible specifications cannot run; unspecified run-time behaviour will raise an exception. The practical realisation is through the extension of programming languages to supports expressive specifications and a toolchain which ensures that the specifications are enforced at run time on Capability hardware. Our project was funded by the Digital Security by Design (DSbD) Programme delivered by UKRI to support the DSbD ecosystem.

The Problem

With the current state of the art, it is possible to limit the access privileges of a third-party program running on a computer system. The addition of architectural capabilities such as provided by CHERI enable unprecedented fine-grained memory protection and isolation. These mechanisms are however not sufficient to control the behaviour of a program so that it follows the intended specification. For example, if a program performs network access, it is not possible to ensure that the network location accessed is intended by the developer, or the result of a backdoor in the system. In general, this is the case for any system call performed by the program. As a result, malicious programs can e.g. participate in DDoS attacks, or send information about the system to a Command and Control server, etc. It is also the case for library calls, which could perform unspecified actions within the memory space of a process.

The Aim

The aim of this project is to enhance the provision of Digital Security By Design for mission-critical Systems-on-Chip through Capability hardware-enabled Design-by-Specification. What this means is that the Systems-on-Chip has a formal, executable specification (typically created by the system architect), and every software component of the SoC is forced to adhere to this specification. Programs with incompatible specifications cannot run; unspecified run-time behaviour will raise an exception. For the above example, the specification could govern the network access and also the access to system information. The practical realisation of this aim is through the extension of programming languages to supports expressive specifications and a toolchain which ensures that the specifications are enforced at run time on Capability hardware.

Recent Posts

news,website

AppControl Project Poster March 2024

March 13, 2024

Continue reading
news,website

AppControl Project Poster November 2023

November 8, 2023

Continue reading
news,website

AppControl Project Poster May 2023

May 27, 2023

Continue reading
news,website

AppControl Project Poster October 2022

October 12, 2022

Continue reading
news,website

AppControl Project Poster April 2022

April 6, 2022

Continue reading
news,website

AppControl Project Poster 2021

May 4, 2021

Continue reading
news,website

Launch of Project Website

November 17, 2020

Continue reading

There are more posts in the here.