3 Pages
English

The Role of Abstract Interpretation in Formal Methods

-

Gain access to the library to view online
Learn more

Description

Niveau: Supérieur, Doctorat, Bac+8
The Role of Abstract Interpretation in Formal Methods Patrick Cousot Ecole normale superieure, 45 rue d'Ulm, 75230 Paris cedex 05, France st n rt . .c oCo fui @eskaP r Formal methods In computer science and software en- gineering, formal methods are mathematically-based tech- niques for the specification, development and verification of software and hardware systems. They therefore establish the satisfaction of a specification by a system semantics. Abstract Interpretation Abstract interpretation [3, 8] is a theory of sound approximation of mathematical structures, in particular those involved in the description of the behav- ior of computer systems. It allows the systematic deriva- tion of sound methods and algorithms for approximating undecidable or highly complex problems in various areas of computer science (semantics, verification and proof, model- checking, static analysis, program transformation and opti- mization, typing, software steganography, etc.). Its main current application is on the safety and security of complex hardware and software computer systems. Semantics The semantics SJpK is a formal model of the execution of these software and hardware systems p ? P. A semantic domain D is a set of such formal models (so ?p ? P : SJpK ? D). An example is an operational semantics of a program describing all possible program executions as a set of max- imal traces that is finite or infinite sequences of states in ?, two successive states corresponding to an elementary pro- gram step.

  • abstract interpretation

  • methodes iteratives de construction et d'approxi- mation de points fixes d'operateurs monotones

  • based abstractions

  • sjpk ?

  • formal methods

  • trace logic

  • model checkers


Subjects

Informations

Published by
Reads 22
Language English

