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

简介

在这项工作中，我们提出了StarMalloc，这是一个经过验证、面向安全、并发的内存分配器，可用作现实项目中的替代品。我们使用Steel分离逻辑框架来说明如何指定和验证StarMalloc，依靠依赖类型和模块化抽象来实现高效验证。作为StarMalloc的一部分，我们还开发了几个通用数据结构和证明库，可直接在未来的系统验证项目中重复使用。最后，我们展示了StarMalloc可以用于实际项目，包括Firefox浏览器，并将其与10种最先进的内存分配器进行评估，证明了其竞争力。
作者讲解

目前尚无作者解读视频，你可点击下方【许愿开讲】按钮，许愿作者开讲~
图表
解决问题

StarMalloc：一种安全、并发的内存分配器
关键思路

使用依赖类型和模块化抽象，依靠Steel分离逻辑框架，设计和验证了StarMalloc，同时开发了几种通用数据结构和证明库。
其它亮点

StarMalloc可以用于真实项目中，包括Firefox浏览器，并且与10种最先进的内存分配器进行了评估。
相关研究

与该论文相关的研究包括： 1. R. Jones等人的“Safe and Efficient Memory Management in Cyclone” 2. J. Yang等人的“Efficient Verification of Sequential and Concurrent C Programs with Kleene Algebra and Substitution Grammars” 3. Y. Li等人的“Formal Verification of a Concurrent Garbage Collector