This article presents an approach to provide strong assurance of the secure execution of distributed event-driven applications on shared infrastructures, while relying on a small Trusted Computing Base. We build upon and extend security primitives provided by Trusted Execution Environments (TEEs) to guarantee authenticity and integrity properties of applications, and to secure control of input and output devices. More specifically, we guarantee that if an output is produced by the application, it was allowed to be produced by the application’s source code based on an authentic trace of inputs. We present an integrated open-source framework to develop, deploy, and use such applications across heterogeneous TEEs. Beyond authenticity and integrity, our framework optionally provides confidentiality and a notion of availability, and facilitates software development at a high level of abstraction over the platform-specific TEE layer. We support event-driven programming to develop distributed enclave applications in Rust and C for heterogeneous TEE, including Intel SGX, ARM TrustZone, and Sancus. In this article we discuss the workings of our approach, the extensions we made to the Sancus processor, and the integration of our development model with commercial TEEs. Our evaluation of security and performance aspects show that TEEs, together with our programming model, form a basis for powerful security architectures for dependable systems in domains such as Industrial Control Systems and the Internet of Things, illustrating our framework’s unique suitability for a broad range of use cases which combine cloud processing, mobile and edge devices, and lightweight sensing and actuation.

We present an integrated open-source framework to develop, deploy, and use event-driven distributed enclaved applications across heterogeneous Trusted Execution Environments (TEEs). Our framework strives for strong application authenticity and integrity guarantees, and optionally confidentiality and availability, while minimizing the run-time Trusted Computing Base (TCB). For software developers, our framework provides a high level of abstraction over the platform-specific TEE layer that provides isolation, attestation and secure communication amongst distributed application components, allowing developers to focus of application logic. We provide a notion of event-driven programming to develop distributed enclave applications in Rust and C for heterogeneous TEEs, including Intel SGX, ARM TrustZone and the open-source Sancus. This heterogeneity makes our framework uniquely suitable for a broad range of use cases which combine cloud processing, mobile and edge devices, and lightweight sensing and actuation.

Information leakage through side-channels poses a serious threat to the security of distributed systems. Recent research on countermeasures against side-channel attacks show that, on embedded platforms with predictable execution times, certain classes of these vulnerabilities can be detected and mitigated automatically by means of language-based security techniques. In this paper, we propose a security type system to statically analyse MSP430 assembly programs to detecting information leakage through novel interrupt-latency attacks (a.k.a. Nemesis), timing side-channels, and undesired information flow. We have implemented our technique in a tool, Side Channel FinderMSP, which automatically verifies MSP430 object-code programs to be free of such vulnerabilities. We evaluate the effectiveness of our tool by applying it to a representative set of vulnerable and benign programs. Our experiments demonstrate that the tool is both effective in detecting vulnerabilities, and scalable to realistic applications.