ˆThe Role of Abstract Interpretation in Formal Methods
Patrick Cousot
´Ecole normale superieure,´ 45 rue d’Ulm, 75230 Paris cedex 05, France
Patrick.Cousot@ens.fr
]Formal methods In computer science and software en- C J K and a sound under-approximation of the property
]gineering, formal methods are mathematically-based tech- P P and make the correctness proof in the abstract
] ]niques for the specification, development and verification C J KP .
] ]of software and hardware systems. They therefore establish For automated proofs,C J K andP must be computer-
the satisfaction of a specification by a system semantics. representable and are not chosen in the concrete domainhP;
]Abstract Interpretation Abstract interpretation [3, 8] is i but in an abstract domainhP ;vi. The correspondence
]a theory of sound approximation of mathematical structures, is given by a concretization function2P 7!P provid-
] ]in particular those involved in the description of the behav- ing the meaning (P ) of abstract properties P and pre-
]ior of computer systems. It allows the systematic deriva- serving the abstract implication8Q ;Q 2P : (Q v1 2 1
] ]tion of sound methods and algorithms for approximating Q ) =) ((Q ) (Q )). ThenC J Kv P implies2 1 2
] ] ]undecidable or highly complex problems in various areas of (C J K) (P ) and by soundnessCJ K (C J K)
]computer science (semantics, verification and proof, model- and(P )P we have proved correctnessCJ KP .
checking, static analysis, program transformation and opti-
Best Abstraction If we want to over-approximate a disk
mization, typing, software steganography, etc.). Its main
in two dimensions by a polyhedron there is no smallest
current application is on the safety and security of complex
one, as shown by Euclid. However if we want to over-
hardware and software computer systems.
approximate a disk by a rectangular parallelepiped which
Semantics The semanticsSJ K is a formal model of the
sides are parallel to the axes, then there is definitely a
execution of these software and hardware systems 2 .
smallest (square) one. In such a case there is an abstrac-
A semantic domainD is a set of such formal models (so ]tion function 2 P 7! P such that for all P 2 P,
8 2 :SJ K2D). ](P ) 2 P is an abstract over-approximation of P (so
An example is an operational semantics of a program
P ((P ))) and it is the most precise abstract over-
describing all possible program executions as a set of max- ]approximation (so8Q2P : P (Q) =)(P )v Q
imal traces that is finite or infinite sequences of states in ,
whence((P ))(Q) by monotony of). It follows in
two successive states corresponding to an elementary pro-
that case of existence of a best abstraction, that the pairh;1gram step. In that caseD,}(T ) that is a subset of the set
S i is a Galois connection [8].+1 n nT , of all possible traces where , [0;n[7! n=1 Abstraction is very often implicit, as shown by the fol-
is the set of traces of lengthn,n = 0; 1;:::; +1.
lowing classical examples.
Properties and Specifications A specification is a re-
quired property of the semantics of the system. The interpre- Aggregation Abstraction In the operational trace seman-
tation of a property is therefore a set of semantic models that tics exampleD , }(T ) so properties areP , }(}(T ))
satisfy this so the set of properties isP , }(D). whereT is the set of traces. An example isP ,ff0j01
The strongest property of a system 2 is its semantics 2Tg;f1j 2Tgg2P specifying that executions
fSJ Kg (called the collecting semanticsCJ K,fSJ Kg). of the system always terminate with 0 or always terminate
with 1. This cannot be expressed in the traditional view ofVerification The satisfaction of a specificationP2P by
program properties as set of traces [1, 21]. This traditionala system (more precisely by the system semanticsSJ K)
understanding of a program property is given by the aggre-isSJ K2P , which can equivalently be defined as the proof S
gation abstraction 2}(}(T ))7!}(T ), (P ), P[ [thatCJ KP .
with concretization 2 }(T ) 7! }(}(T )), (Q) ,[ [Abstraction To proveCJ K P one can use a sound
}(Q). An example is (P ) = ff0;1 j 2 Tgg[ 01over-approximation of the collecting semanticsCJ K
specifying that execution always terminate, either with 0 or
1 0 0}(S),fS j S Sg is the powerset of the setS. with 1.
ppPPppppppPppppppppppppppTransition Abstraction The transition abstraction 2 the algorithm does not terminate in general). For example
}(T ) 7! }( ) collects transitions along traces. in model-checking any abstraction of a trace logic may be
( ::: ) , f ! j 0 6 i < ng, incomplete [17]. 0 n i i+1
( ::: :::) ,f ! j i > 0g, and (T ) , 0 i i i+1 Verification by Static Analysis Static code analysis isS
f()j 2 Tg. The concretization 2 }( ) 7! the analysis of computer system by direct inspection of theS+1
}(T ) is () , f2 [0;n[7! j8i < n :h ; in=1 source or object code describing this system with respect to
i2 g. The abstraction may also collect initial statesi+1 a semantics of this code (without executing programs as in
(T ),f j2Tg so (T ),h (T ); (T )i. We 0 dynamic analysis). The static code analysis is performed by
let , ()\ () where () ,f2T j 2 g 0 an automated tool, as opposed to program understanding or
(h ; i is a Galois connection). program comprehension by humans. The proofCJ K P
] ]This abstraction into a transition system [3] underlies is done in the abstractC J KP , which involves the static
]small-step operational semantics. This is an approximation analysis of that is the effective computation ofC J K, as
since traces can express properties not expressible by a tran- formalized by abstract interpretation [3, 8].
sition system (like fairness of parallel processes).
Adequation of Abstractions The reachability abstraction
Input-Output Abstraction The input-output abstraction is sound and complete for invariance/safety proofs. That
2 }(T ) 7! }( ( [f?g)) collects initial andio means that ifS is a set of safe states so that (S) isr
final states of traces (and maybe ? for infinite traces a set of safe traces then the safety proofCJ K (S) canr
to track nontermination). ( ::: ) = h ; i,io 0 n 0 n always be done as (CJ K)S. This is the fundamentalr
( ::: :::) =h ;?i, and (T ) =f ()j 2 remark of Floyd [16] that it is not necessary to reason onio 0 i 0 io io
Tg. The input-output abstraction underlies denotational traces to prove invariance properties. This does not meanio
semantics, as well as big-step operational, predicate trans- that this abstraction is adequate, that is, informally, the most
former and axiomatic semantics extended to nontermination simple way to do the proof. For example Burstall’s inter-
[5] and interprocedural static analysis using relational pro- mittent assertions may be simpler than Floyd’s invariant as-
cedure summaries [3, 7, 12]. sertions [10] or, in static analysis trace partitioning may be
more adequate that state-based reachability analysis [19].Reachability Abstraction and Invariants The reachabil-
ity abstraction 2 }(T )7! }( ) collects states along Property versus Model-based Abstraction Leth ;i ber
ntraces. (T ),f j9n2 [0; +1] : 2 \T^i2 a transition system model of a software or hardware systemr i
0 0 ?[0;n[g =fs 2 j 9s 2 : hs; si 2 g where 2 (so thatSJ K, (h ; i)). A model-based ab-
? ] ] (T ) =h ; i is the transition abstraction and is the straction is an abstract transition systemh ;i which over-
]reflexive transitive closure of. Expressed in logical form, approximatesh ; i (so that, up to concretization,
] ] ]the reachability abstraction provides a system invariant and ). The set of reachable abstract states forh ;i
(CJ K) that is the set of all states that can be reached along over-approximate the concrete states ofh ; i so
some execution of the system [3, 6]. the model-based abstractions yields sound abstractions of
the concrete reachability states. Some definedFloyd’s method [16] to prove a reachability property
by a Galois connection of sets of (reachable) states may not (T )P consists in finding an invariantI stronger thanr
be model-based abstractions, in particular when the abstractP (i.e.I P ) which is inductive (i.e. I and[I] I
0 0 domain is not a powerset of states (e.g. [20]).where[I],fs j9s2I :hs; si2g is the right-image
transformer for the transition systemh ;i = (T )). This Program-based versus Language-based Abstraction
induction principle has many equivalent variants [9], all un- Static analysis has to define an abstractionJ K for all pro-
derlying different static analysis methods (the equivalence grams 2 of a language . This is different from defin-
may not be preserved by abstraction). In particular back- ing an abstraction specific to a given program. In particu-
1 1ward analyzes are based onh ; (T )i where is the’ lar an to a given program can always
ninverse of and (T ),f jn< +1^2T\ g’ n 1 be refined to be complete using a finite abstract domain [4]
collects final states. whereas this is impossible in general for a language-based
abstraction for which infinite abstract domains have beenSoundness and Completeness of Abstractions An ab-
] ] shown to always produce better results [11].straction is sound if the proof in the abstractC J K P
implies the concrete propertyCJ KP . Abstract interpre- False Alarms Static analysis being undecidable, it relies
tation provides an effective theory to design sound abstrac- on incomplete language-based abstractions. This means
tions. An abstraction is complete if the fact that the system that the analyzer will produce false alarms on infinitely
is correct, that isCJ K P , can always be proved in the many programs (which can even be generated automati-
] ]abstract asC J K P . By refining the abstraction this is cally). A false alarm is a case when a concrete property
always possible [18], but this refinement is not effective (i.e. holds but this cannot be proved in the abstract for the given
ppppppppppPpppPpppPabstraction. An example in reachability analysis is when References
[1] B. Alpern and F. Schneider. Defining liveness. Inf. Process.no inductive invariant can be expressed in the abstract. The
Lett., 21:181–185, 1985.experience of ASTRE´ E (www.astree.ens.fr, [2]) shows
[2] B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne,that it is possible to design precise language-based abstrac-
A. Mine,´ D. Monniaux, and X. Rival. A static analyzer for
tions which produce no false alarm on a well defined family
large safety-critical software. ACM PLDI, 196–207, 2003.2of programs . [3] P. Cousot. Methodes´ iter´ atives de construction et d’approxi-
mation de points fixes d’oper´ ateurs monotones sur un treillis,Design of Abstractions The design of a sound and pre-
´analyse semantique´ de programmes (in French). These` d’Etatcise language-based abstraction is difficult. First from a
es` sciences mathematiques,´ Universite´ scientifique et medica-´mathematical point of view, one must discover the appro-
le de Grenoble, Grenoble, 1978.priate set of abstract properties that are needed to represent
[4] P. Cousot. Partial completeness of abstract fixpoint checking.the necessary inductive invariants. Of course mathematical
SARA, LNAI 1864, 1–25. Springer, 2000.
completion techniques could be used [18] but because of
[5] P. Cousot. Constructive design of a hierarchy of semantics of
undecidability, they do not terminate in general. Second, a transition system by abstract interpretation. Theoret. Com-
from a computer-science point of view, one must find an put. Sci., 277(1—2):47–103, 2002.
appropriate computer representation of abstract properties [6] P. Cousot and R. Cousot. Abstract interpretation: a unified lat-
and abstract transformers. Universal representations (e.g. tice model for static analysis of programs by construction or
thapproximation of fixpoints. 4 ACM POPL, 238–252, 1977.using symbolic terms, automata or BDDs) are in general
[7] P. Cousot and R. Cousot. Static determination of dynamicinefficient and the discovery of appropriate computer repre-
properties of recursive procedures. IFIP Conf. on For-sentations is far from being automatized.
mal Description of Programming Concepts, 237–277, North-
Local versus Global Abstractions A simple approach to Holland, 1977.
static analysis is to use the same global abstraction every- [8] P. Cousot and R. Cousot. Systematic design of program anal-
thwhere in the program, which hardly scales up. More sophis- ysis frameworks. 6 ACM POPL, 269–282, 1979.
´ [9] P. Cousot and R. Cousot. Induction principles for proving in-ticated abstractions, as used in ASTREE are not uniform, dif-
variance properties of programs. Tools & Notions for Programferent local abstractions being in different program regions
Construction, 43–119. Cambridge U. Press, 1982.[2].
[10] P. Cousot and R. Cousot. Sometime = always + recursion
Multiple versus Single Abstractions Because of the always: on the equivalence of the intermittent and invari-
complexity of abstractions, it is simpler to design a precise ant assertions methods for proving inevitability properties of
abstraction by composing many elementary abstractions programs. Acta Informat., 24:1–31, 1987.
´which are simple to understand and implement. ASTREE [11] P. Cousot and R. Cousot. Comparing the Galois connection
and widening/narrowing approaches to abstract interpretation.uses many weakly relational domains (such as octagons
PLILP ’92, LNCS 631, 269–295. Springer, 1992.[20], digital filters [14], arithmetico-geometric progressions
[12] P. Cousot and R. Cousot. Modular static program analysis.[15], etc) that could hardly be encoded efficiently using a
th11 CC, LNCS 2304, 159–178, Springer, 2002.
universal representation of program properties as found in
´[13] P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Mine,
theorem provers, proof assistants or model-checkers. D. Monniaux, and X. Rival. Combination of abstractions
thAbstraction Reduction If several abstractions are used, in the ASTRE´ E static analyzer, invited paper. 11 ASIAN,
LNCS, Springer (to appear).the static analyzer must implement their conjunction in the
th[14] J. Feret. Static analysis of digital filters. 30 ESOP, LNCSconcrete, that is their reduced product in the abstract [8].
2986, 33–48. Springer, 2004.The implementation must be extensible, allowing for the
[15] J. Feret. The arithmetic-geometric progression abstract do-
easy incorporation of new abstractions [13]. thmain. 6 VMCAI, LNCS 3385, 42–58, Springer, 2005.
Refinement For a single program-based abstraction, re- [16] R. Floyd. Assigning meaning to programs. Proc. Symp. in
finement consists in strengthening the abstract invariant un- Applied Math., vol. 19, 19–32. AMS, 1967.
[17] R. Giacobazzi and F. Ranzato. Incompleteness of states w.r.ttil it is inductive, through a fixpoint computation which
traces in model checking. Inform. and Comput., 204(3):376–in general does not terminate or explodes combinatorially.
407, Mar. 2006.The problem is even harder for language-based abstractions.
[18] R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract´The pragmatic approach used in ASTREE is to manually de-
interpretations complete. J. ACM, 47(2):361–416, 2000.
sign new abstractions which are incorporated in the reduced
[19] L. Mauborgne and X. Rival. Trace partitioning in abstract
product of all used by the analyzer thus allow- thinterpretation based static analyzer. 14 ESOP, LNCS 3444,
ing for the strengthening of the abstract invariants for all 5–20. Springer, 2005.
programs until no false alarm is left [13]. [20] A. Mine.´ The octagon abstract domain. Higher-Order and
Symb. Comp., 19:31–100, 2006.
2 thSynchronous, time-triggered, real-time, safety critical, embedded soft- [21] A. Pnueli. The temporal logic of programs. 18 ACM FOCS,
ware written or automatically generated in the C programming language 46–57, 1977.
´for ASTREE.