A survey of static analysis methods for identifying security vulnerabilities in software systems <s> 61 <s> Semantic analysis of programs is essential in optimizingcompilers and program verification systems. It encompasses dataflow analysis, data type determination, generation of approximateinvariant assertions, etc. Several recent papers (among others Cousot & Cousot[77a],Graham & Wegman[76], Kam & Ullman[76], Kildall[73],Rosen[78], Tarjan[76], Wegbreit[75]) have introduced abstractapproaches to program analysis which are tantamount to the use of aprogram analysis framework (A,t,a) where A is alattice of (approximate) assertions, t is an (approximate)predicate transformer and a is an often implicit functionspecifying the meaning of the elements of A. This paper is devotedto the systematic and correct design of program analysis frameworkswith respect to a formal semantics. Preliminary definitions are given in Section 2 concerning themerge over all paths and (least) fixpoint program-wide analysismethods. In Section 3 we briefly define the (forward and backward)deductive semantics of programs which is later used as a formalbasis in order to prove the correctness of the approximate programanalysis frameworks. Section 4 very shortly recall the mainelements of the lattice theoretic approach to approximate semanticanalysis of programs. The design of a space of approximate assertions A is studied inSection 5. We first justify the very reasonable assumption that Amust be chosen such that the exact invariant assertions of anyprogram must have an upper approximation in A and that theapproximate analysis of any program must be performed using adeterministic process. These assumptions are shown to imply that Ais a Moore family, that the approximation operator (wich definesthe least upper approximation of any assertion) is an upper closureoperator and that A is necessarily a complete lattice. We next showthat the connection between a space of approximate assertions and acomputer representation is naturally made using a pair of isotoneadjoined functions. This type of connection between two completelattices is related to Galois connections thus making availableclassical mathematical results. Additional results are proved, theyhold when no two approximate assertions have the same meaning. In Section 6 we study and examplify various methods which can beused in order to define a space of approximate assertions orequivalently an approximation function. They include thecharacterization of the least Moore family containing an arbitraryset of assertions, the construction of the least closure operatorgreater than or equal to an arbitrary approximation function, thedefinition of closure operators by composition, the definition of aspace of approximate assertions by means of a complete joincongruence relation or by means of a family of principalideals. Section 7 is dedicated to the design of the approximatepredicate transformer induced by a space of approximate assertions.First we look for a reasonable definition of the correctness ofapproximate predicate transformers and show that a localcorrectness condition can be given which has to be verified forevery type of elementary statement. This local correctnesscondition ensures that the (merge over all paths or fixpoint)global analysis of any program is correct. Since isotony is notrequired for approximate predicate transformers to be correct it isshown that non-isotone program analysis frameworks are manageablealthough it is later argued that the isotony hypothesis is natural.We next show that among all possible approximate predicatetransformers which can be used with a given space of approximateassertions there exists a best one which provides the maximuminformation relative to a program-wide analysis method. The bestapproximate predicate transformer induced by a space of approximateassertions turns out to be isotone. Some interesting consequencesof the existence of a best predicate transformer are examined. Oneis that we have in hand a formal specification of the programswhich have to be written in order to implement a program analysisframework once a representation of the space of approximateassertions has been chosen. Examples are given, including oneswhere the semantics of programs is formalized using Hoare[78]'ssets of traces. In Section 8 we show that a hierarchy of approximate analysescan be defined according to the fineness of the approximationsspecified by a program analysis framework. Some elements of thehierarchy are shortly exhibited and related to the relevantliterature. In Section 9 we consider global program analysis methods. Thedistinction between "distributive" and "non-distributive" programanalysis frameworks is studied. It is shown that when the bestapproximate predicate transformer is considered the coincidence ornot of the merge over all paths and least fixpoint global analysesof programs is a consequence of the choice of the space ofapproximate assertions. It is shown that the space of approximateassertions can always be refined so that the merge over all pathsanalysis of a program can be defined by means of a least fixpointof isotone equations. Section 10 is devoted to the combination of program analysisframeworks. We study and examplify how to perform the "sum","product" and "power" of program analysis frameworks. It is shownthat combined analyses lead to more accurate information than theconjunction of the corresponding separate analyses but this canonly be achieved by a new design of the approximate predicatetransformer induced by the combined program analysisframeworks. <s> BIB001 </s> A survey of static analysis methods for identifying security vulnerabilities in software systems <s> 61 <s> Shape analysis concerns the problem of determining "shape invariants" for programs that perform destructive updating on dynamically allocated storage. This article presents a parametric framework for shape analysis that can be instantiated in different ways to create different shape-analysis algorithms that provide varying degrees of efficiency and precision. A key innovation of the work is that the stores that can possibly arise during execution are represented (conservatively) using 3-valued logical structures. The framework is instantiated in different ways by varying the predicates used in the 3-valued logic. The class of programs to which a given instantiation of the framework can be applied is not limited a priori (i.e., as in some work on shape analysis, to programs that manipulate only lists, trees, DAGS, etc.); each instantiation of the framework can be applied to any program, but may produce imprecise results (albeit conservative ones) due to the set of predicates employed. <s> BIB002 </s> A survey of static analysis methods for identifying security vulnerabilities in software systems <s> 61 <s> While a typical software component has a clearly specified (static) interface in terms of the methods and the input/output types they support, information about the correct sequencing of method calls the client must invoke is usually undocumented. In this paper, we propose a novel solution for automatically extracting such temporal specifications for Java classes. Given a Java class, and a safety property such as "the exception E should not be raised", the corresponding (dynamic) interface is the most general way of invoking the methods in the class so that the safety property is not violated. Our synthesis method first constructs a symbolic representation of the finite state-transition system obtained from the class using predicate abstraction. Constructing the interface then corresponds to solving a partial-information two-player game on this symbolic graph. We present a sound approach to solve this computationally-hard problem approximately using algorithms for learning finite automata and symbolic model checking for branching-time logics. We describe an implementation of the proposed techniques in the tool JIST--- Java Interface Synthesis Tool---and demonstrate that the tool can construct interfaces accurately and efficiently for sample Java2SDK library classes. <s> BIB003 </s> A survey of static analysis methods for identifying security vulnerabilities in software systems <s> 61 <s> This paper addresses the challenge of sound typestate verification, with acceptable precision, for real-world Java programs. We present a novel framework for verification of typestate properties, including several new techniques to precisely treat aliases without undue performance costs. In particular, we present a flowsensitive, context-sensitive, integrated verifier that utilizes a parametric abstract domain combining typestate and aliasing information.To scale to real programs without compromising precision, we present a staged verification system in which faster verifiers run as early stages which reduce the workload for later, more precise, stages.We have evaluated our framework on a number of real Java programs, checking correct API usage for various Java standard libraries. The results show that our approach scales to hundreds of thousands of lines of code, and verifies correctness for 93% of the potential points of failure. <s> BIB004
Typestate specifications can encode correct usage rules for many security-related libraries and interfaces.  BIB003 For example, Figure 9 presents a partial typestate specification of a Signature object. This partial specification represents a subset of the permitted behaviors for a Signature object (we omit some behaviors for simplicity present an inference algorithm for inferring restricted and confined pointers, which they use to enable strong updates. A state-of-the-art typestate-verifier algorithm This section presents an overview of a state-of-theart typestate verifier algorithm for Java. BIB004 The verification system is a composite verifier built out of several composable verifiers of increasing precision and cost. Each verifier can run independently, but the composite verifier stages analyses in order to improve efficiency without compromising precision. The early stages use the faster verifiers to reduce the workload for later, more precise stages, as shown in Figure 10 . The system is comprised of four stages: a flowinsensitive analysis, an intraprocedural analyzer, an inexpensive analysis based on uniqueness analysis, and an integrated verifier combining alias information and typestates. This subsection covers a short overview of an abstraction technique used by the integrated verifier, the last and most precise analysis stage. The integrated verifier performs flow-and context-sensitive verification with an abstraction that combines aliasing information with typestate information. The use of a combined domain is more precise than separately performing typestate checking and flow-sensitive alias analysis, as is common with abstract interpretation over combined domains. BIB001 The abstract domain captures information about the typestate of the given abstract object, as well as information regarding potential aliases of an abstract object. In this presentation, we represent an abstract program state as a set of tuples, where each tuple has the following elements: AO, a representation of an abstract object from the preliminary pointer analysis T, the typestate occupied by the abstract object Must, a set of symbolic access paths (for example, x.f.g) that must point to a particular object May, a bit indicating whether the Must set is incomplete; may there exist other access paths pointing to the abstract object, which do not appear in the Must set? MustNot, a set of symbolic access paths that must not point to a particular object Notice that this paper presents a simplified abstraction to illustrate the combined tracking of aliasing and typestate. The full verifier 76 also incorporates a uniqueness abstraction and several optimizations, not described here. By way of example, consider the code in Figure 11 . We wish to verify that the program uses Signature objects correctly according to the typestate specification of Figure 9 . The example includes one allocation site for Signature objects, the allocation at line 5, which we will denote by S. When processing this statement for the first time, the solver generates an abstract state representing an abstract object S in the INIT state, pointed-to by s. Immediately after line 5, there can be no other pointers to this object, so May is set to false, resulting in an abstract program state of fhS, INIT, fsg, false, Øig. Based on the typestate automaton, we see that statement 6 forces a typestate transition to the SIGN state. Because the abstract state includes Must points-to information for s, the effect of statement 6 can be precisely reflected by a strong update, resulting in an abstract state of fhS, SIGN, fsg, false, Øig. The next interesting operation occurs at statement 9, which stores the abstract object into a set. Because the abstraction has not been tracking this set, statement 9 induces new access paths which may point to the abstract object. The abstraction models this by setting May to true, as follows: fhS, SIGN, fsg, true, Øig. A key element of the integrated verifier's abstraction is the use of a focus operation, BIB002 which dynamically (during analysis) makes distinctions between objects that the underlying basic points-to analysis does not distinguish. In the example code, the key focus operation occurs at statement 14. When first propagating at statement 14, the solver propagates an abstract state that indicates an abstract object in the SIGN state, but does not indicate any useful Must pointer information: fhS, SIGN, Ø, true, Øig. Statement 14 causes a typestate transition to the VERIFY state. In order to apply strong updates downstream, the solver applies a focus operation to split the abstract state into two cases, each of which holds more precise pointer information. There are two possibilities for each concrete object at this program point: either s2 points to the object, or it does not. In the first case, statement 14 causes a transition to the VERIFY state, and s2 must point to the object; in the second case, statement 14 does not cause a typestate transition, and s2 must not point to the abstract object; therefore, after applying this focus logic to statement 14, the abstraction produces two tuples: fhS, VERIFY, fs2g, true, Øi, hS, SIGN, Ø, true, fs2gig. Downstream, when processing statement 16, the solver uses the alias information to avoid a spurious transition (false positive) to the ERROR state. In particular, the second tuple indicates that s2 must not point to the object manipulated by statement 16; thus, the call to verify will not occur on an object in the SIGN state. The solver thus iterates to a fixed point, updating the abstract state at each program point based on simple flow functions derived from the language semantics. Table 1 shows the final result of the fixed-point iteration at each program point in the example. The abstraction suffices to demonstrate that this example uses Signature objects correctly, although those objects flow through complex collection classes. More generally, this verifier can verify similar patterns that flow across procedures, using flow-