Verified Sequential Malloc/Free

被引：10

作者：

Appel, Andrew W. ^{[1
]}

Naumann, David A. ^{[2
]}

机构：

[1] Princeton Univ, Princeton, NJ 08544 USA

[2] Stevens Inst Technol, Hoboken, NJ 07030 USA

来源：

PROCEEDINGS OF THE 2020 ACM SIGPLAN INTERNATIONAL SYMPOSIUM ON MEMORY MANAGEMENT, ISMM 2020 | 2020年

基金：

美国国家科学基金会;

关键词：

memory management; separation logic; formal verification; FORMAL VERIFICATION;

D O I：

10.1145/3381898.3397211

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We verify the functional correctness of an array-of-bins (segregated free-lists) single-thread malloc/free system with respect to a correctness specification written in separation logic. The memory allocator is written in standard C code compatible with the standard API; the specification is in the Verifiable C program logic, and the proof is done in the Verified Software Toolchain within the Coq proof assistant. Our "resource-aware" specification can guarantee when malloc will successfully return a block, unlike the standard Posix specification that allows malloc to return NULL whenever it wants to. We also prove subsumption (refinement): the resource-aware specification implies a resource-oblivious spec.

引用

页码：48 / 59

页数：12

共 39 条

[31]

Tuch H, 2009, J AUTOM REASONING, V42, P125, DOI 10.1007/s10817-009-9120-2

[32]

Vanspauwen Gijs, 2017, CW Reports, V2017

[33]

Wang Shengyi, 2019, P ACM PROGR LANG OOP

[34] Towards Optimization-Safe Systems: Analyzing the Impact of Undefined Behavior [J].

Wang, Xi ;

Zeldovich, Nickolai ;

Kaashoek, M. Frans ;

Solar-Lezama, Armando .

SOSP'13: PROCEEDINGS OF THE TWENTY-FOURTH ACM SYMPOSIUM ON OPERATING SYSTEMS PRINCIPLES, 2013, :260-275

[35]

Weinstock Charles B., 1976, Ph.D. Dissertation

[36]

Wickerson J, 2010, LECT NOTES COMPUT SC, V6012, P610, DOI 10.1007/978-3-642-11957-6_32

[37] Verified Correctness and Security of mbedTLS HMAC-DRBG [J].

Ye, Katherine Q. ;

Green, Matthew ;

Sanguansin, Naphat ;

Beringer, Lennart ;

Petcher, Adam ;

Appel, Andrew W. .

CCS'17: PROCEEDINGS OF THE 2017 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY, 2017, :2007-2020

[38]

Yu Zhang, 2019, Dependable Software Engineering. Theories, Tools, and Applications. 5th International Symposium, SETTA 2019. Proceedings. Lecture Notes in Computer Science (LNCS 11951), P122, DOI 10.1007/978-3-030-35540-1_8

[39] A Formally Verified NAT [J].

Zaostrovnykh, Arseniy ;

Pirelli, Solal ;

Pedrosa, Luis ;

Argyraki, Katerina ;

Candea, George .

SIGCOMM '17: PROCEEDINGS OF THE 2017 CONFERENCE OF THE ACM SPECIAL INTEREST GROUP ON DATA COMMUNICATION, 2017, :141-154

← 1 2 3 4 →