At its core, SMACK is a translator from the LLVM compiler’s popular intermediate representation (IR) into the Boogie intermediate verification language (IVL). Sourcing LLVM IR exploits an increasing number of compiler frontends, optimizations, and analyses. Targeting Boogie exploits a canonical platform which simplifies the implementation of algorithms for verification, model checking, and abstract interpretation. The main purpose of SMACK is to decouple the implementations of verification algorithms from the details of source languages, and enable rapid prototyping on production code. Our initial experience verifying C language programs is encouraging: SMACK is competitive in SV-COMP benchmarks, is able to translate large programs (100 KLOC), and is used in several verification research prototypes.
SMACK is hosted on GitHub: https://github.com/smackers/smack
FPTaylor is a tool for rigorous estimation of round-off errors of floating-point computations. It is based on a new approach we developed called Symbolic Taylor Expansions that is more precise than previous approaches. Key to our approach is the use of rigorous global optimization, instead of the more familiar interval arithmetic, affine arithmetic, and/or SMT solvers. In addition to providing far tighter upper bounds of round-off error in a vast majority of cases, FPTaylor also emits analysis certificates in the form of HOL Light proofs.
FPTaylor is hosted on GitHub: https://github.com/soarlab/FPTaylor
Archer is a data race detector for OpenMP programs. It combines static and dynamic techniques to identify data races in large OpenMP applications, leading to low runtime and memory overheads, while still offering high accuracy and precision. It leverages open-source tools and infrastructure such as LLVM and ThreadSanitizer to provide portability. Archer is a part of the larger PRUNER project whose goal is to provide reproducibility in ubiquitously non-deterministic high-performance computing environments and runs. We are working on this project in collaboration with our partners from LLNL.
Developing a software protocol stack (e.g., TCP/IP, Bluetooth, USB) is a complex task with many parties and products involved over multiple years. There are many issues that have to be resolved in the process, and it is incredibly hard to get all of them correct for all platforms and all possible states of a system. Hence, there are numerous examples of serious bugs that ended up in production, where the cost of fixing them is high. We propose a more rigorous approach to developing and maintaining such complex software protocol stacks. In particular, formal methods are introduced to find bugs early through rigorous verification and testing, as well as to assist the analysis when locating reported bugs. The usability of the approach is assessed through a real-life case study on the Android Bluetooth software stack. The approach is based on automatically learning abstract and succinct protocol models at different layers of the target software stack. Then, we apply compositional reasoning to find bugs effectively and precisely. We also leverage the generated models to help with error localization and diagnosis.
Deker is a framework for decomposing and verifying commodity operating system kernels. Deker turns a de facto standard commodity operating system kernel into a collection of strongly isolated subsystems suitable for verification. To decompose existing commodity kernels, Deker develops patterns of decomposition: a set of techniques, principles, and tools enabling decomposition of a fully-featured operating system kernel in a practical manner. Further, Deker develops a custom verification framework that builds on top of Deker’s decomposed environment. As the main glue connecting decomposition and verification efforts, a rigorous interface definition language (IDL) is proposed for specifying protocols that govern decomposed subsystems. Explicit protocol specification is enabling easier verification and maintenance, while the accompanying IDL compiler subsequently facilitates automatic generation of the glue code enabling transparent function invocation and object synchronization across share-nothing decomposed subsystems. While decomposing the kernel and providing complete isolation of subsystems, Deker remains practical: retains source-level compatibility with the non-decomposed kernel, enables incremental adoption, and remains fast.
maline is a tool for Android malware detection. It automatically learns to discriminate malicious from benign Android apps based on a dynamic analysis of a large number of existing apps. Once the analysis is done, maline can determine for a new app whether it is malware or not. The tool employs machine learning and a simple, yet effective, model of dependencies between low-level system calls an Android app executes.
STORM is a tool for detection of concurrency errors in system software written in C. More information and source code are available on STORM’s webpage.
During my ﬁrst internship at Microsoft Research back in 2006, I was involved in creating the foundations of HAVOC. HAVOC is a veriﬁer for C programs built on top of Microsoft’s Visual C compiler (cl.exe), and therefore is targeting Windows programs. It transforms a C program into a BoogiePL program, which is the input of the well-known Boogie veriﬁcation-condition (VC) generator. Generated VCs are handed over to the Z3 theorem prover. Based on the VC’s validity, the veriﬁcation either succeeds or the tool returns an error trace.
STRACLOS is a fast decision procedure for our Simple TRAnsitive CLOSure logic. The logic is suitable for reasoning about linked data structures, and contains convenient constructs for expressing unbounded reachability in such structures. Therefore, it can be used for verification of heap-manipulating programs that operate on linked lists. We successfully used STRACLOS to verify a number of heap-manipulating programs using predicate abstraction. Source code and Linux binary distribution are available for download:
STRACLOS has also been integrated into an available SMT solver MathSAT (big thanks to Roberto Bruttomesso and Alessandro Cimatti for helping out!). The version of MathSAT extended with STRACLOS (i.e. the theory of unbounded reachability) can be downloaded from the MathSAT homepage. Here are benchmarks from this work:
STRACLOS is joint work with Jesse Bingham.