Trusted Execution Environments (TEEs) are hardware-enforced memory isolation units, emerging as a pivotal security solution for security-critical applications. TEEs, like Intel SGX and ARM TrustZone, allow the isolation of confidential code and data within an untrusted host environment, such as the cloud and IoT. Despite strong security guarantees, TEE adoption has been hindered by an awkward programming model. This model requires manual application partitioning and the use of error-prone, memory-unsafe, and potentially information-leaking low-level C/C++ libraries. We address the above with \textit{HasTEE}, a domain-specific language (DSL) embedded in Haskell for programming TEE applications. HasTEE includes a port of the GHC runtime for the Intel-SGX TEE. HasTEE uses Haskell's type system to automatically partition an application and to enforce \textit{Information Flow Control} on confidential data. The DSL, being embedded in Haskell, allows for the usage of higher-order functions, monads, and a restricted set of I/O operations to write any standard Haskell application. Contrary to previous work, HasTEE is lightweight, simple, and is provided as a \emph{simple security library}; thus avoiding any GHC modifications. We show the applicability of HasTEE by implementing case studies on federated learning, an encrypted password wallet, and a differentially-private data clean room.

翻译：可信执行环境（TEE）是由硬件强制的内存隔离单元，正成为安全关键型应用的核心安全解决方案。诸如Intel SGX和ARM TrustZone等TEE可以在不可信的主机环境（如云和物联网）中隔离机密代码和数据。尽管提供了强大的安全保障，但TEE的采用一直受困于笨拙的编程模型。该模型要求手动划分应用程序，并使用容易出错、内存不安全且可能泄露信息的底层C/C++库。我们通过\textit{HasTEE}解决了上述问题，这是一种嵌入在Haskell中的领域特定语言（DSL），用于编程TEE应用。HasTEE包含一个为Intel-SGX TEE移植的GHC运行时。HasTEE利用Haskell的类型系统自动划分应用程序，并对机密数据实施\textit{信息流控制}。由于该DSL嵌入在Haskell中，它允许使用高阶函数、单子以及受限的I/O操作集来编写任何标准的Haskell应用。与以往工作不同，HasTEE轻量级、简单，并以一个\textit{简单安全库}的形式提供，从而避免了对GHC的任何修改。我们通过实现联邦学习、加密密码钱包和差分隐私数据清洁室等案例研究，展示了HasTEE的实用性。