RICERCA ITALIANA     

AIDA - Abstract Interpretation Design and Applications

Università degli Studi di Verona

Abstract

Abstract interpretation is a general theory for approximating the semantics of dynamic systems. This theory is widely used for instance for formally deriving static program analysis tools from program semantics. In AIDA, abstract interpretation will serve as the foundational theory to design methodologies and to develop tools to ensure the interoperability, composability, scalability, reliability, robustness, dependability, and security of software and systems. The initial purpose of the AIDA project to is mobilize, unify, galvanize and strengthen the italian abstract interpretation community towards a common goal, which is the design of a uniform advanced platform for automatic system certification by abstract interpretation. We are particularly interested in certifying secure information flows, robustness and reliability of complex systems involving software components and having a potential hybrid behavior. We will approach this problem by refining existing abstract interpretation methods in static program analysis and language-based security, by integrating them with constraint-based description of infinite-state systems and verification methods like model checking. This goal will be achieved by identifying a common pattern in the design of abstract interpretation in: Static program analysis, Security, Testing, Hybrid systems, Constraints, and Automatic verification. Abstract interpretation provides here a common unifying framework where problems coming from different aspects of system certification, which may deeply differ in nature and application, can be integrated to enrich both abstract interpretation theory and practice. Automatic system certification for both discrete dynamic and hybrid systems represents here the perfect application ground for both studying more fundamental aspects of abstract interpretation, like domain theoretic foundations for precision and complexity of program analysis, and for providing useful prototype tools for semantics-based program certification that can directly be embedded in modern software systems. <<<

Principal Investigator

Roberto GIACOBAZZI Università degli Studi di VERONA

Research Objectives

Guaranteeing the reliability, trustworthiness, safety and security of computer systems is a major challenge for modern societies. We rely on systems that are pervasive in human life, are increasingly complex and, at the same time, we experience how spectacularly traditional validation methods, such as testing, may fail to provide the required guarantees despite their very high cost: The failure of Ariane 5 on June 1996, is a famous example. This justifies the growing interest in flexible semantic-based SW technologies for program analysis, verification and manipulation in all system development phases. Abstract interpretation can play a key role in this trend. In AIDA, abstract interpretation will serve as the foundational theory to design methodologies and to develop tools to ensure the interoperability, composability, scalability, reliability, robustness, dependability, and security of software and systems. The initial purpose of the AIDA project to is mobilize, unify, galvanize and strengthen the italian abstract interpretation community towards a common goal, which is the design of a uniform platform for automatic system certification by abstract interpretation. Italy is a long standing active county in abstract interpretation, as proved by the AIDA consortium including 7 universities, more than 25 permanent researchers directly involved in abstract interpretation, more than 10 experts from other fields, such as security, hybrid systems, model checking, and concurrency, interested in joining abstract interpretation as a foundational theory for system certification, and more than 20 among PhD and Post Doc young researchers. Moreover, the interest of italian industries is growing around abstract interpretation, as proved by the recent contracts and expressions of interests in this project shown by GlaxoSmithKilne S.p.A (GSK), CAD-IT S.p.A, and CRF - FIAT.

We are particularly interested in certifying secure information flows, robustness and reliability of complex systems involving software components and having a potential hybrid behavior. We will approach this problem by refining existing abstract interpretation methods in static program analysis and language-based security, by integrating them with constraint-based description of infinite-state systems and verification methods like model checking. This goal will be achieved by identifying a common pattern in the design of abstract interpretation in the following workpackages (WP), coordinated by a recognized expert in the field: WP1: Static program analysis, WP2: Security, WP3: Testing, WP4: Hybrid systems, WP5: Constraints, and WP6: Automatic verification.

WP1: Static program analysis. We are interested in data/control flow analysis by abstract interpretation, in particular in the context of concurrent and OO calculi. In this field we are interested in foundational aspects such as abstract domain design technology, abstract semantics of concurrent and mobile calculi, fixpoint strategies such as widening/narrowing, and efficient implementation and integration in certifying compilers and interpreters. The interest in this phase is particularly focused on new abstract domains providing relational information, which is crucial in any language-base security SW certification (WP2).

WP2: Security. In this workpackage we are interested both in weakening standard non-interference by abstract interpretation and in enhancing semantic models (e.g. bisimulation semantics) to cope with abstract interpretation and quantitative measure concerning information leakage, in connection with WP5, WP6 and WP4. In the last case it would be particularly interesting to derive models of hybrid attackers, which involves both discrete and continuous behavior.

