StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator

• URL: http://arxiv.org/abs/2403.09435v1
• Date: Thu, 14 Mar 2024 14:29:01 GMT
• Title: StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator
• Authors: Antonin Reitz, Aymeric Fromherz, Jonathan Protzenko,
• Abstract summary: We show how to specify and verify StarMalloc, relying on dependent types and modular abstractions to enable efficient verification. We 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.
• Score: 3.7554217682190365
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: 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.

Related papers

• SJMalloc: the security-conscious, fast, thread-safe and memory-efficient heap allocator [0.0]
  Heap-based exploits pose a significant threat to application security. hardened allocators have not been widely adopted in real-world applications. SJMalloc stores its metadata out-of-band, away from the application's data on the heap. SJMalloc demonstrates a 6% performance improvement compared to GLibcs allocator, while using only 5% more memory.
  arXiv  Detail & Related papers  (2024-10-23T14:47:12Z)
• Host-Based Allocators for Device Memory [1.2289361708127877]
  We pose a model where the allocation algorithm runs on host memory but allocates device memory and so incur the following constraint: the allocator can't read the memory it is allocating. This means we are unable to use boundary tags, which is a concept that has been ubiquitous in nearly every allocation algorithm. In this paper, we propose alternate algorithms to work around this constraint, and discuss in general the implications of this system model.
  arXiv  Detail & Related papers  (2024-05-11T19:28:37Z)
• SeMalloc: Semantics-Informed Memory Allocator [18.04397502953383]
  Use-after-free (UAF) is a critical and prevalent problem in memory unsafe languages. We show one way to balance the trinity by passing more semantics about the heap object to the allocator. In SeMalloc, only heap objects allocated from the same call site and via the same function call stack can possibly share a virtual memory address.
  arXiv  Detail & Related papers  (2024-02-02T21:02:15Z)
• UniRef++: Segment Every Reference Object in Spatial and Temporal Spaces [92.52589788633856]
  We propose UniRef++ to unify the four reference-based object segmentation tasks with a single architecture. With the unified designs, UniRef++ can be jointly trained on a broad range of benchmarks and can flexibly complete multiple tasks at run-time. Our proposed UniRef++ achieves state-of-the-art performance on RIS and RVOS, and performs competitively on FSS and VOS with a parameter-shared network.
  arXiv  Detail & Related papers  (2023-12-25T12:54:11Z)
• rCanary: Detecting Memory Leaks Across Semi-automated Memory Management Boundary in Rust [4.616001680122352]
  Rust is a system programming language that guarantees memory safety via compile-time verifications. We present rCanary, a static, non-automated, and fully automated model checker to detect leaks across semiautomated boundary.
  arXiv  Detail & Related papers  (2023-08-09T08:26:04Z)
• MeMOT: Multi-Object Tracking with Memory [97.48960039220823]
  Our model, called MeMOT, consists of three main modules that are all Transformer-based. MeMOT observes very competitive performance on widely adopted MOT datasets.
  arXiv  Detail & Related papers  (2022-03-31T02:33:20Z)
• CryptSan: Leveraging ARM Pointer Authentication for Memory Safety in C/C++ [0.9208007322096532]
  CryptSan is a memory safety approach based on ARM Pointer Authentication. We present a full LLVM-based prototype implementation, running on an M1 MacBook Pro. This, together with its interoperability with uninstrumented libraries and cryptographic protection against attacks on metadata, makes CryptSan a viable solution for retrofitting memory safety to C/C++ programs.
  arXiv  Detail & Related papers  (2022-02-17T14:04:01Z)
• Robust Object Detection via Instance-Level Temporal Cycle Confusion [89.1027433760578]
  We study the effectiveness of auxiliary self-supervised tasks to improve the out-of-distribution generalization of object detectors. Inspired by the principle of maximum entropy, we introduce a novel self-supervised task, instance-level temporal cycle confusion (CycConf) For each object, the task is to find the most different object proposals in the adjacent frame in a video and then cycle back to itself for self-supervision.
  arXiv  Detail & Related papers  (2021-04-16T21:35:08Z)
• Efficient Regional Memory Network for Video Object Segmentation [56.587541750729045]
  We propose a novel local-to-local matching solution for semi-supervised VOS, namely Regional Memory Network (RMNet) The proposed RMNet effectively alleviates the ambiguity of similar objects in both memory and query frames. Experimental results indicate that the proposed RMNet performs favorably against state-of-the-art methods on the DAVIS and YouTube-VOS datasets.
  arXiv  Detail & Related papers  (2021-03-24T02:08:46Z)
• Kanerva++: extending The Kanerva Machine with differentiable, locally block allocated latent memory [75.65949969000596]
  Episodic and semantic memory are critical components of the human memory model. We develop a new principled Bayesian memory allocation scheme that bridges the gap between episodic and semantic memory. We demonstrate that this allocation scheme improves performance in memory conditional image generation.
  arXiv  Detail & Related papers  (2021-02-20T18:40:40Z)
• DMV: Visual Object Tracking via Part-level Dense Memory and Voting-based Retrieval [61.366644088881735]
  We propose a novel memory-based tracker via part-level dense memory and voting-based retrieval, called DMV. We also propose a novel voting mechanism for the memory reading to filter out unreliable information in the memory.
  arXiv  Detail & Related papers  (2020-03-20T10:05:30Z)

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.