AppControl: Enforcing Application Behaviour through Type-Based Constraints
Lead Research Organisation:
University of Glasgow
Department Name: School of Computing Science
Abstract
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.
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.
Planned Impact
AppControl will have major impact through the adoption of our enforceable specifications technology to enable software based security for CHERI based architectures such as the Capability Hardware Morello board being designed by Arm. The use of of our approach will dramatically increase safety and security of smart devices and enable novel product developments. These outcomes will have impact on both society and economy, by helping to protect such future Capability processor based systems utilised in many areas ranging from critical infrastructure to home appliances from cyber attacks. We have identified nine activities to realise the economic, societal and academic impacts of this project. The majority of these activities are pathways to adoption by industry and dissemination in academia as those will have the major impact. However, several of the activities also serve as direct pathways to impacts on Knowledge and People. The Management Team (PIs at Glasgow, Essex and Imperial) will ensure that the impact activities are on track and deliver the relevant outcomes, through quarterly reviews. The progress of the impact activities will also be monitored through the yearly audit meeting of the steering group formed by the management team and the industrial partners.
(1) Validation Exemplars: The most important way to ensure that our research can deliver its promise impact, to the embedded systems community in general, industry and to the ISCF programme in particular, is to build a exemplars of the technologies that showcase the capability enabled by the use of enforceable specifications for secure Systems-on-Chip. Using our technologies, tools and methodologies to create a proof-of-concept exemplars for the Morello boards designed by Arm, which will enable us to demonstrate convincingly the capabilities of our novel approach. This activity is a prerequisite for activities 4, 5 and 6, and will have a major impact on the other activities as well.
(2) Open-Source Community Project: We believe that the most effective way to achieve impact is to share our type system and compilation system under an open source license, via a community development project (hosted e.g. on GitHub).This approach allows users to implement our type system or similar approaches in their own systems, and allows us to invite contributions to improve the compilation system. By taking charge of the management and hosting of the project, we can direct the development and ensure the quality of the releases.
(3) Engaging with Industrial Partners:to accelerate adoption in industry, there will be a close collaboration with industrial partners (Arm, NASA JPL, UltraSoC, cfr. Letters of Support).
(4) Commercialisation: for some outcomes of the research, technology licensing or other forms of IP commercialisation are a better choice than open-source distribution.
(5) Public Engagement and STEM Activities
(6) Postgraduate Skills and Training: AppControl has an important role to play in developing and sustaining the UK skill base in compiler and run-time development for Capability-based SoCs as well as type theory, both research areas where the UK is at the forefront of the international research scene.
(7) Dissemination Workshops, Tutorials and Lectures: Because our work focuses on highly innovative type systems it will be of great relevance o the programming languages and compilers research, as well as the computer architecture and cybersecurity communities.
(8) Research Publications:To maximise the academic impact we shall publish our research in the most respected journals and conferences in the area
(9) Networking
(1) Validation Exemplars: The most important way to ensure that our research can deliver its promise impact, to the embedded systems community in general, industry and to the ISCF programme in particular, is to build a exemplars of the technologies that showcase the capability enabled by the use of enforceable specifications for secure Systems-on-Chip. Using our technologies, tools and methodologies to create a proof-of-concept exemplars for the Morello boards designed by Arm, which will enable us to demonstrate convincingly the capabilities of our novel approach. This activity is a prerequisite for activities 4, 5 and 6, and will have a major impact on the other activities as well.
(2) Open-Source Community Project: We believe that the most effective way to achieve impact is to share our type system and compilation system under an open source license, via a community development project (hosted e.g. on GitHub).This approach allows users to implement our type system or similar approaches in their own systems, and allows us to invite contributions to improve the compilation system. By taking charge of the management and hosting of the project, we can direct the development and ensure the quality of the releases.
(3) Engaging with Industrial Partners:to accelerate adoption in industry, there will be a close collaboration with industrial partners (Arm, NASA JPL, UltraSoC, cfr. Letters of Support).
(4) Commercialisation: for some outcomes of the research, technology licensing or other forms of IP commercialisation are a better choice than open-source distribution.
(5) Public Engagement and STEM Activities
(6) Postgraduate Skills and Training: AppControl has an important role to play in developing and sustaining the UK skill base in compiler and run-time development for Capability-based SoCs as well as type theory, both research areas where the UK is at the forefront of the international research scene.
(7) Dissemination Workshops, Tutorials and Lectures: Because our work focuses on highly innovative type systems it will be of great relevance o the programming languages and compilers research, as well as the computer architecture and cybersecurity communities.
(8) Research Publications:To maximise the academic impact we shall publish our research in the most respected journals and conferences in the area
(9) Networking
Publications
Zhou F
(2020)
Statically Verified Refinements for Multiparty Protocols
Medic D
(2020)
A parametric framework for reversible p-calculi
in Information and Computation
Majumdar R
(2020)
Multiparty motion coordination: from choreographies to robotics programs
in Proceedings of the ACM on Programming Languages
Castro-Perez D
(2020)
CAMP: Cost-Aware Multiparty Session Protocols
Griesemer R
(2020)
Featherweight go
in Proceedings of the ACM on Programming Languages
Zhou F
(2020)
Statically verified refinements for multiparty protocols
in Proceedings of the ACM on Programming Languages
Castro-Perez D
(2020)
CAMP: cost-aware multiparty session protocols
in Proceedings of the ACM on Programming Languages
Ghilezan S
(2021)
Precise subtyping for asynchronous multiparty sessions
in Proceedings of the ACM on Programming Languages
Description | The work aims to make interactions between running applications and with the hardware (access to network, disk, memory) secure by enforcing that every interaction conforms to a formal specification. This specification is part of the program and is enforced by the operating system. We have not achieved this as the project is in an early stage, but we have developed a number of key components: - a mechanism to express the formal specification in the type system of a modern programming language (rust) - a mechanism to validate the interactions against the specification - a mechanism to secure the entry and exit points in a program such that no other entry and exit points are possible |
Exploitation Route | This project is part of the Digital Security by Design initiative https://www.dsbd.tech/ and because of this there is much closer interaction between all projects funded by this call and industry partners such as Arm and Microsoft. Therefore commercial use of the technology researched in the project is much more easily adopted by industry. |
Sectors | Digital/Communication/Information Technologies (including Software) Electronics Energy Financial Services and Management Consultancy Government Democracy and Justice |
URL | https://dsbd-appcontrol.github.io/ |
Title | Additional file 1 of DNA methylation-based sex classifier to predict sex and identify sex chromosome aneuploidy |
Description | Additional file 1 Sex related differentially methylated CpGs. A list of the identified 4331 sex related differentially methylated CpGs on sex chromoseomes which are also used to construct the classifier. |
Type Of Material | Database/Collection of data |
Year Produced | 2021 |
Provided To Others? | Yes |
URL | https://springernature.figshare.com/articles/dataset/Additional_file_1_of_DNA_methylation-based_sex_... |
Title | Additional file 1 of DNA methylation-based sex classifier to predict sex and identify sex chromosome aneuploidy |
Description | Additional file 1 Sex related differentially methylated CpGs. A list of the identified 4331 sex related differentially methylated CpGs on sex chromoseomes which are also used to construct the classifier. |
Type Of Material | Database/Collection of data |
Year Produced | 2021 |
Provided To Others? | Yes |
URL | https://springernature.figshare.com/articles/dataset/Additional_file_1_of_DNA_methylation-based_sex_... |
Title | Artifact: Deadlock-Free Asynchronous Message Reoerderign in Rust with Multiparty Session Types |
Description | Artifact of the paper: "Deadlock-Free Asynchronous Message Reoerderign in Rust with Multiparty Session Types", PPoPP 2022. |
Type Of Technology | Software |
Year Produced | 2021 |
Open Source License? | Yes |
Impact | The Rumpsteak framework is a framework for MPST in Rust. This software is an artifact that shows its capabilities. |
URL | https://zenodo.org/record/5786034 |
Title | Artifact: Dynamically Updatable Multiparty Session Protocols |
Description | Artifact for the paper: Dynamically Updatable Multiparty Session Protocols |
Type Of Technology | Software |
Year Produced | 2023 |
Open Source License? | Yes |
Impact | Artifact supporting the paper Dynamically Updatable Multiparty Session Protocols |
URL | https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.10 |
Title | Artifact: Generic Go to Go: Dictionary-Passing, Monomorphisation, and Hybrid |
Description | Artifact for paper: Generic Go to Go: Dictionary-Passing, Monomorphisation, and Hybrid |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
Impact | Artifact for paper : Generic Go to Go: Dictionary-Passing, Monomorphisation, and Hybrid |
URL | https://dl.acm.org/doi/10.1145/3563331 |
Title | Artifact: Rollback Recovery in Session-Based Programming |
Description | Artifact for paper: Rollback Recovery in Session-Based Programming |
Type Of Technology | Software |
Year Produced | 2023 |
Impact | Artifact for paper: Rollback Recovery in Session-Based Programming |
URL | https://link.springer.com/chapter/10.1007/978-3-031-35361-1_11#chapter-info |
Title | Artifact: Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types |
Description | Artifact for the paper: Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types (https://doi.org/10.4230/DARTS.8.2.9) This introduces the `multicrusty` library. |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
Impact | Artifact supporting the paper. |
URL | https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.9 |
Title | Designing Asynchronous Multiparty Protocols with Crash-Stop Failures (Artifact) |
Description | We introduce Teatrino, a toolchain that supports handling multiparty protocols with crash-stop fail- ures and crash-handling behaviours. Teatrino accompanies the novel MPST theory in the related article, and enables users to generate fault-tolerant protocol-conforming Scala code from Scribble protocols. Local types are projected from the global protocol, enabling correctness-by-construction, and are expressed directly as Scala types via the Effpi concurrency library. Teatrino extends both Scribble and Effpi with support for crash-stop behaviour. The generated Scala code is execut- able and can be further integrated with existing systems. The accompanying theory in the related article guarantees deadlock-freedom and liveness properties for failure handling protocols and their implementation. This artifact includes examples, extended from both session type and distributed systems literature, featured in the related article. |
Type Of Technology | Software |
Year Produced | 2023 |
Open Source License? | Yes |
Impact | Artifact supporting the paper Designing Asynchronous Multiparty Protocols with Crash-Stop Failures |
URL | https://zenodo.org/record/7974824 |
Description | AppControl web site |
Form Of Engagement Activity | Engagement focused website, blog or social media channel |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Industry/Business |
Results and Impact | 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. |
Year(s) Of Engagement Activity | 2020,2021,2022,2023 |
URL | https://dsbd-appcontrol.github.io/ |