Research program
AIDA - Abstract Interpretation Design and Applications
University Co-ordinator
Università "Cà Foscari" di VENEZIA -
INFORMATICA - VENEZIA(VE)
Research Unit Leader
Agostino CORTESI
Description
The research activity in Venice will be done according to the following workpackages.Workpackage WP1: Static AnalysisTask VE_1 Abstract DomainsThere are several different approaches to grammar-based analysis, e.g., regular type domains, set constraints, and tree schemas. Apart from the different expressiveness and complexity of these approaches, there are also various trade-offs between precision and complexity: deterministic versus non-deterministic grammars, program-specific finite height domains versus generic infinite height domains with various widening operators, and implementation techniques such as tabulation. These will be investigated both analytically and experimentally. The combination of grammar-based domains with other domains such as arithmetic abstractions (such as term-size) will also be studied. The design of these combined domains requires advanced methods for domain refinement and simplification, such as reduced product for independent combination, reduced power and tensor product for relational combination, complementation for domain decomposition and domain compression for removing redundancies. We are interested in introducing an algebra of abstract domain transformers that would help in the systematic design of abstract symbolic domains, for tuning them in accuracy and costs. Our goal is to embed semantic properties in abstract domains in such a way that the transformed domains will induce relevant properties of the analysis such as modularity, completeness, and reversability.WorkPackage WP2: SecurityOur goal is to develop accurate and efficient static analysis methods aimed at guaranteeing the security of software, e.g., confidentiality of data and protection of resources. Particular emphasis will be put on techniques for establishing the absence of malicious information flows in concurrent, distributed, and mobile systems (e.g. when describing cryptographic protocols in Mobile Ambient calculus). We will also investigate how to prove that a given code adheres to a given security policy. This, in turn, requires the development of suitable formalisms for expressing such policies in a way that enables their automatic verification.In particular, we will focus on the following tasks: Task VE_2.1 Behavioural Approach: EmbeddingThe general framework proposed in [BFPR04] allows us to study in a uniform way a wide class of security properties. The framework is parametric with respect to two behavioral relations: observation equivalence and reachability. In particular, it has been shown how the compositionality results applicable to the considered properties are connected to the unwinding condition used to instantiate the framework. It has also been shown how compositionality is crucial to derive proof systems (see [BFPR03a]) which build processes which are secure by construction. However, the framework does not directly give us a way of comparing the security properties derived as different instances. In order to analyse this aspect we intend to study an embedding of our framework into a lattice of abstract interpretation domains. To reach such a result our starting point will be the analysis of the correspondence between observational equivalences and abstract domains. A first advantage of this embedding will be the possibility of exploiting abstract interpretation techniques during the verification phase. Moreover, it might lead to the discovery of new properties just by completing the lattice. We also intend to investigate the relationships between the embedding of our framework into abstract interpretation and the abstract interpretation schema described in the POPL'04 paper "Abstract Non-Interference" by Giacobazzi and Mastroeni. On the one hand, this comparison would allow us to integrate the two frameworks from a theoretical point of view. On the other hand, it would suggest us how to combine algorithms and verification techniques coming from the two areas of Static Analysis and Dynamic Verification (Model Checking). For instance, the technique described by Giacobazzi and Mastroeni to derive the most precise domain for which a given program is secure recalls the coarsest partition relation problem which is at the basis of the efficient computation of bisimilarities.Task VE_2.2 Behavioural Approach: Extensions and Comparisons Another, orthogonal, aspect which we intend to investigate is the generalization of our framework to deal also with infinite (large) state processes. This generalization can be obtained by exploiting again abstract interpretation techniques to map the infinite (large) model into a finite one, similarly to what has been done in the area of Abstract Model Checking. Starting from this result and using standard representation techniques we plan to extend our framework to include different languages, e.g., imperative languages. In particular, concrete and abstract semantics of programming languages can be given in terms of Labelled Transition Systems (LTS) by simply representing all the evolutions of the possible computations. Since, the core of our security properties framework relies only on the notion of LTS (endowed with observational equivalences and reachability notions) it is quite natural to exploit it in the analysis LTS based semantics. However, to ensure the applicability of our verification techniques (i.e., to keep size of the LTS under control) it is necessary to deeply analyse the use/combination of different abstract semantics. Many type systems have been proposed to analyse/check the security of programming languages (see "A. Sabelfeld and A. C. Myers. Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communications, 21(1):5-19, IEEE Computer Society Press, 2003" for a survey). Type systems can be seen as particular abstract interpretation domains, hence an extension of our framework based on concrete/abstract semantics would allow us to compare our verification techniques with type checking based techniques.Task VE_2.3 Control-Flow approach: Abstract Domain's Refinement and Algorithms' OptimizationWe intend to refine the abstract domains of the analysis of [BCF02], by using contextual information to confine the effects and the values of the objects of the system. Enhancing the precision of the result can however affect the efficiency of the analysis. Time and space complexities are key-issues for evaluating scalability and practical impact of any static analysis proposal, a careful study is therefore needed to balance the precision and the efficiency of the analysis. In [BCFLP04], we introduced two new algorithms which improve both time and space complexities of the techniques proposed by Nielson and Seidl in [NS01]. We would like to investigate how the method scales up to a class of control flow analyses with particular rule format.Task VE_2.4 Control Flow apprach: ComparisonsSeveral static techniques, formalised as Type systems or Control Flow Analyses, have been devised to study and estabilish various security properties in Mobile Ambients, such as secrecy and informationflow. These approaches are strictly related and compute safe approximations of similar information on the run-time topological structure of processes. Although these methods are proved sound with respect to a formal semantics, they are typically formulated in different styles. As a consequence, it is rather difficult to formally compare them, and the corresponding algorithms for constructing the least analysis or for type-inference. We believe that, by fully understanding the interplay between abstract interpretation and Control Flow Analysis in Flow Logic style, we would benefit from the well-estabilished theory of Abstract Interpretation, thus we would be able to compare the expressive power of the two techniques, understand the pros and cons of each approach, and possibly for which class of properties one method is more adequate than another.
|