WP3: Testing. We are interested in code reuse and modular static analysis applied to code regression, in connection with WP1 and WP5. When a bug has been fixed, a regression test runs tests to verify that the defect is in fact fixed. But, regression testing is also played as the dual of integration testing: when new code is added to existing code, regression testing verifies that the existing code continues to work correctly, whereas integration testing verifies that the new code works as expected. We are interested in systematic design of regression and integration analysis and verification of programs. The advantage of abstract interpretation is clear, as compositionality is a major feature of semantics-based technology, in particular to automatically derive preconditions for code composition minimizing regression-testing drawbacks and to isolate test vectors which are invariant by code upgrade.

WP4: Hybrid systems. We are interested in modeling and designing verification techniques for hybrid systems by combing constraint and standard abstract interpretation. In particular we are interested in using abstract interpretation to systematically derive approximate discrete systems out of a hybrid one. This approach needs enhanced abstract domain design technology (e.g. developed in WP1 for numerical domains) such as constraint-based models for region automata and abstract domain refinement and compression in order balance the state explosion phenomenon and the need of abstractions satisfying the strong preservation relatively to some temporal logic fragment. This WP is strongly related with WP1, WP2, WP5 and WP6.

WP5: Constraints. We plan to investigate the combined application of abstract interpretation and constraint programming for the analysis and verification of multithreaded software programs. To scale up on practical examples, it is critical to study how to extract abstract models from programs and how to perform analysis compositionally. Moreover we are interested in integrating constraint techniques developed for relational abstract domains in WP1 with constraint-based specification (temporal) logic studied in WP6, in order to provide enhanced tools for certifying complex systems and, in connection with WP4, for refining region automata.

WP6: Automatic verification. We are interested in systematic design of abstract model checking verifying strong preservation relative to some fragments of a temporal logic and in the context of multi-level temporal structures, including constraints, intervals, metric and periodicity. In particular we are interested in deriving the most concrete (strongest) logic for which abstract model checking under a given fixed abstraction is strong preserving. Moreover we are interested in understanding the role of abstract domain transformers, such as abstraction refinement and compression, in abstract model checking, in particular in generalizing known efficient algorithms such as the Paige-Tarjan partition refinement algorithm which combines partition (abstraction) compression and refinement.

We identify a common pattern which will be shared by all WP's in AIDA, which consists of the following 5 phases, each one coordinated by a recognized expert in abstract interpretation. The sequence of phases 1--5 is the standard agenda in the design of any abstract interpretation:

Phase 1: Abstraction properties
Phase 2: Abstract domains
Phase 3: Models and semantics
Phase 4: Fixpoint strategies and algorithms
Phase 5: Implementation

The matrix structure of the project in WP's and phases ensures the correct coordination between them. In particular, by sharing the same phases, each WP will benefit of a common technology in abstract interpretation design and implementation. Each partner will be directly involved in WP's and phases, by local tasks coordinated by WP and unit leaders and phase coordinators.

<<<

First Results

