- author = "Jay Bosamiya",
- title = "A Principled Approach Towards Unapologetic Security",
- school = "Computer Science Department, Carnegie Mellon University",
- year = "2024",
- address = "USA",
- month = may,
- keywords = "genetic algorithms, genetic programming, genetic improvement, Formal Techniques, Unapologetic Security, Software Verification, Cryptographic Implementations, Sandboxing, WebAssembly, Parsing, decompilation, Computer Software, faster instruction orderings",
-
URL = "
https://www.jaybosamiya.com/publications/2024/thesis/bosamiya-thesis.pdf",
-
URL = "
https://kilthub.cmu.edu/articles/thesis/A_Principled_Approach_towards_Unapologetic_Security/25898734?file=46535206",
-
URL = "https://kilthub.cmu.edu/ndownloader/files/46535206",
-
DOI = "
10.1184/R1/25898734.v1",
- size = "170 pages",
-
abstract = "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 underprioritized. 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.",
-
notes = "3.5 Optimizing Code for Each Processor
Generation
CMU-CS-24-127
advised by Bryan Parno",
