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 >>>

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 >>>

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 >>>

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 >>>