StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866929276424552448 |
|---|---|
| author | Reitz, Antonin Fromherz, Aymeric Protzenko, Jonathan |
| author_facet | Reitz, Antonin Fromherz, Aymeric Protzenko, Jonathan |
| contents | In this work, we present StarMalloc, a verified, security-oriented, concurrent memory allocator that can be used as a drop-in replacement in real-world projects. Using the Steel separation logic framework, we show how to specify and verify StarMalloc, relying on dependent types and modular abstractions to enable efficient verification. As part of StarMalloc, we also develop several generic datastructures and proof libraries directly reusable in future systems verification projects. We finally show that StarMalloc can be used with real-world projects, including the Firefox browser, and evaluate it against 10 state-of-the-art memory allocators, demonstrating its competitiveness. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_09435 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator Reitz, Antonin Fromherz, Aymeric Protzenko, Jonathan Programming Languages Cryptography and Security In this work, we present StarMalloc, a verified, security-oriented, concurrent memory allocator that can be used as a drop-in replacement in real-world projects. Using the Steel separation logic framework, we show how to specify and verify StarMalloc, relying on dependent types and modular abstractions to enable efficient verification. As part of StarMalloc, we also develop several generic datastructures and proof libraries directly reusable in future systems verification projects. We finally show that StarMalloc can be used with real-world projects, including the Firefox browser, and evaluate it against 10 state-of-the-art memory allocators, demonstrating its competitiveness. |
| title | StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator |
| topic | Programming Languages Cryptography and Security |
| url | https://arxiv.org/abs/2403.09435 |