ABSTRACT. Rabbit is a modeling language for networked systems that allows processes and their communications to be programmed using familiar imperative constructs, while enabling various security assertions to be automatically verified via the Tamarin prover as a back-end. We propose an extension of Rabbit with general unbounded and nondeterministic loops, which are essential for modeling more realistic scenarios, along with optimization techniques that keep automatic verification via Tamarin tractable. We further introduce parameterized processes and communication channels, making Rabbit expressive enough to model systems such as a centralized server communicating with an unbounded number of client processes via a family of parameterized channels. We provide a proof-of-concept implementation of the extended Rabbit and present evaluation results.

ABSTRACT. Cloud computing providers employ sophisticated authorization engines to decide when a request to access a resource should be allowed or denied. Several approaches have formalized the behavior of individual authorization policies, but authorization engines employ multiple types of policies that can interact in different ways. This paper presents a modular formalization of the Amazon Web Services (AWS) authorization engine and a corresponding analysis tool, called Ginkgo, for verifying properties pertaining to multiple policies of different types. Ginkgo adopts Zelkova--i.e., the formalization of individual IAM policies--as a basic building block, and uses a new domain-specific language for modularly describing how the authorization engine composes individual uses of Zelkova. As a result, Ginkgo provides a trusted, reusable, human-readable, and performant SMT-backed model of AWS's authorization logic that is now used within multiple AWS applications. We have run conformance testing of our model against the engine implementation and its documentation; the corner cases identified by our testing have led to improvements and modifications to the official AWS documentation.

ABSTRACT. Compilers for programmable hardware accelerators are complex and involve progressively lowering an application down to the hardware. Bugs can be introduced at many different stages, but simulation does not provide full bug coverage and has poor bug localization. We propose a methodology for automated formal translation validation of compilers for statically scheduled accelerators. This includes generating symbolic representations of every stage in the application compiler and the hardware, leveraging scheduling information for automatically generating translation validation queries, and implementing performance enhancements for effective formal verification. This work provides a blueprint for rigorous verification of compilers and generators for hardware accelerators.

ABSTRACT. DQMax#SAT is a newly developed extension of Max#SAT that incorporates Henkin-type quantifiers and is utilized in function synthesis to enhance program security. This study refutes the earlier hypothesis that efficient reduction from DQMax#SAT to the dependency stochastic Boolean satisfiability (DSSAT) is not possible. We introduce a conversion algorithm that eliminates variables from dependency sets to achieve the reduction. Experimental results show that transforming DQMax#SAT formulas that encode function synthesis applications into DSSAT formulas and solving them using an off-the-shelf DSSAT solver yields superior results compared to directly solving them with the leading DQMax#SAT solver. This research not only clarifies the relationship between DQMax#SAT and DSSAT but also equips developers with conversion tools to assist in the evaluation of both DQMax#SAT and DSSAT solvers.

ABSTRACT. String constraint solving describes the problem of determining the satisfiability of first-order formulas where variables range over strings. Automated procedures for solving these problems are known as string solvers. Most existing solvers adopt a lazy SMT approach, where a SAT solver handles the Boolean structure of the formula and alternates with a specialized string reasoning engine, following the CDCL(T) paradigm. An alternative strategy, called eager SMT solving, reduces the entire problem to Boolean satisfiability, allowing it to be handled directly by a SAT solver. While successful eager approaches have been proposed, current implementations either lack expressiveness or are not publicly available. Here, we present a new eager string solver based on existing techniques, capable of solving Boolean combinations of word equations, regular constraints, and linear arithmetic over string lengths. An evaluation on the SMT-LIB string benchmarks shows that our approach is competitive on a broad set of problems compared to state-of-the-art solvers, and even outperforms them in many cases. In particular, our solver demonstrates near best-in-class performance on the SMT-COMP pure string benchmarks.

ABSTRACT. The Realizable, Responsive, Unobtrusive Unit (R2U2) is a real-time, temporal logic-based runtime monitoring engine that has been successfully deployed on-board a wide range of cyber-physical systems, from aircraft to spacecraft to robots, checking in real time whether these systems uphold specified system requirements. However, the efficacy of deploying runtime monitors is highly sensitive to their correct configuration. Moreover, there are many barriers to adopting runtime monitors, including a high learning curve and the challenge of eliciting formal specifications that accurately capture system requirements. Therefore, we present the R2U2 Playground, an interactive web-based playground that provides visualization of R2U2. The R2U2 Playground provides stepwise execution coupled with reactive timeline plotting and visualization of its internal abstract syntax tree architecture. To this extent, the R2U2 Playground provides insight into how R2U2 evaluates specifications, allowing for easier specification understanding and debugging.

