HasTEE: Programming Trusted Execution Environments with Haskell
summary
A Haskell DSL called HasTEE embeds enclave, app and client monads, provides a GHC runtime port for Intel SGX and partitions a single Haskell program by compiling it twice with a flag that substitutes dummy implementations, using the type system to get automatic partitioning via types and a Gateway API that enforces information-flow constraints (binary instance + restricted IO). Implementation uses the Gramine library OS and patched mmap/select; measured resident enclave memory stays under 93 MB and observed latency is about 60 ms latency vs 6 ms native on the password-wallet benchmark; demos include federated learning with a simple homomorphic linear-regression library, an encrypted password wallet, and a differential-privacy clean room.
AI-written summary · about
chapters (15)
- 0:00HasTEE and Haskell TEE intro
- 1:46Trusted Execution Environments needed
- 3:12TEE programming challenges
- 5:00HasTEE domain-specific language
- 6:03Password checker demo
- 7:51HasTEE program partitioning
- 9:17Compiling HasTEE for enclaves
- 10:00Enclave code binary analysis
- 11:02Information flow control in HasTEE
- 13:30Runtime dependencies and hosting
- 15:56Enclave execution performance
- 17:43Zero-trust federated learning
- 19:31Password wallet and privacy examples
- 20:12Future work and Cherry integration
- 21:34Q&A
related talks
15mSecured Routines: Language-based Construction of Trusted Execution Environments
50mTrusted Execution Environments Meet the Blockchain
41mPanel: A New Root Of Trust: Changing Computing With TEE
40mConfidential Computing and Privacy-Enhancing Technologies - The Landscape
38mOne Ring -3 To Secure Them All: Computing with Hardware Enclaves
36mAttacking & Defending Kubernetes TEE Enclaves in Critical Infrastructure
34mTeaclave: Making Computation on Privacy-Sensitive Data Safe and Simple
38mDeveloping Trusted Applications for Trusted Execution Environments and vTEEs