Privagic: confidential computing made practical with secure typing
Team work: Gaël Thomas presented "Privagic: confidential computing made practical with secure typing" at 1D19 the 29/9/2023 at 11h00.
Abstract
For more than twenty years, several tools have been proposed to automatically partition an application between a secure memory zone and an non-secure memory zone. These tools analyze the data flow of the application in order to identify the memory locations that may contain sensitive values. Unfortunately, in the presence of pointers, most of these tools miss-behave. When they do not miss-behave, they are unable to handle threads because of the difficulty to track pointers in a multi-threaded application. They also significantly over-approximate the number of sensitive memory locations, which makes these tools unable to split an application in more than two partitions.
In this talk, instead of starting from data-flow analysis, we propose to accurately identify the memory locations that contain sensitive values by using typing. We introduce secure typing, which consists in directly embedding a partition identifier in the type system of a language. Based on secure typing, we designed a language-agnostic compiler based on LLVM. The compiler takes a legacy application enriched with secure types as input, and generates multiple partitions for Intel SGX. Our evaluation with micro- and macro-applications show that (i) adding secure types in a legacy application is easy, (ii) secure typing can be used in multi-threaded applications, to generate multiple partitions, and for different languages, (ii) secure typing helps to reduce the trusted computing base and is more efficient than embedding a full application inside an enclave.
Bio
Since 2023, Gaël Thomas is a senior researcher at Inria Saclay. His research focuses on virtualization, operating systems, concurrency and language runtimes. He is particularly interested in improving the performance, the design and the safety of the systems. He leads the Benagil team, which is a joint team between Inria and Telecom SudParis/IP Paris. After having been the chair of the french chapter of the ACM SIGOPS from 2011 to 2014, he acted as treasurer from 2014 to 2016. he received the PhD degree from UPMC Sorbonne Université in 2005 and his "Habilitation à diriger les recherche", also from UPMC Sorbonne Université, in 2012. From 2014 to 2023, he was full professor at Telecom SudParis/IP Paris, and from 2006 to 2014, he was associate professor at UPMC Sorbonne Université, in the LIP6 laboratory. In 2005, he performed postdoctoral research at the Université de Grenoble "Jospeh Fourier".
