Formal Guarantees about Real Software

At BlueRock Security, we are on a mission to secure systems from the ground up. Formal verification is a crucial part of this goal because it is the only way to provide mathematical guarantees about a system. To enable reasoning about software, we are developing state-of-the-art tools to prove that software behaves as intended in all possible situations. Our tools build on decades of research into modular reasoning principles for highly concurrent software.

To date, we have applied these tools to verify (parts of) complex, concurrent C++ code across the BlueRock ULTRA™ stack from the NOVA microhypervisor to user-mode applications including a console multiplexor and a Virtual Machine Monitor (VMM). These verifications have been collaborative efforts between systems engineers with no background in formal methods and formal methods engineers, and the experiences have been beneficial on both sides. Our verification efforts have found and fixed many subtle bugs ranging from shallow undefined behavior to race conditions and semantic bugs across the entire stack.

While we continue our work hardening the BlueRock stack, fully realizing our mission has lead us to enable the broader use of our verification tools outside of BlueRock. This work includes polishing our tools to improve usability and developing specifications for common C++ infrastructure such as the C++ standard library.