This paper presents a static mutability analysis approach relying on escape information for Java components and uses the techniques to detect the security threats to data integrity before software components are deployed. In order to increase the precision of our analysis, we make a couple of significant modifications to mutability definitions based on previous work in the context of components. We extended our security analysis tool SecDetector with proposed mutability analysis, and used it to find potential threats to data integrity in Java components and lead developers to fix the security flaws. On the benchmarks in our experimental evaluation, we show that our tool can correctly find potential modification access violations with few false positives and provide evidence of the effectiveness of our techniques. While the analysis techniques are in the context of Java code, the basic concepts are applicable to other object-oriented programming languages as well.

This paper presents an extension of escape analysis for static detection of threats to data confidentiality in Java components, called field escape analysis. We augment existing escape analyses, which are typically based on points-to analysis for reference (or pointer) type, with data and control dependence analyses with respect to primitive type. To meet the demand of security analysis, we propose a graph representation, called primitive value dependence graph (PVDG), and a novel semantics for dependence analysis. We have built a static analysis tool for Java components called SecDetector. In the experimental evaluation, using different combinations of underlying analysis techniques (e.g., points-to analysis, dependence analysis), we evaluated trades-offs between precision and performance on five publicly-available J2EE applications. On the benchmarks examined, there are few false positives in our study. It provides evidence of the usefulness of our approach.

Modern enterprise systems support Role-Based Access Control (RBAC). Although RBAC allows restricting access to privileged operations, a deployer may actually intend to restrict access to privileged data. This paper presents a theoretical foundation for correlating an operation-based RBAC policy with a data-based RBAC policy. Relying on a location consistency property, this paper shows how to infer whether an operation-based RBAC policy is equivalent to any databased RBAC policy. We have built a static analysis tool for Java Platform, Enterprise Edition (Java EE) called Static Analysis for Validation of Enterprise Security (SAVES). Relying on interprocedural pointer analysis and dataflow analysis, SAVES analyzes Java EE bytecode to determine if the associated RBAC policy is location consistent, and reports potential security flaws where location consistency does not hold. The experimental results obtained by using SAVES on a number of production-level Java EE codes have identified several security flaws with no false positive reports.

This article describes FLAVERS, a finite-state verification approach that analyzes whether concurrent systems satisfy user-defined, behavioral properties. FLAVERS automatically creates a compact, event-based model of the system that supports efficient dataflow analysis. FLAVERS achieves this efficiency at the cost of precision. Analysts, however, can improve the precision of analysis results by selectively and judiciously incorporating additional semantic information into an analysis.We report on an empirical study of the performance of the FLAVERS/Ada toolset applied to a collection of multitasking Ada systems. This study indicates that sufficient precision for proving system properties can usually be achieved and that the cost for such analysis typically grows as a low-order polynomial in the size of the system.

Protection of digital data from unauthorized access is of paramount importance. In the past several years, much research has concentrated on protecting data from the standpoint of confidentiality, integrity and availability. Software is a form of data with unique properties and its protection poses unique challenges. First, software can be reverse engineered, which may result in stolen intellectual property. Second, software can be altered with the intent of performing operations this software must not be allowed to perform.With commercial software increasingly distributed in forms from which source code can be easily extracted, such as Java bytecodes, reverse engineering has become easier than ever. Obfuscation techniques have been proposed to impede illegal reverse engineers. Obfuscations are program transformations that preserve the program functionality while obscuring the code, thereby protecting the program against reverse engineering. Unfortunately, the existing obfuscation techniques are limited to obscuring variable names, transformations of local control flow, and obscuring expressions using variables of primitive types. In this paper, we propose obfuscations of design of object-oriented programs.We describe three techniques for obfuscation of program design. The class coalescing obfuscation replaces several classes with a single class. The class splitting obfuscation replaces a single class with multiple classes, each responsible for a part of the functionality of the original class. The type hiding obfuscation uses the mechanism of interfaces in Java to obscure the types of objects manipulated by the program. We show the results of our initial experiments with a prototype implementation of these techniques. In particular, we shown that the runtime overheads of these obfuscations tend to be small.

Open distributed systems are becoming increasingly popular. Such systems include components that may be obtained from a number of different sources. For example, Java allows run-time loading of software components residing on remote machines. One unfortunate side-effect of this openness is the possibility that "hostile" software components may compromise the security of both the program and the system on which it runs. Java offers a built-in security mechanism, using which programmers can give permissions to distributed components and check these permissions at run-time. This security model is flexible, but using it is not straightforward, which may lead to insufficiently tight permission checking and therefore breaches of security.In this paper, we propose a data flow algorithm for automated analysis of the flow of permissions in Java programs. Our algorithm produces, for a given instruction in the program, a set of permissions that are checked on all possible executions up to this instruction. This information can be used in program understanding tools or directly for checking properties that assert what permissions must always be checked before access to certain functionality is allowed. The worst-case complexity of our algorithm is low-order polynomial in the number of program statements and permission types, while comparable previous approaches have exponential costs.

