RECORD
Rely-guarantee Reasoning about Concurrent Memory Management: Correctness, Safety and Security
Software Engineering · Submitted 17 Sep 2023
abstract compiled · 2026-09-23 · no language-model review
The authors' main claim 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.
The compiled record
The paper's own sentences, arranged. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.
Open the compiled record
The abstract, sentence by sentence
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.
background contribution method result interpretation main claim
| # | sentence | role | the authors' own work | states the main conclusion | strength |
|---|---|---|---|---|---|
| s0 | 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. | background 1.00 | 0.06 | 0.02 | asserted 1.00 |
| s1 | An incorrect specification and implementation of the memory management may lead to system crashes or exploitable attacks. | background 1.00 | 0.05 | 0.02 | hedged possibility 0.99 |
| s2 | 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. | contribution 1.00 | 0.95 | 0.51 | asserted 1.00 |
| s3 | 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. | method 0.76 | 0.96 | 0.05 | asserted 1.00 |
| s4 | The rely-guarantee-based compositional verification technique has been enforced over the formal model. | method 0.98 | 0.84 | 0.04 | asserted 1.00 |
| s5 | To support formal verification of the security property, we extend our rely-guarantee framework PiCore by a compositional reasoning approach for integrity. | method 0.58 | 0.93 | 0.04 | asserted 1.00 |
| s6 | Whilst the security verification of the design shows that it preserves the integrity property, the verification of the functional properties shows several problems. | result 0.99 | 0.92 | 0.39 | asserted 1.00 |
| s7 | 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. | result 0.98 | 0.95 | 0.27 | asserted 1.00 |
What was examined, and what was not
- arXiv listing abstract v1
- full text
- figures and tables
- references and citing sentences
- relations to other papers
- P abstract
- S sections
- T body sentences
- C citations
- R cross-paper relations
The paper
Original 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.
Human review
Discussion
Know something about this paper? Leave a comment, or highlight any passage above to comment on it.