The advent of trusted execution environments (TEEs) has ushered in a new era of confidential computing. However, using such TEEs is still non-trivial. To be able to use them well, especially while keeping the trusted computing base small, developers have to understand how to program with them, the exact security guarantees they provide, and how to correctly set them up and attest programs in them, as well. This is especially cumbersome as many different TEEs exist in the meantime, which differ substantially in their programming interfaces and usage, security guarantees, and performance characteristics, making it hard to port programs from one to another, let alone develop programs that use several TEEs together.

At Securified, we specialize in leveraging formal programming techniques in the context of confidential computing. In particular, we have devised static type systems based on information flow that allow us to precisely reason about guarantees in the vein of non-interference at every step of computations automatically using a variety of TEEs, including software-based cryptographic primitives for confidentiality, and even combine them on the same programs. We believe that such techniques are key to more secure, efficient, and effective use of TEEs.

Part of our work was described in an article published at ACM PLDI'24.