Sponsor
This work was supported by the National Science Foun-dation under Grant No. 2048499, Specifying and Verifying Secure Compilation of C Code to Tagged Hardware; by ERC Starting Grant SECOMP (715753), Efficient Formally Secure Compilers to a Tagged Architecture; by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) as part of the Excellence Strategy of the German Federal and State Governments, EXC 2092 CASA - 390781972; by NSF award #2145649, CAREER: Fuzzing Formal Specifications, by NSF award #1955610, Bringing Python Up To Speed, and by NSF award #1521523, Expeditions in Computing: The Science of Deep Specification.
Published In
IEEE
Document Type
Pre-Print
Publication Date
8-2023
Subjects
Computer security, Computer security -- Evaluation -- Methodology
Abstract
The term stack safety is used to describe a variety of compiler, runtime, and hardware mechanisms for protecting stack memory. Unlike “the heap,” the ISA-level stack does not correspond to a single high-level language concept: different compilers use it in different ways to support procedural and functional abstraction mechanisms from a wide range of languages. This protean nature makes it difficult to nail down what it means to correctly enforce stack safety.
Rights
Copyright (c) 2023 The Authors
Locate the Document
DOI
10.1109/CSF57540.2023.00037
Persistent Identifier
https://archives.pdx.edu/ds/psu/40811
Citation Details
Published as: Anderson, S. N., Blanco, R., Lampropoulos, L., Pierce, B. C., & Tolmach, A. (2023, July). Formalizing Stack Safety as a Security Property. In 2023 IEEE 36th Computer Security Foundations Symposium (CSF) (pp. 356-371). IEEE.
Description
This is the author’s version of a work that was accepted for publication in IEEE. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published in IEEE.