We present a new approach to static analysis for security vetting of Android apps and a general framework called Amandroid. Amandroid determines points-to information for all objects in an Android app component in a flow and context-sensitive (user-configurable) way and performs data flow and data dependence analysis for the component. Amandroid also tracks inter-component communication activities. It can stitch the component-level information into the app-level information to perform intra-app or inter-app analysis. In this article, (a) we show that the aforementioned type of comprehensive app analysis is completely feasible in terms of computing resources with modern hardware, (b) we demonstrate that one can easily leverage the results from this general analysis to build various types of specialized security analyses—in many cases the amount of additional coding needed is around 100 lines of code, and (c) the result of those specialized analyses leveraging Amandroid is at least on par and often exceeds prior works designed for the specific problems, which we demonstrate by comparing Amandroid’s results with those of prior works whenever we can obtain the executable of those tools. Since Amandroid’s analysis directly handles inter-component control and data flows, it can be used to address security problems that result from interactions among multiple components from either the same or different apps. Amandroid’s analysis is sound in that it can provide assurance of the absence of the specified security problems in an app with well-specified and reasonable assumptions on Android runtime system and its library.

We propose a new approach to conduct static analysis for security vetting of Android apps, and built a general framework, called Amandroid for determining points-to information for all objects in an Android app in a flow- and context-sensitive way across Android apps components. We show that: (a) this type of comprehensive analysis is completely feasible in terms of computing resources needed with modern hardware, (b) one can easily leverage the results from this general analysis to build various types of specialized security analyses -- in many cases the amount of additional coding needed is around 100 lines of code, and (c) the result of those specialized analyses leveraging Amandroid is at least on par and often exceeds prior works designed for the specific problems, which we demonstrate by comparing Amandroid's results with those of prior works whenever we can obtain the executable of those tools. Since Amandroid's analysis directly handles inter-component control and data flows, it can be used to address security problems that result from interactions among multiple components from either the same or different apps. Amandroid's analysis is sound in that it can provide assurance of the absence of the specified security problems in an app with well-specified and reasonable assumptions on Android runtime system and its library.

Previous applications of symbolic execution (Sym-Exe) have focused on bug-finding and test-case generation. However, SymExe has the potential to significantly improve usability and automation when applied to verification of software contracts in safety-critical systems. Due to the lack of support for processing software contracts and ad hoc approaches for introducing a variety of over/under-approximations and optimizations, most SymExe implementations cannot precisely characterize the verification status of contracts. Moreover, these tools do not provide explicit justifications for their conclusions, and thus they are not aligned with trends toward evidence-based verification and certification. We introduce the concept of explicating symbolic execution (xSymExe) that builds on a strong semantic foundation, supports full verification of rich software contracts, explicitly tracks where over/under-approximations are introduced or avoided, precisely characterizes the verification status of each contractual claim, and associates each claim with explications for its reported verification status. We report on case studies in the use of Bakar Kiasan, our open source xSymExe tool for Spark Ada.

This tool paper describes the design and implementation of an interactive environment for discovering and browsing information flow in SPARK programs. SPARK is a subset of Ada that has been used in a number of industrial contexts for implementing certified safety and security critical systems. SPARK requires explicit specification of information flow properties in the form of procedure contracts. To write such contracts, developers need to understand the data and control dependencies in the program. Our tool Bakar Alir, implemented as an Eclipse Plug-in, utilizes classic slicing and chopping techniques to assist developers in writing information flow contracts.

As a Behavioral Interface Specification Language (BISL) for Java, the Java Modeling Language (JML) is tightly coupled to the base language it enhances. Up until Java 1.4, JML kept apace with the evolution of its base language. Java 5 and subsequent revisions have yet to be fully supported by JML tools. Recent efforts such as JML4 have been addressing this issue by providing an Eclipse-based tooling infrastructure. In its current form, JML4 has a fairly steep learning curve for developers wishing to contribute to or extend it. To address this issue and bring JML tools one step closer to a desired plug-in model, we propose a JML Intermediate Representation (JIR) and supporting software infrastructure for JML front-ends and back-ends.

Automated theorem proving techniques such as Satisfiability Modulo Theory (SMT) solvers have seen significant advances in the past several years. These advancements, coupled with vast hardware improvements, have drastic impact on, for example, program verification techniques and tools. The general availability of robust general purpose solvers have reduced a significant engineering overhead when designing and developing program verifiers. However, most solver implementations are designed to be used as a black box, and due to their aim as general purpose solvers, they often miss optimization opportunities that can be done by leveraging domain-specific knowledge.

Recent work has demonstrated that symbolic execution techniques can serve as a basis for formal analysis capable of automatically checking heap-manipulating software components against strong interface specifications. In this paper, we present an enhancement to existing symbolic execution algorithms for object-oriented programs that significantly improves upon the algorithms currently implemented in Bogor/Kiasan and JPF. To motivate and justify the new strategy for handling heap data in our enhanced approach, we present a significant empirical study of the performance of related algorithms and an interesting case counting analysis of the heap shapes that can appear in several widely used Java data structure packages.

