Tagged “concurrency”

• Specifying and Verifying the NOVA Microhypervisor in Concurrent Separation Logic

  Jan 17, 2026

  We present the current progress of specifying and verifying the NOVA microhypervisor at BlueRock Security. We carry out these tasks using the BRiCk C++ program logic and verification tools, building on top of the Iris framework for concurrent separation logics (CSLs), in Rocq. We found that the use of CSLs has enabled us to carry out highly modular specifications and verifications of even sophisticated, fine-grained concurrent algorithms in NOVA. We believe this is a significant step forward over other hypervisor verification projects that are either limited to single-threaded verification or are highly non-modular.

  rocq c++ program verification separation logic brick concurrency nova hypervisor skylabs-ai bluerock-security

• Recursive Mutexes in Separation Logic

  Jan 17, 2026

  Mutexes (i.e., locks) are well understood in separation logic, and can be specified in terms of either protecting an invariant or atomically changing the state of the lock. In this abstract, we develop the same styles of specifications for _recursive_ mutexes, a common variant of mutexes in object-oriented languages like C++ and Java. A recursive mutex can be acquired any number of times by the same thread, and our specifications treat all acquires/releases uniformly, with clients only needing to determine whether they hold the mutex when accessing the lock invariant.

  rocq c++ program verification separation logic brick concurrency skylabs-ai

• Modular, Full-System Verification

  May 14, 2025

  We present an approach to specifying operating systems that is both highly modular and supports deriving various properties necessary to modern operating systems. The approach combines a machine semantics decomposed by privilege levels with a separation logic specification of the operating system API. We describe how the specification style enables natural proofs of robust safety in addition to deep behavioral refinements of user-mode applications running atop the OS. This approach enables simple and flexible concurrent specifications and unlocks new opportunities for whole-system verification.

  microkernel full-system c++ program verification separation logic brick concurrency