[2507.11282] The downgrading semantics of memory safety (Extended version)

-->

Computer Science > Programming Languages

arXiv:2507.11282 (cs)

[Submitted on 15 Jul 2025 (v1), last revised 17 Apr 2026 (this version, v2)]

Title:The downgrading semantics of memory safety (Extended version)

Authors:René Rydhof Hansen, Andreas Stenbæk Larsen, Aslan Askarov<br>View a PDF of the paper titled The downgrading semantics of memory safety (Extended version), by Ren\'e Rydhof Hansen and 2 other authors

View PDF<br>HTML (experimental)

Abstract:Memory safety is traditionally characterized in terms of bad things that cannot happen. This approach is currently embraced in the literature on formal methods for memory safety. However, a general semantic principle for memory safety, that implies the negative items, remains elusive.

This paper focuses on the allocator-specific aspects of memory safety, such as null-pointer dereference, use after free, double free, and heap overflow. To that extent, we propose a notion of gradual allocator independence that accurately captures the allocator-dependent aspects of memory safety. Our approach is inspired by the previously suggested connection between memory safety and noninterference, but extends that connection in a fundamentally important direction towards downgrading.

We consider a low-level language with access to an allocator that provides malloc and free primitives in a flat memory model. Pointers are just integers, and as such it is trivial to write memory-unsafe programs. The basic intuition of gradual allocator independence is that of noninterference, namely that allocators must not influence program execution. This intuition is refined in two important ways that account for the allocators running out-of-memory and for programs to have pointer-to-integer casts. The key insight of the definition is to treat these extensions as forms of downgrading and give them satisfactory technical treatment using the state-of-the-art information flow machinery.

Comments:<br>65 pages, 26 figures, Extended version of PLDI 2026 paper with the same title

Subjects:

Programming Languages (cs.PL)

Cite as:<br>arXiv:2507.11282 [cs.PL]

(or<br>arXiv:2507.11282v2 [cs.PL] for this version)

https://doi.org/10.48550/arXiv.2507.11282

Focus to learn more

arXiv-issued DOI via DataCite

Related DOI:

https://doi.org/10.1145/3808260

Focus to learn more

DOI(s) linking to related resources

Submission history<br>From: Aslan Askarov [view email]<br>[v1]<br>Tue, 15 Jul 2025 12:59:11 UTC (310 KB)

[v2]<br>Fri, 17 Apr 2026 15:24:10 UTC (236 KB)

Full-text links:<br>Access Paper:

View a PDF of the paper titled The downgrading semantics of memory safety (Extended version), by Ren\'e Rydhof Hansen and 2 other authors<br>View PDF<br>HTML (experimental)<br>TeX Source

view license

Current browse context:

cs.PL

next >

new<br>recent<br>| 2025-07

Change to browse by:

cs

References & Citations

NASA ADS<br>Google Scholar

Semantic Scholar

export BibTeX citation<br>Loading...

BibTeX formatted citation

&times;

loading...

Data provided by:

Bookmark

Bibliographic Tools

Bibliographic and Citation Tools

Bibliographic Explorer Toggle

Bibliographic Explorer (What is the Explorer?)

Connected Papers Toggle

Connected Papers (What is Connected Papers?)

Litmaps Toggle

Litmaps (What is Litmaps?)

scite.ai Toggle

scite Smart Citations (What are Smart Citations?)

Code, Data, Media

Code, Data and Media Associated with this Article

alphaXiv Toggle

alphaXiv (What is alphaXiv?)

Links to Code Toggle

CatalyzeX Code Finder for Papers (What is CatalyzeX?)

DagsHub Toggle

DagsHub (What is DagsHub?)

GotitPub Toggle

Gotit.pub (What is GotitPub?)

Huggingface Toggle

Hugging Face (What is Huggingface?)

ScienceCast Toggle

ScienceCast (What is ScienceCast?)

Demos

Demos

Replicate Toggle

Replicate (What is Replicate?)

Spaces Toggle

Hugging Face Spaces (What is Spaces?)

Spaces Toggle

TXYZ.AI (What is TXYZ.AI?)

Related Papers

Recommenders and Search Tools

Link to Influence Flower

Influence Flower (What are Influence Flowers?)

Core recommender toggle

CORE Recommender (What is CORE?)

Author

Venue

Institution

Topic

About arXivLabs

arXivLabs: experimental projects with community collaborators

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs .

Which authors of this paper are endorsers? |<br>Disable MathJax (What is MathJax?)