The Role of Abstract Interpretation in Formal Methods

Patrick Cousot

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

Sujets

• Abstract interpretation
• Formal methods

Informations

• Publié par: profil-zyak-2012
• Nombre de lectures: 22
• Langue: English

Extrait

ˆThe Role of Abstract Interpretation in Formal Methods
Patrick Cousot
´Ecole normale superieure,´ 45 rue d’Ulm, 75230 Paris cedex 05, France
[e-mail]
]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 property