| EPSRC Reference: |
EP/V000462/1 |
| Title: |
AppControl: Enforcing Application Behaviour through Type-Based Constraints |
| Principal Investigator: |
Vanderbauwhede, Professor W |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
School of Computing Science |
| Organisation: |
University of Glasgow |
| Scheme: |
Standard Research |
| Starts: |
01 September 2020 |
Ends: |
30 June 2024 |
Value (£): |
1,483,020
|
| EPSRC Research Topic Classifications: |
| Computer Sys. & Architecture |
Software Engineering |
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
06 Apr 2020
|
ISCF Digital Security by Design Research Projects
|
Announced
|
|
|
Summary on Grant Application Form |
Background: 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.
Project 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.
Key Ideas in a Nutshell
Our vision of how to achieve this goal is through the use of behavioural type systems, i.e. the specification of the SoC and each of its individual components are expressed as a type, which effectively and formally describes the allowed interfaces and interactions of each component. This type-based specification will be an integral component of the program executable, and be validated against an overall system specification by the operating system.
This proposal focuses on software components, and will build on the capability hardware for enforcement of the type-based specifications. The type-based Design-by-Specification of hardware components is the topic of the EPSRC Border Patrol project (EP/N028201/1), which will run until 2023 and therefore present great potential for synergies with the current proposal.
Prior Work
In our current EPSRC project Border Patrol (EP/N028201/1) we investigate digital security by design for the design of hardware IP-core based SoCs. The key mechanism is the use of type-driven design-by-specification. A design's specification is encoded in the type system, so that the implementation must follow the specification. Adherence to the spec can be enforced at design time for trusted modules, and at run time for untrusted modules by patrolling the untrusted module's borders with FSM-based run-time type checkers.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
http://www.gla.ac.uk |