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层之上提供高抽象级抽象来简化软件开发。我们支持事件驱动编程，使用Rust和C语言为包括Intel SGX、ARM TrustZone和Sancus在内的异构TEE开发分布式飞地应用。本文讨论了方法的工作机制、对Sancus处理器的扩展，以及开发模型与商业TEE的集成方案。安全与性能评估表明，TEE结合我们的编程模型能为工业控制系统和物联网等领域的可信系统构建强大安全架构，展示了该框架在融合云计算、移动边缘设备及轻量级感知执行场景中的独特适用性。