Border Patrol: Improving Smart Device Security through Type-Aware Systems Design
Lead Research Organisation:
University of Glasgow
Department Name: School of Computing Science
Abstract
There are increasing concerns about the safety and security of critical infrastructure such as nuclear power plants, the electricity grid and other utilities in the face of possible cyber attacks. As ageing controllers are replaced by smart devices based on Field-Programmable Gate Arrays (FPGAs) and embedded microprocessors, the safety of such devices raises many concerns. In particular, there is the very real risk of malicious functionality hidden in the silicon or in software binaries, dormant and waiting to be activated. Current
hardware and software systems are of such complexity that it is impossible to discover such malicious code through testing.
We aim to address this problem by closely connecting the system design specification with the actual implementation through the use of a formal design methodology based on type systems with static and dynamic type checking. The type system will be used as a formal language to encode the design specification so that the actual implementation will automatically be checked against the specification.
Static type checking of data types and multiparty session types can ensure the correctness of the interaction between the components. However, as static checking assume full access to the design source code it cannot be used to protect against potential threads issuing from third-party functional blocks (know as ``Intellectual Property Cores'' or IP cores) that are commonly used in hardware design:
the provider of the IP core can claim adherence to the types and protocols, so that the IP core will meet the compile-time requirements, but the run-time the behaviour cannot be controlled using static techniques. The same applies to third-party compiled software libraries.
Therefore we propose to use run-time checking of data types as well as session types at the boundaries of untrusted modules ("Border Patrol"), so that any intentional or unintentional
breach of the specification will safely be intercepted.
hardware and software systems are of such complexity that it is impossible to discover such malicious code through testing.
We aim to address this problem by closely connecting the system design specification with the actual implementation through the use of a formal design methodology based on type systems with static and dynamic type checking. The type system will be used as a formal language to encode the design specification so that the actual implementation will automatically be checked against the specification.
Static type checking of data types and multiparty session types can ensure the correctness of the interaction between the components. However, as static checking assume full access to the design source code it cannot be used to protect against potential threads issuing from third-party functional blocks (know as ``Intellectual Property Cores'' or IP cores) that are commonly used in hardware design:
the provider of the IP core can claim adherence to the types and protocols, so that the IP core will meet the compile-time requirements, but the run-time the behaviour cannot be controlled using static techniques. The same applies to third-party compiled software libraries.
Therefore we propose to use run-time checking of data types as well as session types at the boundaries of untrusted modules ("Border Patrol"), so that any intentional or unintentional
breach of the specification will safely be intercepted.
Planned Impact
Realising our vision will lead to a revolution in the programming of FPGA-based Systems-on-Chip in particular and embedded systems in general. Progress in the area of systems security is essential to ensure trust in critical infrastructure (e.g. controllers for nuclear power plants) as well as consumer products (cars, smart household appliances). Thanks to the strong theoretical foundations of our work, our methodology will provide very string guarantees about system security. Adoption of our approach into standards for embedded systems would have a very significant impact by removing the security concerns related to the adoption of such systems.
Our proposed work will lead to highly novel compiler technologies, based on a sound formal foundation with guarantees for systems integrity. Not only will our approach make systems more secure, it will also make application development more efficient..
In a nutshell, our methodology encodes the design specification of the system in the type system, so that it is not possible to design a system implementation that does not conform to the formal specification. There is a clear need for more secure systems design, driven by the sectors mentioned above: protection of critical infrastructure is becoming more and more important not only because of the increased threat level but also because aging controller are being replaced with smart devices. The Internet of Things promises a revolution in the home by allowing us a high degree of remote control over our appliances, but security is crucial because compromising such systems could lead to nightmare scenarios. The same is true for the automotive industry: already embedded systems in cars have been hacked, demonstrating the need for a more secure desing approach.
The applications domain for our work is very broad, both in terms of the sectors where smart devices and FPGA-based systems are deployed (much wider than the three examples cited above) but also in terms of applications that are not security related. The obvious one is safety, because our approach makes systems more safe as well as more secure. But apart from that, the adoption of the advanced type systems we propose into design tools and methodologies will make systems design more efficient as well: by dramatically reducing the amount of errors and catching the errors much sooner in the design phase, the debugging times will be reduced very considerably.
Impact of our work will result primarily from adoption of our approach in industry and academia. The Pathways to Impact document explains how we will achieve this impact.
Our proposed work will lead to highly novel compiler technologies, based on a sound formal foundation with guarantees for systems integrity. Not only will our approach make systems more secure, it will also make application development more efficient..
In a nutshell, our methodology encodes the design specification of the system in the type system, so that it is not possible to design a system implementation that does not conform to the formal specification. There is a clear need for more secure systems design, driven by the sectors mentioned above: protection of critical infrastructure is becoming more and more important not only because of the increased threat level but also because aging controller are being replaced with smart devices. The Internet of Things promises a revolution in the home by allowing us a high degree of remote control over our appliances, but security is crucial because compromising such systems could lead to nightmare scenarios. The same is true for the automotive industry: already embedded systems in cars have been hacked, demonstrating the need for a more secure desing approach.
The applications domain for our work is very broad, both in terms of the sectors where smart devices and FPGA-based systems are deployed (much wider than the three examples cited above) but also in terms of applications that are not security related. The obvious one is safety, because our approach makes systems more safe as well as more secure. But apart from that, the adoption of the advanced type systems we propose into design tools and methodologies will make systems design more efficient as well: by dramatically reducing the amount of errors and catching the errors much sooner in the design phase, the debugging times will be reduced very considerably.
Impact of our work will result primarily from adoption of our approach in industry and academia. The Pathways to Impact document explains how we will achieve this impact.
Publications
Altayeva A
(2019)
Service Equivalence via Multiparty Session Type Isomorphisms
in Electronic Proceedings in Theoretical Computer Science
Archibald B
(2018)
Replicable parallel branch and bound search
in Journal of Parallel and Distributed Computing
Archibald B
(2020)
YewPar
Barbanera F
(2023)
Multicompatibility for Multiparty-Session Composition
Barwell A
(2023)
Designing Asynchronous Multiparty Protocols with Crash-Stop Failures
Barwell A
(2023)
Designing Asynchronous Multiparty Protocols with Crash-Stop Failures
Description | We have developed a framework of domain-specific languages to describe Systems-on-Chip in such a way that the type system of the language is used as the specification of the composition of the system. That means that we can formally guarantee that the System-on-Chip design is composed of the right components and that they are connected correctly. We have also developed a session-type based mechanism for validating transactions on interconnections between blocks in a System-on-Chip |
Exploitation Route | Our work could be implemented in an IDE for SoC design such as the Xilinx SDSoC tool or similar tools, to ensure the correctness of the designs created. |
Sectors | Digital/Communication/Information Technologies (including Software) Electronics |
URL | https://border-patrol.github.io/ |
Title | Replicable Parallel Branch and Bound Search |
Description | |
Type Of Material | Database/Collection of data |
Year Produced | 2017 |
Provided To Others? | Yes |
Title | YewPar: Skeletons for Exact Combinatorial Search |
Description | |
Type Of Material | Database/Collection of data |
Year Produced | 2019 |
Provided To Others? | Yes |
URL | http://researchdata.gla.ac.uk/id/eprint/935 |
Title | A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming (Artifact) |
Description | This artifact contains a version of the Scribble tool that, given a protocol specification with multiple participants, can generate Scala APIs for implementing each participant in a type-safe, protocol-abiding way. Crucially, the API generation leverages a decomposition of the multiparty protocol into type-safe peer-to-peer interactions between pairs of participants; and this, in turn, allows to implement the API internals on top of the existing lchannels library for type-safe binary session programming. As a result, several technically challenging aspects in the implementation of multiparty sessions are solved "for free", at the underlying binary level. This includes distributed multiparty session delegation: this artifact implements it for the first time. |
Type Of Technology | Software |
Year Produced | 2017 |
Title | A Typing Discipline for Hardware Interfaces (Artifact) |
Description | Modern Systems-on-a-Chip (SoC) are constructed by composition of IP (Intellectual Property) Cores with the communication between these IP Cores being governed by well described interaction protocols. However, there is a disconnect between the machine readable specification of these protocols and the verification of their implementation in known hardware description languages. Although tools can be written to address such a separation of concerns, such tooling is often hand written and used to check hardware designs a posteriori. We have developed a dependent type-system and proof-of-concept modelling language to reason about the physical structure of hardware interfaces respective to user provided descriptions. Our type-system provides correct-by-construction guarantees that the interfaces on an IP Core will be well-typed if they adhere to a specified standard. |
Type Of Technology | Software |
Year Produced | 2019 |
Open Source License? | Yes |
Impact | This software is the implementation of a modelling language to reason about the physical structure of hardware interfaces. |
URL | https://drops.dagstuhl.de/opus/volltexte/2019/10791/ |
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: Design-By-Contract for Flexible Multiparty Session Protocols |
Description | Artifact for the paper : Design-By-Contract for Flexible Multiparty Session Protocols |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
Impact | Artifact supporting the paper : Design-By-Contract for Flexible Multiparty Session Protocols |
URL | https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.21 |
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: Generalised Multiparty Session Types with Crash-Stop Failures |
Description | Artifact supporting the paper : Generalised Multiparty Session Types with Crash-Stop Failures |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
Impact | Artifact for the paper : https://github.com/alcestes/mpstk-crash-stop |
URL | https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.35 |
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 | CAMP: Cost-Aware Multiparty Session Protocols (artifact) |
Description | This is the artifact for the paper *CAMP: Cost-Aware Multiparty Session Protocols*.
The artifact comprises: - A library for specifying cost-aware multiparty protocols. - The raw data used for comparing the cost models with real execution costs. - The cost-aware protocol specifications of the benchmarks that we studied. The library for specifying cost-aware protocols also provides functions for extracting cost equations from them, and for estimating recursive protocol latencies (i.e. average cost per protocol iteration). We provide a script for extracting cost equations, and instantiating them using the parameters used in the paper. |
Type Of Technology | Software |
Year Produced | 2020 |
Open Source License? | Yes |
URL | https://zenodo.org/record/4046893 |
Title | CAMP: Cost-Aware Multiparty Session Protocols (artifact) |
Description | This is the artifact for the paper *CAMP: Cost-Aware Multiparty Session Protocols*.
The artifact comprises: - A library for specifying cost-aware multiparty protocols. - The raw data used for comparing the cost models with real execution costs. - The cost-aware protocol specifications of the benchmarks that we studied. The library for specifying cost-aware protocols also provides functions for extracting cost equations from them, and for estimating recursive protocol latencies (i.e. average cost per protocol iteration). We provide a script for extracting cost equations, and instantiating them using the parameters used in the paper. |
Type Of Technology | Software |
Year Produced | 2020 |
Open Source License? | Yes |
URL | https://zenodo.org/record/4046892 |
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 | Talk at the ARM Research Summit |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Industry/Business |
Results and Impact | The ARM Research Summit is a conference organized by the multinational microprocessor company ARM. This forum allows us to reach an industry audience and has been a great way to create industry contact for future projects. In particular, ARM Is now part of the advisory board of the Border Patrol. |
Year(s) Of Engagement Activity | 2017 |
URL | https://developer.arm.com/research/summit/previous-summits/2017 |