Cloud computing relies on hypervisors to enforce isolation between co-tenanted virtual machines. Hypervisors are therefore critical security infrastructure, and assurance of their correctness is paramount. Traditional engineering techniques - code review, testing, fuzzing - provide strong assurance but cannot exhaustively verify that isolation holds across all possible execution paths. Formal verification extends and complements these approaches by establishing mathematical guarantees about system behaviour. This talk presents our experience applying interactive theorem proving to verify a production hypervisor component: the Nitro Isolation Engine. This is a trusted, minimalist computing base written in Rust, enforcing isolation between virtual machines on AWS Graviton5 EC2 instances. Designed for verification from inception, we have specified the intended behaviour of this component and verified correctness in the Isabelle/HOL interactive theorem prover, producing approximately 330,000 lines of machine-checked models and proofs, and establishing three key classes of property: 1) Functional correctness: The system behaves as specified for all operations including virtual machine creation, memory mapping, and abort handling. Our total verification approach additionally establishes memory-safety, termination, and absence of runtime errors. 2) Confidentiality: A noninterference-style property demonstrates that guest virtual machine state remains hidden from an expansive definition of observer monitoring system actions, formalised as indistinguishability preservation up to permitted declassification flows. 3) Integrity: Guest virtual machine private state is unaffected by operations on distinct virtual machines. Currently, our proof coverage extends to verification of the core virtual machine-management hypercalls, guest power management, various utility hypercalls, and a subset of data, instruction, and asynchronous abort handling, and will continue to expand to cover more functionality including PCI device management and virtual GIC (Generic Interrupt Controller) handling. The talk will discuss the verification approach, key proof techniques, and challenges in applying formal methods to production systems. Note that this work builds on decades of academic research across interactive theorem proving, formal specification, separation logic and its automation, and programming language semantics.

Abstract Many security- and performance-critical domains, such as cryptography, rely on low-level verification to minimize the trusted computing surface and allow code to be written directly in assembly. However, verifying assembly code against a realistic machine model is a challenging task. Furthermore, certain security properties—such as constant-time behavior—require relational reasoning that goes beyond traditional correctness by linking multiple execution traces within a single specification. Yet, relational verification has been extensively explored at a higher level of abstraction. In this work, we introduce a Hoare-style logic that provides low-level, expressive relational verification. We demonstrate our approach on the s2n-bignum library, proving both constant-time discipline and equivalence between optimized and verification-friendly routines. Formalized in HOL Light, our results confirm the real-world applicability of relational verification in large assembly codebases.

Firmware validation is driven by imperatives and challenges distinct from those of application level software. In this tutorial we will survey the characteristics of firmware projects, focusing on those that make them particularly challenging and important to validate. Well look at the tasks accomplished using firmware, the environments in which it executes, and how firmware is shaped by the constraints imposed by the greater product development program in which it fits. Finally, well look at some of our experiences in firmware validation and the lessons weve learned from them. Specifically, well be looking for lessons that can help to guide the selection of problems to study and appropriate case studies on which to evaluate them.

We present a new 2-phase symbolic execution driven strategy that achieves high branch coverage in software quickly. Phase 1 follows a greedy approach that quickly covers as many branches as possible by exploring each branch through its corresponding shortest path prefix. Phase 2 covers the remaining branches that are left uncovered if the shortest path to the branch was infeasible. In Phase 1, a basic conflict-driven learning is used to skip all the paths that may have any of the earlier encountered conflicting conditions, while in Phase 2, a more intelligent conflict-driven learning is used to skip regions that do not have a feasible path to any unexplored branch. This results in considerable reduction in unnecessary SMT solver calls. Experimental results show that significant speedup can be achieved, effectively reducing the time to detect a bug and providing higher branch coverage for a fixed time-out period than previous techniques.

The Verilog hardware description language has padding semantics that allow designers to write descriptions where wires of different bit widths can be interconnected. However, many of these connections are nothing more than bugs inadvertently introduced by the designer and often result in circuits that behave incorrectly or use more resources than required. A similar problem occurs when wires are incorrectly indexed by values (or ranges) that exceed their bounds. These two problems are exacerbated by generate blocks. While desirable for reusability and conciseness, the use of generate blocks to describe circuit families only makes the situation worse as it hides such inconsistencies making them harder to detect. Inconsistencies in the generated code are only exposed after elaboration when the code is fully-expanded.In this paper we show that these inconsistencies can be pinned down prior to elaboration using static analysis.We combine dependent types and constraint generation to reduce the problem of detecting the aforementioned inconsistencies to a satisfiability problem. Once reduced, the problem can easily be solved with a standard satisfiability modulo theories (SMT) solver. In addition, this technique allows us to detect unreachable code when it resides in a block guarded by an unsatisfiable set of constraints. To illustrate these ideas, we develop a type system for Featherweight Verilog (FV), a core calculus of structural Verilog with generative constructs and previously defined elaboration semantics. We prove that a well-typed FV description will always elaborate into an inconsistency-free description. We also provide a freely-available implementation demonstrating our approach.

Modern hardware description languages support code-generation constructs like generate/endgenerate in Verilog. These constructs are intended to describe regular or parameterized hardware designs and, when used effectively, can make hardware descriptions shorter, more understandable, and more reusable. In practice, however, designers avoid these constructs because it is difficult to understand and predict the properties of the generated code. Is the generated code even type safe? Is it synthesizable? What physical resources (e.g. combinatorial gates and flip-flops) does it require? It is often impossible to answer these questions without first generating the fully-expanded code. In the Verilog and VHDL communities, this generation process is referred to as elaboration.

This paper introduces reFLect, a functional programming language with reflection features intended for applications in hardware design and verification. The reFLect language is strongly typed and similar to ML, but has quotation and antiquotation constructs. These may be used to construct and decompose expressions in the reFLect language itself. The paper motivates and presents the syntax and type system of this language, which brings together a new combination of pattern-matching and reflection features targeted specifically at our application domain. It also gives an operational semantics based on a novel use of contexts as expression constructors, and it presents a scheme for compiling reFLect programs using the same context mechanism.

Abstract We propose a new format for writing proofs, called structured calculational proof . The format resembles the calculational style already familiar to many computer scientists, but extends it to allow the hierarchical decomposition of larger proofs into smaller ones. Structured calculation is actually an alternative presentation of natural deduction, a style of reasoning which uses hierarchical decomposition to great effect, but which is traditionally expressed in a notation that is inconvenient for writing calculational proofs. The hierarchical nature of structured calculational proofs can be used for browsing proofs in electronic publications.

This paper presents a generalization of Robinson and Staple's window inference system of hierarchical reasoning. The generalization enhances window inference so that it is capable of supporting transformational proofs. In addition, while Robinson and Staples proposed window inference as an alternative to existing styles of reasoning, this paper describes window inference in terms of sequent formulation of natural deduction. Expressing window inference in terms of natural deduction, a style of reasoning already known to be sound, demonstrates the soundness of window inference itself. It also illustrates how mechanized support for window inference can be implemented using existing sequent-based theorem provers. The paper also examines the use of contextual assumptions with window inference. Two definitions of what may be assumed in a context are presented. The first is a general definition; while the second has a simpler form. These definitions are shown to be equivalent for contexts that do not bind variables.