Abstract Sound static analyses are an important ingredient for compiler optimizations and program verification tools. However, mathematically proving that a static analysis is sound is a difficult task due to two problems. First, soundness proofs relate two complicated program semantics (the static and the dynamic semantics) which are hard to reason about. Second, the more the static and dynamic semantics differ, the more work a soundness proof needs to do to bridge the impedance mismatch. These problems increase the effort and complexity of soundness proofs. Existing soundness theories address these problems by deriving both the dynamic and static semantics from the same artifact, often called generic interpreter. A generic interpreter provides a common structure along which a soundness proof can be composed, which avoids having to reason about the analysis as a whole. However, a generic interpreter restricts which analyses can be derived, as all derived analyses must roughly follow the program execution order. To lift this restriction, we develop a soundness theory for the blackboard analysis architecture, which is capable of describing backward, demand-driven, and summary-based analyses. The architecture describes static analyses with small independent modules, which communicate via a central store. Soundness of a compound analysis follows from soundness of all of its modules. Furthermore, modules can be proven sound independently, even though modules depend on each other. We evaluate our theory by proving soundness of four analyses: a pointer and call-graph analysis, a reflection analysis, an immutability analysis, and a demand-driven reaching definitions analysis.

Static call graphs are a fundamental building block of program analysis. However, differences in call-graph construction and the use of specific language features can yield unsoundness and imprecision. Call-graph analyses are evaluated using measures of precision and recall, but this is hard when a ground truth for real-world programs is generally unobtainable. In this work, we propose to use carefully constructed dynamic baselines based on fixed entry points and input corpora. The creation of this dynamic baseline is posed as an approximation of the ground truth---an optimization problem. We use manual extension and coverage-guided fuzzing for creating suitable input corpora. With these dynamic baselines, we study call-graph quality of multiple algorithms and implementations using four real-world Java programs. We find that our methodology provides valuable insights into call-graph quality and how to measure it. With this work, we provide a novel methodology to advance the field of static program analysis as we assess the computation of one of its core data structures---the call graph.

Traditional call-graph construction algorithms conflate the computation of possible runtime types with the actual resolution of (virtual) calls. This tangled design impedes supporting complex language features and APIs and making systematic trade-offs between precision, soundness, and scalability. It also impedes implementation of precise downstream analyses that rely on type information. To address the problem, we propose Unimocg, a modular architecture for call-graph construction that decouples the computation of type information from resolving calls. Due to its modular design, Unimocg can combine a wide range of different call-graph algorithms with algorithm-agnostic modules to support individual language features. Moreover, these modules operate at the same precision as the chosen call-graph algorithm with no further effort. Additionally, Unimocg allows other analyses to easily reuse type information from the call-graph construction at full precision. We demonstrate how Unimocg enables a framework of call-graph algorithms with different precision, soundness, and scalability trade-offs from reusable modules. Unimocg currently supports ten call-graph algorithms from vastly different families, such as CHA, RTA, XTA, and k-l-CFA. These algorithms show consistent soundness without sacrificing precision or performance. We also show how an immutability analysis is improved using Unimocg.

Modern software is often implemented in multiple interacting programming languages. When performing static analysis of such software, it is desirable to reuse existing single-language analyses to allow access to the results of decades of implementation effort.

The usage of WebAssembly (Wasm) is not only increasing in the web browser, but also as a backend technology on servers. Since Wasm introduces several security issues, like the possibility to obfuscate malicious code and cryptomining, an adequate analysis framework is needed for creating analyses that reveal such issues. Existing state-of-the-art analysis approaches lack in soundness, in fully providing essential information to client analyses, or entail a considerable amount of overhead due to their dynamic nature. To meet this challenge, we developed WasmA a static analysis framework for WebAssembly that determines necessary information needed by static client analyses, like call, control-, and data-flow graphs. In the evaluation we show that WasmA is performant, generic and extensible and thus competitive in comparison to state-of-the art tools. The implementation of a cryptominer detection tool on top of WasmA shows its applicability. WasmA is able to provide the required functionality while having a comparative resource-efficient approach, and as a result WasmA outperforms the state of the art.

Reasoning about immutability is important for pre-venting bugs, e.g., in multi-threaded software. So far, static analysis to infer immutability properties has mostly focused on individual objects and references. Reasoning about fields and entire classes, while significantly simpler, has gained less attention. Even a consistently used terminology is missing, which makes it difficult to implement analyses that rely on immutability information. We propose a model for class and field immutability that unifies terminology for immutability flavors considered by previous work and covers new levels of immutability to handle lazy initialization and immutability dependent on generic type parameters. Using the OPAL static analysis framework, we implement CiFi, a set of modular, collaborating analyses for different flavors of immutability, inferring the properties defined in our model. Additionally, we propose a benchmark of representative test cases for class and field immutability. We use the benchmark to showcase CiFi’s precision and recall in comparison to state of the art and use CiFi to study the prevalence of immutability in real-world libraries, showcasing the practical quality and relevance of our model.

Autonomous driving poses unique challenges for vehicle environment perception due to the complex driving environment where the autonomous vehicle interacts with surrounding traffic participants. Due to the limited capability of any sensor perception system, it is highly desirable that an autonomous driving vehicle could use not only information from onboard sensors (say, radar/camera/lidar) but also from remote (network) information via inter-vehicle communication systems. The collaborative information from cooperative/non-cooperative remote vehicles (along with the onboard sensor data) could substantially improve the vehicle decision making process and push autonomous driving to be safer and more reliable. Inter-vehicle communication technologies are at the stage of development for market introduction, after years of research and standardization. In this paper, we setup a dedicated short range communication (DSRC) system to provide a low-latency inter-vehicle wireless communication channel. The task is to build a record linkage between the onboard sensor data and the corresponding DSRC-transmitted remote vehicle information when both sets belong to the same object, for the purpose of enhancing host vehicle environment perceiving capability and reliability. This is a typical data association problem. The challenges mainly lie in the inherent uncertain nature of the observation data and the practical issues that information often suffers from delays and drops. We propose a track-based association approach using an interacting multiple model estimator with a sequential multiple hypothesis test (denoted as IMM-SMHT) as an ubiquitous solution to handle different situations in complicated driving scenarios. To fully exploit the potential of such a system, only position information (from the DSRC channel and onboard radar system) is used for the object matching purpose-we try to use the least amount of information to achieve a high association accuracy; additional information can be used but not currently considered. We aim to provide a real world solution, and therefore, a prototype vehicle system is built with practical consideration on market availability, cost, and sensor limitations. We design meaningful use cases for creating functionality modules from a systematic point of view. The inter-vehicle information fusion system based on the track fusion approach using the IMM-SMHT is tested in real traffic on the U.S. roads and shows promising object matching performance of significant practical feasibility.

Dedicated Short Range Communication (DSRC) systems will become ubiquitous among vehicles in the near future. Because this technology enables communication between any set of DSRC-equipped vehicles, precise knowledge of these other vehicles is available to the host car. In addition to the DSRC system, onboard radars are able to provide high fidelity dynamics measurements of other objects within the sensing range. Given these two methods of measurement, environmental perception for driver assistance systems can be greatly improved, especially if the measurements are fused together. However, this is not a trivial task because of an inherent data association problem: Given the objects detected by the radar sensor, which one is truly the DSRC message sender? In this paper, we propose a system architecture to fuse DSRC and radar data. This architecture uses a reliable statistical track-to-track association algorithm in a novel way to solve this data matching problem. We present experimental results of this architecture on a system running in real traffic situations in the U. S.