Data flow analysis is used widely in program compilation, understanding, design, and analysis tools. In data flow analysis, problem-specific information is associated with nodes and/or edges in the flow graph representation of a program or component and re-comp\-uted iteratively. A popular data flow analysis design relies on a worklist that stores all nodes and edges whose data flow information has to be re-computed. While this approach is straightforward, it has some drawbacks. First, the presence of the worklist makes data flow algorithms centralized, which may reduce effectiveness of parallel implementations of these algorithms. Second, the worklist approach is difficult to implement in a way that minimizes the amount of information passed between flow graph nodes.In this paper, we propose to use the well-known Observer pattern for implementation of data flow analyses. We argue that such implementations are more object-oriented in nature, as well as less centralized, than worklist-based ones. We argue that by adopting this Observer-based view, data flow analyses that minimize the amount of information passed between flow graph nodes can be implemented easier than by using the worklist view. We present experimental data indicating that for some types of data flow problems, even single-threaded implementations of Observer-based data flow analysis have better run times than comparable worklist-based implementations.

Traditionally, verification properties have been classified as safety or liveness properties. While this taxonomy has an attractive simplicity and is useful for identifying the appropriate analysis algorithm for checking a property, determining whether a property is safety, liveness, or neither can require significant mathematical insight on the part of the analyst. In this paper, we present an alternative property taxonomy. We argue that this taxonomy is a more natural classification of the kinds of questions that analysts want to ask. Moreover, most classes in our taxonomy have a known, direct mapping to the safety-liveness classification, and thus the appropriate analysis algorithm can be automatically determined.

In this paper we show how the FLAVERS data flow analysis technique, originally formulated for programs with the rendezvous model of concurrency, can be applied to concurrent Java programs. The general approach of FLAVERS is based on modeling a concurrent program as a flow graph and using a data flow analysis algorithm over this graph to check statically if a property holds on all executions of the program. The accuracy of this analysis can be improved by supplying additional information, represented as finite state automata, to the data flow analysis algorithm. In this paper we present a straightforward approach for modeling Java programs that uses the accuracy improving mechanism to represent the possible communications among threads in Java programs, instead of representing them directly in the flow graph model. We also discuss a number of error-prone thread communication patterns that can arise in Java and describe how FLAVERS can be used to check for the presence of these.

Partial order optimization techniques for distributed systems improve the performance of finite state verification approaches by avoiding redundant exploration of some portions of the state space. Previously, such techniques have been applied in the context of model checking approaches. In this paper we propose a partial order optimization of the program model used by FLAVERS, a data flow based finite state verification approach for checking user-specified properties of distributed software. We demonstrate experimentally that this optimization often leads to significant reductions in the run time of the analysis algorithm of FLAVERS. On average, for those cases where this optimization could be applied, we observed a speedup of 21%. For one of the cases, the optimization resulted in an analysis speedup of 91%.

FLAVERS, a tool for verifying properties of concurrent systems, uses composite data flow analysis to incrementally improve the precision of the results of its verifications. Although FLAVERS is one of the few static analysis techniques for concurrent systems that has the potential to handle large scale systems, it sometimes can still be very expensive to use. In this paper we experimentally compare the cost of two versions of this approach for solving composite data flow analysis problems. The first version, product-based, uses the more straightforward approach, and the second, tuple-based, is built around the idea of reducing analysis space requirements at the expense of analysis time. We demonstrate experimentally, by analyzing properties of actual concurrent programs, that the tuple-based version is comparable in time to the product-based version but for large composite data flow problems it requires several orders of magnitude less space.

Information about which pairs of statements in a concurrent program can execute in parallel is important for optimizing and debugging programs, for detecting anomalies, and for improving the accuracy of data flow analysis. In this paper, we describe a new data flow algorithm that finds a conservative approximation of the set of all such pairs. We have carried out an initial comparison of the precision of our algorithm and that of the most precise of the earlier approaches, Masticola and Ryder's non-concurrency analysis [8], using a sample of 159 concurrent Ada programs that includes the collection assembled by Masticola and Ryder. For these examples, our algorithm was almost always more precise than non-concurrency analysis, in the sense that the set of pairs identified by our algorithm as possibly happening in parallel is a proper subset of the set identified by non-concurrency analysis. In 132 cases, we were able to use reachability analysis to determine exactly the set of pairs of statements that may happen in parallel. For these cases, there were a total of only 10 pairs identified by our algorithm that cannot actually happen in parallel.

In this demonstration we give a scenario of how FLAVERS, an implementation of the incremental accuracy improving data flow analysis approach [I], is used to verify event sequence properties of concurrent or distributed software programs.

In this paper we demonstrate the effectiveness of data flow analysis for verifying requirements of communication protocols. Data flow analysis is a static analysis method for increasing confidence in the correctness of software systems by automatically verifying that a given software artifact (e.g., design or code) must behave consistently with a specified requirement. In this case study, we apply the FLAVERS data flow analysis tool to pseudocode designs of the three way handshake connection establishment protocol and of the alternating bit protocol and prove that the behavior of the pseudocode is consistent with protocol behavioral requirement specifications. We show how FLAVERS is a particularly effective because it is computationally inexpensive, requires minimal human interaction, and is a general approach that can be applied incrementally until the desired accuracy is achieved. In addition, we show how assumptions about the environment in which a software system is executed can be incorporated into the analysis, using message losses as an example. We present experimental results and derive some guidelines about the classes of protocol requirement specifications that may be amenable to verification using FLAVERS.