Research program
AIDA - Abstract Interpretation Design and Applications
University Co-ordinator
Università di PISA -
INFORMATICA - PISA(PI)
Research Unit Leader
Roberto BARBUTI
Description
The research activity in Pisa will be done according to the following workpackages.Workpackage WP1. Static analysis.Task PI1.1Static analysis of mobile calculi.We plan to use abstract interpretation to formally compare existing CFA and type systems of Mobile Ambients. We want to evaluate their precision and expressive power, and to compare the information, which is effectively computed by their algorithms. In particular, we are interested in their application for the verification of open systems, and therefore we will take into account their ability to model the behaviour with respect to the possible external contexts. Moreover, we will investigate a common approach in CFA, based on the idea of analysing the system in parallel with a process, called hardest attacker, which simulates some of the possible external contexts. It is particularly interesting to find out an hardest attacker representing all the well-typed contexts. In fact, this could be used to integrate the two techniques, by combining the compositionality of the type system, needed to handle the contexts, and the precision of the CFA. In the second year we will extend this approach to other properties, namely to other type systems, or to other calculi for mobility.Task PI1.2Static analysis of concurrent object oriented calculi.We want to use abstract interpretation techniques for proving properties of a concurrent object oriented calculus. Such properties can be used as a guide to the construction of tool for real object oriented languages with concurrent features (like Java). The research will start by defining the features which the calculus must include for capturing the relevant aspects of the real language. In a second phase, the concrete and abstract semantics will be defined together with the tools based on them. We are interested in studying the relations among such tools and the analogous ones based on type systems.Task PI1.3Static analysis of declarative languagesThe first step in any abstract interpretation-based analysis of logic languages is the choice of a suitable collecting semantics, starting from a non-collecting one. In the field of abstract interpretation of logic programs, there are essentially two different ways to build a collecting semantics: a goal-dependent and a goal-independent way. Since the goal-dependent semantics suffers from the loss of precision stated above, many abstract analysis are performed on the base of a goal-independent collecting semantics. However, while some abstract domains (those for anti-instance closed properties) do actually benefit from goal-independent semantics, the opposite holds for instance-closed properties, and nothing may be told for the general case. Some research has been done in trying to unify both semantic styles, obtaining a new semantics which just computes both the goal-dependent and the goal-independent semantics, improving each one with the result of the other. While this could be effective from the point of view of the precision of the analysis, it is not adequate from the computational point of view. Hence, we are looking for a new semantics which is built from the ground up to be more precise than goal-dependent and goal-independent semantics for all the abstract domains. The benefits of this research would be the availability of an unique semantics for all the kind of analysis over logic programs. We also think that it would lead to a deeper understanding of the way abstract domains are built, especially of the way in which they could be decomposed in a upward-closed and a downward-closed part. Once fixed the collecting semantics, we plan to study algorithms for abstract unification of both substitutions and constraints. In fact, despite the large amount of work recently devoted to this subject, most of the present abstract unification algorithms can be proved to be sub-optimal. This leads to a significant loss of precision in the overall analysis result. We plan to devise a general scheme from which we can derive abstract unification algorithms which are optimal, i.e. as precise as possible, with respect to the abstract domain of interest. In this context, we are particularly interested in abstract domains for aliasing and sharing analysis, whose goal is the automatic parallelization of (constraint) logic programs. We also think that abstract matching can be used in other field, like (abstract) term rewriting and semantics of functional languages, and that many results concerning optimality of abstract unification could be reused in these domains. In particular, we plan to study the relationships among various domains for interval analysis, from the point of view of the increased precision. We believe that many techniques from declarative languages concerning optimality and completeness of abstract operators, could be applied to interval analysis as well. This can reveal new domains with a better cost/performance trade-off. This research will be done in collaboration with the research unit in Bologna.Task PI1.4Abstract interpretation and type systems.We want to study the systematic derivation of an abstract domain for monomorphic type inference in lambda-calculus. The main goal of the task is the development of techniques for the systematic transformation of a type domain devised for type checking into a domain adequate to type inference. While the domain used in type checking is usually exactly the property we want to observe, a precise type inference requires a much more complex domain. The idea is to try the application of some of the refinement operators, which lead to more concrete (and more precise) domains. In particular, we will try to reconstruct the abstract domain used in the ML type inference algorithm, which consists of terms and constraints, as the transformation of the simple domain of monotypes with variables (represented as Herbrand terms). The reconstruction will use a suitable combination of domain refinement operators. Techniques which allow us to easily transform type checking rules into type inference rules are indeed very important in the static analysis of calculi oriented towards concurrency and mobility. In fact properties one might be interested in inferring (for example those related to security) are often specified by type checking rules. In the first year, we will develop the transformation, by deriving the abstract domain and the corresponding optimal abstract operations. In the second year, we will define the analyzer as an abstract interpreter, compare it to the ML type inference algorithm and provide a prototype implementation. We will also evaluate the applicability of similar transformations to type systems defined for mobile calculi.Task PI1.5Probabilistic abstract interpretation.Techniques based on probabilistic abstract interpretation turn out to be very appropriate for the construction of static analyses of approximate properties. Considering approximate rather than absolute properties corresponds to asserting the property up to a given error margin rather than as a Boolean relation. The significance of this approach is that it allows in general for more realistic analyses. As an example, a security property such as confinement is never satisfied by real systems in its absolute formulation asserting whether the system is confined or not. We plan to relate these probabilistic abstract interpretation based techniques for the analysis of approximate (security) properties to non-standard type-inference based analyses for such properties. By showing a correspondence (in fact a duality) between these two different approaches to static analysis, we can take advantage of the efficiency of the algorithms for checking and inferring types of programs which is usually better compared to those used in abstract interpretation (algorithms for finding fixpoints etc.). In order to establish such a correspondence, we will look at the relationship between probabilistic abstract interpretation and non-standard type inference as a special case of the relationship between denotational and axiomatic semantics.Workpackage WP2. Security.Task PI2.1Security properties of object oriented languages.We intend to define suitable abstract interpretations capturing the secure information flow property of object oriented languages. A formal definition of secure information flow in the presence of dynamic object creation and destruction is required. The secure information flow property is normally defined using the notion of non-interference. Classical non-interfernce, in the context of secure information flow theory, requires the definition of a relation between initial and final states of two executions of the same program. Here, the definition of this relation is complicated by the fact that the initial states may differ in the number and type of existing objects. Abstract interpretation should be able to capture the flow of information, both explicit and implicit, among the objects manipulated by the program beeing analysed. Since objects are created dynamically, they are potentially infinite, any finite abstract interpretation will have to coalesce several concrete objects into the same abstraction. Thus, the abstraction may introduce false information flows among unrelated concrete objects. We plan to study abstract interpretations that try to reduce the number of false positives in the program analysis. Objects are normally allocated at run-time in a heap. Abstract domains for the heap dynamic data structure must be defined. We plan to study and, possibly, extend, token based approaches. The secrecy of data stored in the ojects and the allowed information flows among the objects will be modelled using the classical lattice approch of security levels (introduced by Denning). We plan to use a collecting semantics to trace data dependences among the objects. Widening techniques will be studied to guarantee the finiteness of the fixpoint calculation even in the presence of possibly recursive method invocations. We plan to choose Java bytecode as a case study for the techniques resulted from the theoretical research. Then we plan to develop a tool for checking secure information flow property in Java applets. Finally, we want to express the Java bytecode verifier as an abstract interpretation of a suitable semantics. We want to show that abstract interpretation is able to detect a class of safe peograms larger than the one detected by standard implementations. This research will be done in collaboration with the research unit in Bologna.Task PI2.2Probabilistic confinement.An area where probabilistic aspects are particularly important for the analysis is computer security. Perfect security is often unrealistic and unachievable; instead the question arises of how much protection effort leads to what kind of security level, e.g. expected average damage. This leads to a quantitative risk analysis rather than an absolute security certification. In previous work we were looking into the issue of quantifying the confinement level of concurrent systems based on a probabilistic analysis of their behaviour. We plan to extend this approach to distributed systems, the ultimate aim being the development of a semantics based quantitative analysis of distributed systems. As an example we will look at problem how information is being disseminated in distributed systems, addressing not only the problem whether some information will eventually be transmitted from one node in a network to another one, but also the probability that this will happen within a given number of time steps. If one thinks of the information transmitted as of some malicious code (a computer virus or worm) then this kind of quantitative analysis effectively addresses the question of how fast a computer virus with a certain infection mechanism will propagate in a network with a given topology. The intention is that such an analysis will allow for the identification of weaknesses of certain network topologies with respect to some infection mechanisms. Our approach to the static analysis of distributed languages/calculi we will be based on Probabilistic Abstract Interpretation. This requires that we represent the collecting semantics as a linear operator, that is that we introduce a linear operator semantics for networks. One main contribution of this investigation will be the use of tensor product and an explication of its interaction with probabilistic abstract interpretation to allow for a compositional analysis of networks. We believe that tensor product is a particularly suited operation for expressing network semantics: it allows us to combine the results of the analysis of each individual nodes without loss of precision. This provides the basis for a compositional approach to analysis.Task PI2.3Timed non-interferenceA class of possible attacks to network components is based on use of the time. Time can be used to gather information, for example when the execution time is used to reveal a secret key. Time can be also used in direct attacks. If the frequency of the intrusion is high enough, the attacked system cannot work properly. We want to study the strength of a system with respect to the frequency of attacks. To this purpose we specified the system by timed automata and defined a notion of timed non-interference. Timed non-interference embodies also the notion of time and is suitable to detect interference due to the frequency of certain actions. Unfortunately, in many cases the notion of timed non-interference is undecidable. We want to define a suitable abstract interpretation to define suitable tools. This research will be done in collaboration with the research unit in Bologna.Workpackage WP3. Testing and debugging.Task PI3.1Although generally too weak to guarantee correctness, testing is an indispensable technique for the validation of reactive systems. Abstract Interpretation has been used to overcome some of the problems associated with testing such as the termination of a program run within an acceptable interval of time. We plan to use Probabilistic Abstract Interpretation for measuring the error made in the evaluation of the reliability of systems via Monte-Carlo testing. The problem we consider is to determine the probability that a reactive system's response falls within a certain set of possible outputs, i.e. that it passes a certain test. As Monte-Carlo testing of the concrete system is not always feasible, tests can be performed instead on an abstract system. This abstraction introduces a further approximation which must be taken into account in the estimation of the error made by testing. The problem is to find out how much the expectation value (or average) of the abstract system differs from the one of the concrete system. We show how to measure such difference by lifting the abstraction to a probabilistic abstract interpretation.
|