The expected results in this phase are:
- A clearly defined algebra of abstract domain transformers, including relevant properties of abstractions encoded as abstract domain transformers, such as strong preservation for abstract model checking of discrete and hybrid systems against fragments of temporal logic, absence of false alarms in numerical and relational abstract domains, and compositionality for test regression (all WP's)
- Precise conditions for abstract domain reversibility and relative algorithms for reversing abstract domain refinements in the sense of abstract domain compression, i.e. towards an operation that returns, when it exists, the most abstract domain having the same refinement as its input domain (WP1, WP4 and WP6)
- Extension of the algebra of abstract domain transformers toward fixpoint strategies, such as widening/narrowing techniques (WP1, WP4, and WP5)
- A characterization of properties of hybrid systems as properties of their abstraction (WP4)
- A Taxonomy of abstractions in abstract model checking under the strong preservation requirement relatively to fragments of the mu-calculus (WP6).The expected results in this phase are:
- Improved domains for attribute independent program analysis over numerical domains (WP1)
- Improved domains for relational program analysis over numerical domains (WP1 and WP5)
- Design of enhanced symbolic domains for OO code static analysis adequate for compositionality (WP1, WP2 and WP5)
- Systematic design of abstract domains for type inference (WP1, WP2 and WP6)
- Design of optimal domains and operations for aliasing in declarative programming languages (WP1)
- Design of domains for infinite region approximation for discretizing hybrid automata (WP4)
- Enhanced domains with quantitative measure (WP1 and WP2)
- A logical framework for dealing with abstractions as certificates (WP2).The expected results in this phase are:
- Design of compositional models for static analysis and verification of mobile ambient
- Design of semantics for modeling abstract non-interference in concurrent calculi
- Design of semantics for modeling abstract non-interference in real-time and hybrid systems
- Design syntax-directed proof-systems for abstract non-interference
- Design models for multithreaded languages based on CCP and CHR languagesThe expected results in this phase are:
- Advanced fixpoint strategies for numerical domains (WP1, WP4, WP5, and WP6)
- Handling NNC polyhedra (WP1, WP4, and WP5)
- Enhanced escape and class analysis by set-constraints (WP1 and WP5)The expected results in this phase are:
- A general purpose library of numerical domains for relational and attribute-independent program analysis (WP1 and WP5)
- An efficient implementation for class and escape analysis in Julia (WP1 and WP5)
- Experimental evaluation of abstract domain refinement and compression in the context of abstract model checking (WP6)
- A PCC-like prototype architecture for certifying abstract non-interference relatively to predicate abstractions (WP2)
- A prototype parametric program slicer implementing abstract non-interference based slicing criteria (WP3 and WP3).
- A prototype model checker for timed concurrent constraint programs (WP4, WP6, and WP5). <<<

Timescale

24 months

National and international background

Abstract interpretation is well known as a general theory for approximating the semantics of dynamic systems [CC77]. Introduced by Cousot and Cousot [CC77] as a unifying framework for designing and then validating static (compile-time) program analyses, in recent years abstract interpretation has increasingly gained popularity as a general methodology for describing and formalizing approximate computations in many different areas of computer science. We are interested in design methods which are common in most applications of abstract interpretation from static program analysis to security, verification and testing in both discrete/hybrid finite/infinite state systems.

- Standard abstract domain design and applications
The success of abstract interpretation stems from its simple, but nevertheless rigorously defined, underlying idea that the specification of the behavior of a system, e.g., a program, at different levels of abstraction, is a suitable approximation of its formal semantics [C76th,CC77,JN95,NNH99]. In the context of this project we are interested in using the essence of the abstract interpretation view, which is analyzing systems by approximating its semantics, as a concrete and adequate unifying paradigm for designing and specifying certification methods for both SW components and for dynamic hybrid systems. A fundamental feature of abstract interpretation is that most properties of the analysis derive from the properties of underlying concrete model of computation (semantics) and of the abstraction, the last being uniquely identified by the chosen abstract domain. Therefore, transforming domains and semantics is transforming analyzers. A number of operators have been designed to systematically improve precision, reduce complexity, and modularize analyses by refining, simplifying and decomposing domains. The foundation of a theory of abstract domains and abstract domain transformers was fixed by Cousot and Cousot in [CC79]. After that, a unifying algebraic setting for abstract domain transformers have been introduced in [FGR96,GR97,GR98unif]. However, while the calculational derivation of sound and complete approximate models from abstractions is well known [CC99], no such methodologies are known to provide an analogous calculational design of domain transformers. Most of well known operations for refining and simplifying domains are in fact the result of either solutions to specific problems in refining or simplifying domains (e.g. disjunctive completion [CC79,CC94,J92], complete refinements and kernels [GRS00], reduced power [CC79], and Heyting completion [GS98]) or inherited directly from the basic structure of the lattice of abstract interpretations (reduced product [CC79], complementation [CFGPR97]). Completeness plays a key role in abstract interpretation, and in particular in most problems concerning abstraction refinement [BPR02]. While standard abstract interpretation ensures soundness, completeness formalizes the intuition that, relatively to the properties encoded by the underlying concrete domains, there is no additional loss of information accumulated in abstract computations. Complete abstractions can be always constructively derived [GRS00] as the least complete refinement and the greatest complete restriction of any abstract domain. Two notions of complete abstractions have been introduced in [GQ01]: forward and backward completeness, the second being precisely standard completeness. These two notions correspond respectively to ask that an abstract domain includes the forward and backward image of the semantics for which it has to be complete. These results provide advanced abstract domain transformers to achieve both forms of completeness by minimally refining or simplifying domains. However, in order to gain efficiency, the design of adequate domains is not often sufficient. The experience gained in Italy with the development of the aliasing analysis component of the China analyzer [BHZ02, ZHB02] and with the ongoing development of the ``Parma Polyhedra Library'' [BHRZ03, BHZ03, BRZH02] has shown that the creation of a professional, full-fledged abstract domain is a very significant and challenging task (both from the theoretical and the implementation points of view), involving complex domain transformers and people over several years. Efficient fixpoint strategies such as widening/narrowing fixpoint acceleration techniques [CC77] are often required, and often are the added value of most abstract interpretation-based algorithms for program analysis. This is particularly crucial in relational domains, like polyhedra [CH78], where abstractions provide precise approximations of the relations between program's variables. The most recent developments in this field lead to the search of a balance between precision and complexity. As an example, octagons [Min01] offer a simpler and computationally efficient example of relational abstractions. Relational analysis is particularly relevant in complexity analysis. This is a rather unexplored field, whose aim is the derivation of upper and lower bounds to the complexity of algorithms, processes, data structures and programs, by approximating semantics. The results of such analyses, which may be partially or wholly automated, can be used, say, to decide whether mobile agents should be allowed to run in a given context, assist programmers in reasoning about the behavior of programs, guide applications of optimized program transformations, and discover efficiency bugs that are otherwise very difficult to detect [DL93].

- Security
Type systems, control/data flow analyses (CFA) based on flow logic, and abstract interpretation are the most known techniques, which have been successfully applied to statically verify security properties of mobile and distributed systems, modelled in Ambient Calculus or in some of its variants [LS03, MPW92], or modelled by object oriented calculi. The Flow Logic [NN02] is based on a constraint based analysis which allows to integrate state-of-the-art insights from abstract interpretation and data flow analysis. In calculi of mobile agents, abstract interpretation has been mainly applied [LM04, HJNN99] to refine existing analyses, such as the CFA of [NNH99] and Flow Logic, all devoted to certify security by control/data flow analysis of confidential vs public channels. In a system, information is typically protected via some access control policies, limiting accesses of entities (such as users or processes) to data. In Multilevel Security [BP] entities and data are associated to (ordered) security levels and no access to data at higher levels is ever possible, even if the owner of the data is willing to reveal them. These strong mandatory security policies have been designed to avoid internal attacks performed by the so called Trojan Horse programs, i.e., malicious software that, once executed by a user, modifies the access rights of the data belonging to such a user. Unfortunately, even when direct access to data is forbidden by (strong) security policies, it might be the case that data are indirectly leaked by Trojan Horses which might exploit some observable system side-effects like, e.g., the CPU load or, more in general, the space/time availability of shared resources (see, e.g., [M89]). The necessity of controlling information flow as a whole (both direct and indirect) motivated Goguen and Meseguer in introducing the notion of non-interference [GM82]. Non-Interference requires that confidential inputs never affect the outputs on the public interface of the system. If such a property holds, one can conclude that no information flow is ever possible from confidential to the public level. This is clearly a too restrictive condition: Since most variables are semantically interdependent, most programs will not pass a rigorous non-interference test. The problem of refining security policies, i.e. weakening non-interference, has been addressed as a major challenge in language-based security (see [SM03] for a survey). In [GM04,Low02,VS00] the problem of characterizing the degree of secrecy of a program has been linked to the power of the successful/harmless attacker. The idea in [GM04] is to consider attackers as abstract interpretations, whose task is to reveal properties of confidential data by statically analyzing public resources. A domain transformer characterizing the most powerful harmless attacker unable to disclose properties of confidential data has been introduced together with a domain transformer that identifies the maximal amount of information disclosed by a program under attack. The extension of abstract non-interference to more complex models of interaction, e.g. in communicating protocols, and models of computation (e.g. concurrency and probabilistic non-determinism) is still open. In order to cope with more complex semantic models, abstractions need to be further refined. The idea of enhancing abstract interpretation with probabilistic and quantitative aspects is relatively new and has a great impact in language-based security [SM03]. The approach developed in [M00] consists in the application of (classical) abstract interpretation-based techniques to give upper bounds on the worst-case probability of the a given program property, while in [M01] a combination of random testing and abstract interpretation has been proposed for the analysis of programs featuring both probabilistic and non-probabilistic nondeterminism. Further techniques have been proposed in [DW00a, DW00b] by re-casting the classical framework in a probabilistic setting. Standard non-interference has been also considered in different settings such as process algebra [RS01,FG01], timed models [GLM03], cryptographic protocols [FGM00]. A possibilistic security property can be regarded as an extension of non-interference to non-deterministic systems. In [FG01] the concept of non-interference in the Security Process Algebra (SPA) has been introduced in terms of bisimulation semantics. A system E is BNDC (Bisimulation-based non Deducibility on Compositions) if what a low (public) level user sees of the system is not modified (in the sense of the bisimulation semantics) by composing any high (private) level process with E. The main advantage of BNDC with respect to trace-based properties is that it is powerful enough to detect information flows due to the possibility, for a high level malicious process, to block or unblock a system. In [FG01], it is shown that a malicious process may build a channel from high to low, by suitably blocking and unblocking some system services accessible by low level users. The system used to build this covert channel turns out to be secure for trace- based properties, justifying bisimulation as concrete semantics.

- Abstract interpretation and verification from discrete to hybrid system
The interest in abstractions in automatic verification methods like model checking is a long standing research theme. The abstract model checking approach [CGL94,CGP99] provides a solution to the critical issue of model checking scalability, the well-known state explosion problem: the basic idea is to check the correctness specification of a (model of a) reactive system M on an abstract model approximating some properties of interest of the concrete model M. An abstract model A strongly preserves a specification language L when any formula of L is valid in the abstract model A if and only if it is valid in the concrete model M. Clearly, this is a highly desirable property for abstract model checking, in particular because this eliminates the so-called spurious counterexamples in abstract verification [CGJLV03,GQ01]. The relationship between abstract interpretation and abstract model checking has been well studied [CC99, CC00, CC02, CGL94, DGG97, GQ01, GR02, LGSBB95, Ran02]. The classical approach to abstract model checking [CGL94,CGJLV03] is based on defining an abstract model as a partition of the set of system states which therefore induces an abstract system. Recent studies [RT04] have proved that strong preservation for classical abstract model checking relatively to any abstract model specified as a generic abstract interpretation can be systematically achieved by transforming abstractions. The authors proved that the problem of minimally refining one such abstract model A in order to get strong preservation for some specification language L corresponds precisely to the problem of minimally refining the underlying abstract interpretation in order to get the completeness property w.r.t. the logical/temporal operators of L. Constraints play a key role in verifying infinite-state systems [Del03], and in particular in verifying communication protocols [AB02]. In this setting, constraints are viewed as symbolic representation of "abstract system models". The application of this technology to multithreaded programs sketched in [DRV02] requires a preliminary abstraction step in which a "model" is extracted from the program. This step can be clearly formalized as an abstract interpretation. By contrast to the discrete case, the use of abstract interpretation in the analysis of hybrid systems is still an open field. Hybrid Systems have received considerable attention in the literature [MMP92,ACH+95,LSV03] because they turn out to be quite useful for the description of real systems, including digital controllers of physical plants and biological systems. A hybrid system describes objects that exhibit discrete as well as continuous behavior, e.g. derived from the field of Control Theory and used as a modeling framework for physical plants, biological phenomena, and of their controllers [ACB+01]. There is an extensive literature about models for hybrid systems and related verification techniques [see, e.g., MMP92,ACH+95,LSV03]. The difficulties lie in the interrelations between discrete and continuous behaviors, where it is required to keep as much as possible the separation between the underlying theories, so that all the known math applies. In particular, when dealing with verification, it is well known how to handle continuous and discrete systems separately, but little is known about hybrid verification techniques. Most of the existing techniques reduce the problem either to the analysis of fully discrete systems or to the analysis of fully continuous system. There is also an extensive literature about model checking of hybrid systems [see, e.g., ACH+95], and essentially in all contributions a hybrid automaton is transformed into a discrete automaton, usually called region automaton or zone automaton, in a way that the validity of temporal logic formulas is preserved. The transformation of hybrid automata into discrete automata does not work in general, and indeed model checking of hybrid systems is not decidable, so the literature has concentrated mainly on the identification of appropriate sub-classes of hybrid automata where the construction of region or zone automata works. The classification of Henzinger et al. in [HM00] introduces the concept of symbolic transition systems to generalize the idea behind region and zone automata, and describes five classes of symbolic transition systems that are characterized in terms of appropriate closure operators and appropriate sub-logics that are preserved. <<<