TY - GEN
T1 - Fine-grained formal specification and analysis of buddy memory allocation in zephyr RTOS
AU - Feng, Zhang
AU - Yongwang, Zhao
AU - Dianfu, Ma
AU - Wensheng, Niu
N1 - Publisher Copyright:
© 2019 IEEE.
PY - 2019/5
Y1 - 2019/5
N2 - Bugs in memory management of Operating Systems may lead to crashing. This paper presents a case study of formal verification on the buddy memory allocation component of the Zephyr RTOS kernel. The algorithm of the component allows memory blocks of 4-power sizes to be dynamically allocated by efficiently partitioning larger blocks into smaller ones, and then be released supporting immediate and automatic combining of smaller blocks. The execution of memory allocation is preemptive, which means that the allocation may invoke rescheduling when there is no block available for memory requests. In this paper, we provide a fine-grained formal specification of buddy memory allocation and formally verify its safety via invariants and functional correctness. The specification covers all the elements of the data structure as well as all statements of memory initialization, allocation, and release presented in the C source code. During the formal verification, we found a functional flaw in the C code. To the best of our knowledge, this paper is the first effort of formal verification at a fine-grained level on buddy memory allocation in Operating Systems.
AB - Bugs in memory management of Operating Systems may lead to crashing. This paper presents a case study of formal verification on the buddy memory allocation component of the Zephyr RTOS kernel. The algorithm of the component allows memory blocks of 4-power sizes to be dynamically allocated by efficiently partitioning larger blocks into smaller ones, and then be released supporting immediate and automatic combining of smaller blocks. The execution of memory allocation is preemptive, which means that the allocation may invoke rescheduling when there is no block available for memory requests. In this paper, we provide a fine-grained formal specification of buddy memory allocation and formally verify its safety via invariants and functional correctness. The specification covers all the elements of the data structure as well as all statements of memory initialization, allocation, and release presented in the C source code. During the formal verification, we found a functional flaw in the C code. To the best of our knowledge, this paper is the first effort of formal verification at a fine-grained level on buddy memory allocation in Operating Systems.
KW - Buddy memory allocation
KW - Fine-grained formal specification and analysis
KW - Functional correctness
KW - Zephyr
UR - https://www.scopus.com/pages/publications/85070356278
U2 - 10.1109/ISORC.2019.00013
DO - 10.1109/ISORC.2019.00013
M3 - 会议稿件
AN - SCOPUS:85070356278
T3 - Proceedings - 2019 IEEE 22nd International Symposium on Real-Time Distributed Computing, ISORC 2019
SP - 10
EP - 17
BT - Proceedings - 2019 IEEE 22nd International Symposium on Real-Time Distributed Computing, ISORC 2019
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 22nd IEEE International Symposium on Real-Time Distributed Computing, ISORC 2019
Y2 - 7 May 2019 through 9 May 2019
ER -