This paper 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.

翻译：本文提出一种方法，在依赖小型可信计算基的前提下，为共享基础设施上分布式事件驱动应用的安全执行提供强有力保证。我们构建并扩展可信执行环境（TEE）提供的安全原语，以确保应用的认证性和完整性属性，并安全控制输入输出设备。具体而言，我们保证：若应用产生输出，则该输出必定基于真实的输入轨迹被应用源代码所允许。我们提出一个集成式开源框架，支持跨异构TEE开发、部署和使用此类应用。除认证性和完整性外，该框架可选提供机密性和可用性概念，并通过在平台特定TEE层之上封装高抽象层级，促进软件开发。我们支持事件驱动编程，用于在异构TEE（包括Intel SGX、ARM TrustZone和Sancus）上使用Rust和C语言开发分布式飞地应用。本文探讨该方法的工作原理、对Sancus处理器的扩展，以及开发模型与商用TEE的集成。安全与性能评估表明，TEE结合我们的编程模型能够为工业控制系统和物联网等领域的可信系统构建强大的安全架构，充分展示该框架在结合云计算、移动与边缘设备、轻量传感与执行等广泛用例中的独特适用性。