Sponsor
Portland State University. Department of Computer Science
First Advisor
Andrew P. Tolmach
Term of Graduation
Fall 2024
Date of Publication
12-12-2024
Document Type
Dissertation
Degree Name
Doctor of Philosophy (Ph.D.) in Computer Science
Department
Computer Science
Language
English
Subjects
Formal Methods, Formal Verification, Programming Languages, Theoretical Security
Physical Description
1 online resource (xii, 166 pages)
Abstract
The C language is ubiquitous and insecure. Tag-based security policies offer a flexible toolkit for runtime protection, including policies that mitigate the effects of undetected programming bugs and those that enforce security properties of the program logic. But tag policies can be difficult to define, and the protection that they offer can be difficult to specify and to prove.
This dissertation builds from an assembly-level specification of stack safety, encompassing the essential control-flow structure of C and other high level languages, to a C source-level policy definition framework called Tagged C. Tagged C includes a variant C semantics parameterized by a user-defined tag policy, and an interpreter that provably implements that semantics. It is flexible enough to define a wide range of security policies, including memory safety, compartmentalization, and secure infor- mation flow. Finally, introduces a novel compartmentalization policy, CluMPS, with a formal specification and an implementation in Tagged C, verified by mechanized proof in Coq.
Rights
In Copyright. URI: http://rightsstatements.org/vocab/InC/1.0/ This Item is protected by copyright and/or related rights. You are free to use this Item in any way that is permitted by the copyright and related rights legislation that applies to your use. For other uses you need to obtain permission from the rights-holder(s).
Persistent Identifier
https://archives.pdx.edu/ds/psu/42912
Recommended Citation
Anderson, Sean Noble, "Tag-based Security in C: Writing and Specifying Flexible Protection" (2024). Dissertations and Theses. Paper 6737.
Comments
This work was supported by the National Science Foundation under Grant No. 2048499, Specifying and Verifying Secure Compilation of C Code to Tagged Hardware. This material is based upon work supported by the Defense Advanced Research Projects Agency (DARPA) under Contract No. HR0011-18-C-0011.