Rely-guarantee Reasoning about Concurrent Memory Management: Correctness, Safety and Security

TL;DR

This paper presents a formal specification and mechanized proof of concurrent memory management in Zephyr RTOS, ensuring correctness, safety, and security through rely-guarantee reasoning, and identifies bugs in the implementation.

Contribution

It introduces the first formal specification and verification of Zephyr's memory management, extending rely-guarantee reasoning to security and uncovering implementation bugs.

Findings

Formal specification of Zephyr RTOS memory management

Verification of safety and security properties

Identification of three bugs in the source code

Abstract

Formal verification of concurrent operating systems (OSs) is challenging, in particular the verification of the dynamic memory management due to its complex data structures and allocation algorithm. An incorrect specification and implementation of the memory management may lead to system crashes or exploitable attacks. This article presents the first formal specification and mechanized proof of a concurrent memory management for a real-world OS concerning a comprehensive set of properties, including functional correctness, safety and security. To achieve the highest assurance evaluation level, we develop a fine-grained formal specification of the Zephyr RTOS buddy memory management, which closely follows the C code easing validation of the specification and the source code. The rely-guarantee-based compositional verification technique has been enforced over the formal model. To support formal verification of the security property, we extend our rely-guarantee framework PiCore by a compositional reasoning approach for integrity. Whilst the security verification of the design shows that it preserves the integrity property, the verification of the functional properties shows several problems. These verification issues are translated into finding three bugs in the C implementation of Zephyr, after inspecting the source code corresponding to the design lines breaking the properties.