Memory-safety bugs are a major source of vulnerabilities in C code. Much work has focused on spatial memory safety (e.g., buffer overflows), while temporal memory safety (e.g., use-after-free) has received less attention. One solution for achieving temporal memory safety is to apply an ownership model to an existing program and enforce it. In this paper, we describe the design and implementation of a new temporal memory safety model for C source code. Our design improves on CERT's Pointer Ownership Model with enhancements including use of a SAT solver to enforce constraint satisfaction, LLMs to complete a per-program model, and an improved mechanism to prevent use-after-free errors inspired by Rust's borrow checker and object lifetimes. Our implementation performed well on a large test suite of memory-safe and memory-unsafe code examples. We tested all 4,604 C code examples for the 5 CWEs associated with temporal memory safety (CWEs 401, 415, 416, 590, 761) from the Juliet C/C++ test suite. In our tests, all of the memory-unsafe examples were correctly recognized as unsafe, and 81% of the 2,302 memory-safe examples were correctly recognized as memory-safe.

Tue 16 Jun

Displayed time zone: Mountain Time (US & Canada) change

10:40 - 12:20
Session 3: Formal Methods and Systems ReliabilityLCTES at Flatirons 3
Chair(s): Sanjiva Prasad Indian Institute of Technology Delhi
10:40
22m
Talk
Towards Verifiable System Code using a DSL Compiled to Efficient and Readable C CodeArtifacts AvailableArtifacts Evaluated
LCTES
Clément Chavanon Inria, Univ Rennes, CNRS, IRISA, Henrik Karlsson KTH Royal Institute of Technology, Frédéric Besson Univ Rennes, Inria, CNRS, IRISA, Sandrine Blazy University of Rennes, Roberto Guanciale KTH Royal Institute of Technology
DOI
11:02
22m
Talk
A Pointer-Ownership Model for C Inspired by RustResults ReproducedArtifacts AvailableArtifacts Evaluated
LCTES
David Svoboda , William Klieber Software Engineering Institute, Carnegie Mellon University, Lori Flynn CERT, Ruben Martins Carnegie Mellon University, Jeffrey Hoskinson Software Engineering Institute, Carnegie Mellon University
DOI
11:24
22m
Talk
Hikami: A Lightweight Hypervisor for Emulating RISC-V Extension Semantics with Sail-Driven Auto-generationResults ReproducedArtifacts Available
LCTES
Norimasa Takana University of Tsukuba, Yoshihiro Oyama University of Tsukuba
DOI
11:46
10m
Short-paper
Scheduled Partial-Credit RL for Reliable Code Generation with Small Language Models (WIP)
LCTES
Suryansh Singh Sijwali The Pennsylvania State University, Suman Saha pc
DOI