Best program practices in software engineering emphasize software components that are loosely coupled and can be independently developed by different vendors. While these approaches improve the process of software development, however, they present a number of challenges involving reasoning about the correctness of individual components as well as their integration. Design-by-contract reasoning offers a promising approach to reason about software components by requiring software contracts that describe the behaviors of the components. This allows one to focus at satisfying the contract of each component, i.e., it allows compositional reasoning. In this paper, we present Kiasan, a technique that combines symbolic execution, model checking, theorem proving, and constraint solving to support design-by-contract reasoning of object-oriented software. There are a number of interesting tradeoffs between Kiasan other approaches such as ESC/Java. While checking in Kiasan is sometime more expensive, Kiasan can check much stronger behavioral properties of object-oriented software including properties/software that makes extensive use of heap-allocated data. In addition, Kiasan naturally generates counter examples, visualization of code effects, and JUnit test cases that are driven by code and user-supplied specifications. We present Kiasan and describe how it is implemented on top of the Bogor framework. Furthermore, we present a case study in which Kiasan is applied to a variety of examples and we discuss insights gained from our experience.

This paper presents Kiasan, a bounded technique to reason about open systems based on a path sensitive, relatively sound and complete symbolic execution instead of the usual compositional reasoning through weakest precondition calculation that summarizes all execution paths. Kiasan is able to check strong heap properties, and it is fully automatic and flexible in terms of its cost and the guarantees it provides. It allows a user-adjustable mixed compositional/non-compositional reasoning and naturally produces error traces as fault evidence. We implemented Kiasan using the Bogor model checking framework and observed that its performance is comparable to ESC/Java on similar scales of problems and behavioral coverage, while providing the ability to check much stronger specifications

Model checking has proven to be an effective technology for verification and debugging in hardware and more recently in software domains. We believe that recent trends in both the requirements for software systems and the processes by which systems are developed suggest that domain-specific model checking engines may be more effective than general purpose model checking tools. To overcome limitations of existing tools which tend to be monolithic and non-extensible, we have developed an extensible and customizable model checking framework called Bogor. In this tutorial, we give an overview of (a) Bogor's direct support for modeling object-oriented designs and implementations, (b) its facilities for extending and customizing its modeling language and algorithms to create domain-specific model checking engines, and (c) pedagogical materials that we have developed to describe the construction of model checking tools built on top of the Bogor infrastructure

The use of component models such as Enterprise Java Beans and the CORBA Component Model (CCM) in application development is expanding rapidly. Even in real-time safety-critical and mission-critical domains, component-based development is beginning to take hold as a mechanism for in-corporating non-functional aspects such as real-time, quality-of-service, and distribution.

Model checking is emerging as a popular technology for reasoning about behavioral properties of a wide variety of software artifacts including: requirements models, architectural descriptions, designs, implementations, and process models. The complexity of model checking is well-known, yet cost-effective analyses have been achieved by exploiting, for example, naturally occurring abstractions and semantic properties of a target software artifact. semantic properties of target software artifacts. Adapting a model checking tool to exploit this kind of domain knowledge often requires in-depth knowledge of the tool's implementation.We believe that with appropriate tool support, domain experts will be able to develop efficient model checking-based analyses for a variety of software-related models. To explore this hypothesis, we have developed Bogor, a model checking framework with an extensible input language for defining domain-specific constructs and a modular interface design to ease the optimization of domain-specific state-space encodings, reductions and search algorithms. We present the pattern-oriented design of Bogor and discuss our experiences adapting it to efficiently model check Java programs and event-driven component-based designs.

Numerous researchers have reported success in reasoning about properties of small programs using finite-state verification techniques. We believe, as do most researchers in this area, that in order to scale those initial successes to realistic programs, aggressive abstraction of program data will be necessary. Furthermore, we believe that to make abstraction-based verification usable by non-experts significant tool support will be required. In this paper we describe how several different program analysis and transformation techniques are integrated into the Bandera toolset to provide facilities for abstracting Java programs to produce compact, finite-state models that are amenable to verification for example via model checking. We illustrate the application of Bandera's abstraction facilities to analyze a realistic multi-threaded Java program.

Finite-state verification techniques, such as model checking, have shown promise as a cost-effective means for finding defects in hardware designs. To date, the application of these techniques to software has been hindered by several obstacles. Chief among these is the problem of constructing a finite-state model that approximates the executable behavior of the software system of interest. Current best-practice involves hand-construction of models which is expensive (prohibitive for all but the smallest systems), prone to errors (which can result in misleading verification results), and difficult to optimize (which is necessary to combat the exponential complexity of verification algorithms).

Despite emerging tool support for assertion-checking and testing of object-oriented programs, providing convincing evidence of program correctness remains a difficult challenge. This is especially true for multi-threaded programs. Techniques for reasoning about finite-state systems have been developing rapidly over the past decade and have the potential to form the basis of powerful software validation theologies.We have developed the Bandera toolset [1] to harness the power of existing model checking tools to apply them to reason about correctness requirements of Java programs. Bandera provides tool support for defining and managing collections of requirements for a program, for extracting compact finite-state models of the program to enable tractable analysis, and for displaying analysis results to the user through a debugger-like interface. This paper describes and illustrates the use of Bandera's source-level user interface for model checking Java programs.