Michael Emmi

Michael Emmi, Constantin Enea

Multithreaded software is typically built with specialized concurrent objects like atomic integers, queues, and maps. These objects' methods are designed to behave according to certain consistency criteria like atomicity, despite being optimized to avoid blocking and exploit parallelism, e.g., by using atomic machine instructions like compare and exchange (cmpxchg). Exposing atomicity violations is important since they generally lead to elusive bugs that are difficult to identify, reproduce, and ultimately repair. In this work we expose atomicity violations in concurrent object implementations from the most widely-used software development kit: The Java Development Kit (JDK). We witness atomicity violations via simple test harnesses containing few concurrent method invocations. While stress testing is effective at exposing violations given catalytic test harnesses and lightweight means of falsifying atomicity, divining effectual catalysts can be difficult, and atomicity checks are generally cumbersome. We overcome these problems by automating test-harness search, and establishing atomicity via membership in precomputed sets of acceptable return-value outcomes. Our approach enables testing millions of executions of each harness each second (per processor core). This scale is important since atomicity violations are observed in very few executions (tens to hundreds out of millions) of very few harnesses (one out of hundreds to thousands). Our implementation is open source and publicly available.

Shaobo He, Michael Emmi, Gabriela Ciocarlie

Testing-based methodologies like fuzzing are able to analyze complex software which is not amenable to traditional formal approaches like verification, model checking, and abstract interpretation. Despite enormous success at exposing countless security vulnerabilities in many popular software projects, applications of testing-based approaches have mainly targeted checking traditional safety properties like memory safety. While unquestionably important, this class of properties does not precisely characterize other important security aspects such as information leakage, e.g., through side channels. In this work we extend testing-based software analysis methodologies to two-safety properties, which enables the precise discovery of information leaks in complex software. In particular, we present the ct-fuzz tool, which lends coverage-guided greybox fuzzers the ability to detect two-safety property violations. Our approach is capable of exposing violations to any two-safety property expressed as equality between two program traces. Empirically, we demonstrate that ct-fuzz swiftly reveals timing leaks in popular cryptographic implementations.