ABSTRACT. In recent years, methods based on Symbolic Computer Algebra (SCA) have become increasingly successful in the field of formal verification of arithmetic circuits. While several different approaches have been proposed to tackle this challenging task, most of them are based on the same mathematical operations. They perform ideal membership tests that reduce specification polynomials by a series of polynomial divisions. For integer arithmetic, under certain conditions, the polynomial divisions boil down to substitutions of variables in integer polynomials. In this context, the overall performance of an SCA verification tool is closely related to the efficiency of the steps manipulating integer polynomials. In this paper we present our tool FastPoly, a package for representing integer polynomials that provides efficient operations including variable substitution with integrated normalization steps. We provide the sources of our tool, making it available for other research groups to support future progress in this field.

ABSTRACT. We present OSTRICH2, the latest evolution of the SMT solver OSTRICH for string constraints. OSTRICH2 supports a wide range of complex functions on strings and provides completeness guarantees for a substantial fragment of string constraints, including the straight-line fragment and the chain-free fragment. OSTRICH2 provides full support for the SMT-LIB theory of Unicode strings, extending the standard with several unique features not found in other solvers: among others, parsing of ECMAScript regular expressions (including look‐around assertions and capture groups) and handling of user‐defined string transducers. We empirically demonstrate that OSTRICH2 is competitive to other string solvers on SMT-COMP benchmarks.

ABSTRACT. Software fault isolation (SFI) is a popular way to sandbox untrusted software. A key component of SFI is the verifier that checks the untrusted code is written in a subset of the machine language that guarantees it never reads or writes outside of a region of memory dedicated to the sandbox. Soundness bugs in the SFI verifier completely break the SFI security model and allow the supposedly sandboxed code to read protected memory. In this paper, we address the concern of verifier bugs by performing an automated formal verification of a popular software fault isolation system called LFI. In particular, we formally verify that programs accepted by the verifier are memory safe, i.e., never read or write to memory outside of a designated sandbox region.

ABSTRACT. The results of software verification are only as trustworthy as the provided specification. Errors or incompleteness in the specification can result in unwarranted confidence in the implementation. Previous work, particularly in the realm of model checking, has investigated a notion of coverage in verification. Portions of the system that could be replaced arbitrarily without causing verification failure are considered uncovered. We show that the same notion of coverage used in model checking can be applied to deductive software verification, with a reasonable performance penalty when using an implementation based on unsatisfiable cores. This approach provides opportunities for identifying specification gaps by detecting vacuous proofs, unconstrained code, and unnecessary or redundant specifications. We describe an implementation of this approach for the Boogie intermediate verification language, the use of this implementation from the verification-aware programming language Dafny, and experimental results on a large corpus of industry-scale Dafny code.

ABSTRACT. The Rust type system provides strong compile-time guarantees. However, some properties cannot be fully verified by the compiler. Specifically, properties like panic freedom and memory safety in mixed safe-unsafe code require verification beyond what the language enforces. We explore how to verify these properties in real-world Rust code using SEABMC, a bounded model checker that ingests LLVM-IR generated by the Rust compiler. We demonstrate our approach through two case studies. In the first, we develop unit proofs of functional properties of four data-structure libraries: SMALLVEC, TINYVEC, SEAVEC, and RESULT-TYPE from the Rust standard library. These unit proofs are checkable by both SEABMC and KANI, a state-of-the-art bounded model checker for Rust, and we find that SeaBMC verifies these units an order of magnitude faster than Kani. The second case study focuses on verifying panic freedom of Wasmtime’s WINCH compiler. This application is driven by the requirement for high reliability when compiling WASM smart-contracts in the Stellar network. This case study highlights that executable counterexamples from SEABMC are highly effective for localizing issues and discovering invariants. Our main contributions are (1) a new tool for Rust verification which, on our benchmarks, is an order of magnitude faster than KANI, (2) two case studies with reusable benchmarking and testing infrastructure, and (3) practical guidelines stemming from our experience verifying real-world code-bases.