UC San Diego

There has been significant work on defining and guaranteeing security for the components that make up software systems, in particular software fault isolation for untrusted libraries and constant time for cryptographic libraries. But these components exist in the context of a larger application, and there has been comparatively little work on what happens at the boundary between library and application. In this dissertation we examine security in two settings: trusted applications interacting with untrusted third-party libraries and untrusted applications interacting with trusted cryptographic libraries. For each we examine the boundary between application and library, formally defining the security properties required of the transitions between the components. In the case of untrusted third-party libraries we develop a set of zero-cost conditions that capture sufficient structure to ensure a sandboxed library can securely and efficiently context switch to and from the trusted application. In the case of cryptographic libraries we define a notion of robust constant time, characterizing security for cryptographic libraries used in a (potentially unsafe) application. We use our formal security properties to identify and develop compilers to automatically provide security for the overall application and prove that the compilers do indeed guarantee security.