A Principled Approach Towards Unapologetic Security

Software is incredibly difficult to write correctly, let alone safely. Prior work (quite successfully) has, amongst other things, relied on formal verification—a powerful hammer to achieve provable guarantees. However, improvements in the state-of-the-art of software security often come with significant apologies for other important objectives, such as development velocity, software performance, or loss of functionality. While many developers (and more so, users) would like their software to be secure, these apologies cause security to become under-prioritized. To be adopted, advances in security thus need to not only improve the state-of-the-art in security, but also focus on other practical considerations that have historically inhibited widespread deployment, and indeed prevented building secure software from being the natural default choice.

In this thesis, we argue that security objectives are achievable without apology, through the use of principled approaches and formalism. To validate this thesis, we look at a collection of case studies that span across a wide collection of different kinds of software systems: (i) high-performance cryptographic primitives, (ii) safe execution of arbitrary untrusted code, (iii) agile safety enforcement for code, (iv) low-level serializers and parsers for untrusted data, and (v) source-unavailable executable comprehension. In each, we demonstrate that principled approaches and formalism help remove the need for the apologies required by prior work.

Our hope is that providing security without apology, even in the face of practical complexities, makes a big step towards the shared goal of security researchers—making security the natural default choice.