Formalizing Stack Safety as a Security Property

• URL: http://arxiv.org/abs/2105.00417v4
• Date: Thu, 21 Mar 2024 10:28:34 GMT
• Title: Formalizing Stack Safety as a Security Property
• Authors: Sean Noble Anderson, Roberto Blanco, Leonidas Lampropoulos, Benjamin C. Pierce, Andrew Tolmach,
• Abstract summary: We propose a new formal characterization of stack safety using concepts from language-based security. This formulation is motivated by a particular class of enforcement mechanisms, the "lazy" stack safety micro-policies studied by Roessler and DeHon. We validate the properties by using them to distinguish between correct and incorrect implementations of Roessler and DeHon's micro-policies.
• Score: 0.6466206145151128
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The term stack safety is used to describe a variety of compiler, run-time, 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. We propose a new formal characterization of stack safety using concepts from language-based security. Rather than treating stack safety as a monolithic property, we decompose it into an integrity property and a confidentiality property for each of the caller and the callee, plus a control-flow property: five properties in all. This formulation is motivated by a particular class of enforcement mechanisms, the "lazy" stack safety micro-policies studied by Roessler and DeHon, which permit functions to write into one another's frames but taint the changed locations so that the frame's owner cannot access them. No existing characterization of stack safety captures this style of safety; we capture it here by stating our properties in terms of the observable behavior of the system. Our properties go further than previous formal definitions of stack safety, supporting caller- and callee-saved registers, arguments passed on the stack, and tail-call elimination. We validate the properties by using them to distinguish between correct and incorrect implementations of Roessler and DeHon's micro-policies using property-based random testing. Our test harness successfully identifies several broken variants, including Roessler and DeHon's lazy policy; a repaired version of their policy passes our tests.

Related papers

• ReF Decompile: Relabeling and Function Call Enhanced Decompile [50.86228893636785]
  The goal of decompilation is to convert compiled low-level code (e.g., assembly code) back into high-level programming languages. This task supports various reverse engineering applications, such as vulnerability identification, malware analysis, and legacy software migration.
  arXiv  Detail & Related papers  (2025-02-17T12:38:57Z)
• SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations [0.15800607910450126]
  We address the problem of preserving non-interference across compiler transformations under speculative semantics. We develop a proof method that ensures the preservation uniformly across all source programs.
  arXiv  Detail & Related papers  (2024-07-21T07:30:30Z)
• SORRY-Bench: Systematically Evaluating Large Language Model Safety Refusal Behaviors [64.9938658716425]
  Existing evaluations of large language models' (LLMs) ability to recognize and reject unsafe user requests face three limitations. First, existing methods often use coarse-grained of unsafe topics, and are over-representing some fine-grained topics. Second, linguistic characteristics and formatting of prompts are often overlooked, like different languages, dialects, and more -- which are only implicitly considered in many evaluations. Third, existing evaluations rely on large LLMs for evaluation, which can be expensive.
  arXiv  Detail & Related papers  (2024-06-20T17:56:07Z)
• Characterizing Unsafe Code Encapsulation In Real-world Rust Systems [2.285834282327349]
  Interior unsafe is an essential design paradigm advocated by the Rust community in system software development. The Rust compiler is incapable of verifying the soundness of a safe function containing unsafe code. We propose a novel unsafety isolation graph to model the essential usage and encapsulation of unsafe code.
  arXiv  Detail & Related papers  (2024-06-12T06:59:51Z)
• AdaShield: Safeguarding Multimodal Large Language Models from Structure-based Attack via Adaptive Shield Prompting [54.931241667414184]
  We propose textbfAdaptive textbfShield Prompting, which prepends inputs with defense prompts to defend MLLMs against structure-based jailbreak attacks. Our methods can consistently improve MLLMs' robustness against structure-based jailbreak attacks.
  arXiv  Detail & Related papers  (2024-03-14T15:57:13Z)
• SECOMP: Formally Secure Compilation of Compartmentalized C Programs [2.5553752304478574]
  Undefined behavior in C often causes devastating security vulnerabilities. We introduce SECOMP, a compiler for compartmentalized C code with machine-checked proofs. This is the first time such a strong criterion is proven for a mainstream programming language.
  arXiv  Detail & Related papers  (2024-01-29T16:32:36Z)
• Static Deadlock Detection for Rust Programs [6.596623081054982]
  Rust relies on its unique ownership mechanism to ensure thread and memory safety. New language features in Rust pose new challenges for vulnerability detection. This paper proposes a static deadlock detection method tailored for Rust programs.
  arXiv  Detail & Related papers  (2024-01-02T09:09:48Z)
• Certifying LLM Safety against Adversarial Prompting [70.96868018621167]
  Large language models (LLMs) are vulnerable to adversarial attacks that add malicious tokens to an input prompt. We introduce erase-and-check, the first framework for defending against adversarial prompts with certifiable safety guarantees.
  arXiv  Detail & Related papers  (2023-09-06T04:37:20Z)
• Safe Deep Reinforcement Learning by Verifying Task-Level Properties [84.64203221849648]
  Cost functions are commonly employed in Safe Deep Reinforcement Learning (DRL) The cost is typically encoded as an indicator function due to the difficulty of quantifying the risk of policy decisions in the state space. In this paper, we investigate an alternative approach that uses domain knowledge to quantify the risk in the proximity of such states by defining a violation metric.
  arXiv  Detail & Related papers  (2023-02-20T15:24:06Z)
• Unsafe's Betrayal: Abusing Unsafe Rust in Binary Reverse Engineering toward Finding Memory-safety Bugs via Machine Learning [20.68333298047064]
  Rust provides memory-safe mechanisms to avoid memory-safety bugs in programming. Unsafe code that enhances the usability of Rust provides clear spots for finding memory-safety bugs. We claim that these unsafe spots can still be identifiable in Rust binary code via machine learning.
  arXiv  Detail & Related papers  (2022-10-31T19:32:18Z)
• A first-order logic characterization of safety and co-safety languages [63.29821624186913]
  Safety and co-safety languages, where a finite prefix suffices to establish whether a word does not belong or belongs to a language, play a crucial role in lowering the complexity of problems like model checking and reactive synthesis. This paper introduces a fragment of FO-TLO, called SafetyFO, and of its dual coSafety, which are expressively complete with respect to the safety and co-safety languages.
  arXiv  Detail & Related papers  (2022-09-06T09:00:38Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.