English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Formal verification of concurrent operating systems (OSs) is challenging, inparticular the verification of the dynamic memory management due to its complexdata structures and allocation algorithm. An incorrect specification andimplementation of the memory management may lead to system crashes orexploitable attacks. This article presents the first formal specification andmechanized proof of a concurrent memory management for a real-world OSconcerning a comprehensive set of properties, including functional correctness,safety and security. To achieve the highest assurance evaluation level, wedevelop a fine-grained formal specification of the Zephyr RTOS buddy memorymanagement, which closely follows the C code easing validation of thespecification and the source code. The rely-guarantee-based compositionalverification technique has been enforced over the formal model. To supportformal verification of the security property, we extend our rely-guaranteeframework PiCore by a compositional reasoning approach for integrity. Whilstthe security verification of the design shows that it preserves the integrityproperty, the verification of the functional properties shows several problems.These verification issues are translated into finding three bugs in the Cimplementation of Zephyr, after inspecting the source code corresponding to thedesign lines breaking the properties.

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