< Back

Leveraging Formal Programming Techniques for Robust Confidential Computing

June 6, 2:50 PM - 3:10 PM
Imperial Room A

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.

About the speakers

Patrick Eugster

Patrick Eugster

Chief Technology Officer, Securified

Patrick Eugster is a full professor of computer science at USI in Lugano, Switzerland. Prior to that, he was a professor at Purdue University (2005-2016) and TU Darmstadt (2014-2017). Patrick is interested in distributed systems, notably their intersections with networks, programming languages, and security. He has been awarded for his research by various funding agencies (NSF CAREER 2007, DARPA CSSG 2011, ERC Consolidator 2014). Patrick has more than 10 years of experience in confidentiality-preserving data processing, including working as a consultant for the US Department of Defense in matters of cloud security. Patrick is also currently the Chief Technology Officer of the university spin-off Securified, a company specializing in secure distributed data processing. Securified's solutions leverage formal programming language techniques to provably achieve strong guarantees with automated use of security mechanisms such as trusted execution environments.

Romain Boichat

Romain Boichat

Chief Executive Officer, Securified

Romain Boichat studied computer science at EPFL, followed by an MSc degree at Carnegie Mellon University and a Ph.D. in communication systems at EPFL. To complement his scientific background with managerial and financial skills, he went on to obtain a Master's in Business Administration from IMD.

Romain joined Swiss Medical Network as Chief Operating Officer in 2011 and then became Managing Director of the holding Aevis Victoria. Prior to that, he was a consultant with McKinsey for several years, working for clients worldwide. He also held leadership positions, including as the first Dean of the School of Management of Technology at EPFL.

Romain Boichat is a serial entrepreneur with a particular focus on healthcare. He is motivated by the complexity of the healthcare industry for several reasons. First, it is a regulated environment that needs to be re-engineered in the long run in order to remain sustainable. Second, it has a strong and far-reaching impact on people's lives, and when it comes to costs and your health, economics become irrelevant. That is why he founded Corpus Health in September 2016, which aims to develop ventures offering innovative and disruptive products and services. As part of this effort, he also co-founded Securified to supply technical solutions, acting as its Chief Executive Officer.