曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
Overview
Introduction
Static analysis
First analyses
Language and semantics
Design of Astr´ee
Architecture
Iterator
Abstract domains
Results
Antoine Min´e Building a specialized static analyzer p. 4 / 112
Introduction
Introduction
Antoine Min´e Building a specialized static analyzer p. 5 / 112
Introduction Static analysis
Existing verification methods
Testing
well-established method
but no formal warranty, high cost
Antoine Min´e Building a specialized static analyzer p. 6 / 112
Introduction Static analysis
Existing verification methods
Testing
well-established method
but no formal warranty, high cost
Formal methods:
Theorem proving
proof essentially manual, but checked automatically
powerful, but very steep learning curve
Model checking
check a model of the program (usually user-specified, finite)
automatic and complete (wrt. model), but costly
Antoine Min´e Building a specialized static analyzer p. 6 / 112
Introduction Static analysis
Existing verification methods (cont.)
(Semantic-based) static analysis
works directly on the source code (not a model)
automatic, always terminating
sound (full control and data coverage)
incomplete (false alarms)
parameterized by one/several abstraction(s)
mostly used to check simple properties,
with low precision requirements (e.g., for optimisation)
Antoine Min´e Building a specialized static analyzer p. 7 / 112
Introduction Static analysis
Existing verification methods (cont.)
(Semantic-based) static analysis
works directly on the source code (not a model)
automatic, always terminating
sound (full control and data coverage)
incomplete (false alarms)
parameterized by one/several abstraction(s)
mostly used to check simple properties,
with low precision requirements (e.g., for optimisation)
Specialized static analyzer
checks for run-time errors (overflow, etc.)
is very precise at least on a chosen class of programs
(no false alarm)
gives sound results on all programs
Antoine Min´e Building a specialized static analyzer p. 7 / 112
Introduction Static analysis
Abstract interpretation
Abstract Interpretation
General theory of semantic approximations [Cousot Cousot 77,91]
D
−
D
]
(e.g. P(Zn)) (e.g. n-dim boxes)
Concrete domain Abstract domain
Elements in D]
represent properties of interest (semantical)
are computer-representable (algorithmic)
Choosing D] is a trade-off between cost and expressiveness
Antoine Min´e Building a specialized static analyzer p. 8 / 112
Introduction Static analysis
Abstract interpretation (cont.)
For each concrete semantic operator F : Dn ! D:
assignment,
test,
control-flow join, etc.
define F] : D]n ! D] that
can be implemented (algorithm)
is sound: F(
(X]
1), . . . ,
(X]
n))
(F](X]
1, . . . ,X]
n))
various precision / cost trade-offs
=) computable over-approximation
Antoine Min´e Building a specialized static analyzer p. 9 / 112
Introduction Static analysis
Construction by refinement
Approach
define a concrete semantics
build a simple and fast analyzer (intervals)
refine the analyzer until 0 false alarm:
determine which necessary properties are missed
add / refine an abstract domain to infer it
Benefits
sound by construction
efficient (adapted cost / precision trade-off)
encourages modular, reusable abstractions
Antoine Min´e Building a specialized static analyzer p. 10 / 112
Introduction First analyses
Analysis input and output
Astrée
− alarms
− invariants
(environment
configuration)
C sources
(preprocessed)
Antoine Min´e Building a specialized static analyzer p. 11 / 112
Introduction First analyses
Example analysis
loop.c
1 void main() {
2 unsigned i;
3 for (i=10; i>=0; i--) {
4 /* */
5 }
6 }
Starting the analysis
% astree loop.c --exec-fn main | egrep WARN
Antoine Min´e Building a specialized static analyzer p. 13 / 112
Introduction First analyses
Example analysis
loop.c
1 void main() {
2 unsigned i;
3 for (i=10; i>=0; i--) {
4 /* */
5 }
6 }
Analysis result
% astree loop.c --exec-fn main | egrep WARN
loop.c:3.19-22::[call#main@1:loop@4>=4:]: WARN:
unsigned int arithmetic range [-1, 4294967294]
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：航空资料41(91)
