Static Analysis Techniques Overview
EXERCISE #5
1
STATIC ANALYSIS REVIEW
Write your name and answer the following on a piece of paper
•
Show the
instruction flowchart
of the following function
void v(int a){ if (a < 2){ while (c < 3){ c++;
}
if (b > 3){c = 12;
}
}
return;
}
ADMINISTRIVIA
AND
ANNOUNCEMENTS
CONTROL FLOW GRAPHS
EECS 677: Software Security Evaluation
Drew Davidson
CLASS PROGRESS
OVERVIEWED TWO ANALYSIS
APPROACHES:
-
DYNAMIC ANALYSIS: ANALYSIS THAT
USES A RUN OF THE PROGRAM
-
STATIC ANALYSIS: ANALYSIS WITHOUT
RUNNING THE PROGRAM
4
CONTINUE TO EXPLORE STATIC ANALYSIS
5
CLASS PROGRESS
L
OOK
INTO
CONCRETE
FORMS
OF
S
TATIC
A
NALYSIS
-
Particularly interested in dataflow analysis
for now
-
Building up the underlying abstractions /
techniques to perform such analysis
OPPORTUNITIES OF STATIC ANALYSIS
6
CLASS PROGRESS
F
INITE
A
BSTRACTIONS
OF
U
NBOUNDED
S
TATE
S
PACE
-
Unnecessary to supply a given program
input
-
Summarize the behavior of the program
under ANY input
LAST TIME: STATIC ANALYSIS
7
REVIEW: STATIC ANALYSIS
M
ENTIONED
SOME
STATIC
ANALYSIS
T
ECHNIQUES
-
Syntactic Analysis
-
Dataflow Analysis
-
Model Checking
S
TARTED
B
UILDING
A
F
UNDAMENTAL
U
NIT
OF
S
TATIC
A
NALYSIS
:
THE
B
ASIC
B
LOCK
-
Sequence of code that executes… sequentially
8
BASIC BLOCKS BOUNDARIES
REVIEW: STATIC ANALYSIS
TWO DISTINGUISHED INSTRUCTIONS IN A BLOCK (MAY BE THE
SAME INSTRUCTION)
•
Leader: An instruction that begins the block
•
Terminator: An instruction that ends the block
9
BASIC BLOCKS BOUNDARIES
REVIEW: STATIC ANALYSIS
TWO DISTINGUISHED INSTRUCTIONS IN A BLOCK
(MAY BE THE SAME INSTRUCTION)
•
Leader: An instruction that begins the block
•
Terminator: An instruction that ends the block
A jump (ifz, goto)
The first instruction in the procedure
The target of a jump
The last instruction of the procedure
A call (We’ll use a special LINK edge)
The instruction after an terminator
BASIC BLOCKS EXAMPLE
10
STATIC ANALYSIS: CONTROL FLOW GRAPHS
y = 0;
if ( g ) {x = 1;
x = 2;
} else {x = 3;
if (g2) {x = y;
}
x = 4;
}
z = x;
BENEFITS OF BASIC BLOCKS
11
STATIC ANALYSIS: CONTROL FLOW GRAPHS
If-stmt
Loops
If-else
AN ADDITIONAL ABSTRACTION LAYER
•
Leader: An instruction that begins the block
CFGS: A PER-FUNCTION ABSTRACTION
12
STATIC ANALYSIS: CONTROL FLOW GRAPHS
BY DEFINITION, A CFG NEVER INCLUDES MULTIPLE FUNCTIONS
Call instruction simply has a special “link” edge to its successor
CFG-Like analysis is possible on multiple functions, but requires special care to
avoid infeasible paths
LECTURE OUTLINE
•
(Local) Dataflow analysis
•
Global dataflow analysis
DATAFLOW ANALYSIS: BIG IDEA
14
DATAFLOW ANALYSIS
V
IEW
E
ACH
S
TATEMENT
AS
A
D
ATA
T
RANSFER
F
UNCTION
-
Transform a program state into a new (updated) program state
-
Simple idea: concrete program state into a new concrete program state
Stmt
1
: x = y ;
y has the value 1
x has the value 1
y has the value 1
state M
state M’
COMPOSING TRANSFER FUNCTIONS
15
DATAFLOW ANALYSIS
S
TATEMENTS
C
OMPOSE
N
ATURALLY
WITH
EACH
OTHER
*
Stmt
1
: x = y ;
y has the value 1
x has the value 1
y has the value 1
z has the value 1
state M
state M’
Stmt
2
: z = x ;
For now, we’ll only think about
analysis within a BBL
AN EARLY WIN
16
DATAFLOW ANALYSIS
E
VEN
WITH
THIS
V
ERY
S
IMPLE
C
ONCEPT
,
MIGHT
BE
ABLE
TO
DETECT
SOME
ISSUES
Stmt
1
: x = y ;
y has the value 1
state M
Stmt
2
: z = 0 ;
Stmt
3
: p = 1 / z ;
FORMALIZING TRANSFER FUNCTIONS
17
DATAFLOW ANALYSIS
I
F
WE
WANT
TO
B
UILD
AN
A
UTOMATED
(L
OCAL
) D
ATAFLOW
ANALYSIS
,
WE
NEED
PROGRAMMATIC
P
RECISION
Stmt
1
: k += 1 ;
Memory state M
Memory state M’
-
Some sort of specification of what a statement does
-
A statement is a memory state transformer
Need a semantics!
Representation mapping (large)
set of memory states to each other
Depend somewhat on the analysis
-
Keep states manageable
-
Handle the uncertainty inherent in
static analysis
Goals:
MEMORY AS VALUE SETS
18
DATAFLOW ANALYSIS
L
ET
EACH
MEMORY
L
OCATION
CORRESPOND
TO
A
S
ET
OF
V
ALUES
IT
MIGHT
C
ONTAIN
Stmt
1
: k += 1 ;
Memory state M
Memory state M’
-
Define (informally) transfer functions as mapping
elements of M to elements of M’
We’re still kinda-dodging the
larger semantic questions here,
for now lets just say we’re using a
big ol’ if statement to define an operator
COMPOSING VALUE SETS
19
DATAFLOW ANALYSIS
Stmt
1
: x = y ;
Stmt
2
: z = 0 ;
Stmt
3
: p = 1 / z ;
MODELLING UNCERTAINTY
20
DATAFLOW ANALYSIS
W
E
CAN
NOW
HANDLE
OPAQUE
DATA
SOMEWHAT
CLEANLY
Stmt
1
: x = y ;
Stmt
2
: z = USER_INPUT ;
Stmt
3
: p = 1 / z ;
Stmt
1
: x = y ;
Stmt
2
: z = global ;
Stmt
3
: p = 1 / z ;
LECTURE OUTLINE
•
(Local) Dataflow analysis
•
Global dataflow analysis
COMPOSING BLOCKS
22
DATAFLOW: TRANSFER FUNCTIONS
V
ALUE
-S
ET
M
ODEL
OF
MEMORY
IMPLIES
AN
EASY
WAY
TO
EXTEND
BEYOND
L
OCAL
A
NALYSIS
01. int x = 2;
02. if ( g ){03.
x = x - 1;
04. if ( g2 ){05. x = x – 1;
06. }
07. }
08. return 1 / x;
COMPOSING BLOCKS
23
GLOBAL DATAFLOW ANALYSIS
V
ALUE
-S
ET
M
ODEL
OF
MEMORY
IMPLIES
AN
EASY
WAY
TO
EXTEND
BEYOND
L
OCAL
A
NALYSIS
01. int x = 2;
02. if ( g ){03.
x = x - 1;
04. if ( g2 ){05. x = x – 1;
06. }
07. }
08. return 1 / x;
CHAOTIC ITERATION
24
GLOBAL DATAFLOW ANALYSIS
I
N
WHAT
ORDER
DO
WE
PROCESS
BLOCKS
?
01. int x = 2;
02. if ( g ){03.
x = x - 1;
04. if ( g2 ){05. x = x – 1;
06. }
07. }
08. return 1 / x;
01. int x = 2;
02. if ( g ){03. x = x – 1;
04. if ( g2 ){05. x = x -1;
06. }
07. }
08. return 1 / x;
TROUBLE ON THE HORIZON
25
GLOBAL DATAFLOW ANALYSIS
Loops
LOOPS ARE TOUGH TO HANDLE!
26
GLOBAL DATAFLOW ANALYSIS
I
SSUES
WITH
L
OOPS
-
Generate lots of paths
-
Cyclic data dependency
Oh, brother! You may have some loops
LECTURE END!
•
Local Dataflow analysis
•
Global Dataflow analysis
Explore static analysis techniques such as syntactic analysis, dataflow analysis, and model checking. Understand the concept of basic blocks in static analysis and their boundaries. Dive into the opportunities provided by static analysis in summarizing program behavior without executing it.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
EXERCISE #5 STATIC ANALYSIS REVIEW Write your name and answer the following on a piece of paper Show the instruction flowchart of the following function void v(int a){ if (a < 2){ while (c < 3){ c++; } if (b > 3){ c = 12; } } return; } 1
ADMINISTRIVIA AND ANNOUNCEMENTS
CONTROL FLOW GRAPHS EECS 677: Software Security Evaluation Drew Davidson
4 CLASS PROGRESS OVERVIEWED TWO ANALYSIS APPROACHES: - DYNAMIC ANALYSIS: ANALYSIS THAT USES A RUN OF THE PROGRAM - STATIC ANALYSIS: ANALYSIS WITHOUT RUNNING THE PROGRAM
5 CONTINUE TO EXPLORE STATIC ANALYSIS CLASS PROGRESS LOOKINTOCONCRETEFORMSOF STATIC ANALYSIS - Particularly interested in dataflow analysis for now - Building up the underlying abstractions / techniques to perform such analysis
6 OPPORTUNITIES OF STATIC ANALYSIS CLASS PROGRESS FINITE ABSTRACTIONSOF UNBOUNDED STATE SPACE - Unnecessary to supply a given program input - Summarize the behavior of the program under ANY input
7 LAST TIME: STATIC ANALYSIS REVIEW: STATIC ANALYSIS MENTIONEDSOMESTATICANALYSIS TECHNIQUES - Syntactic Analysis - Dataflow Analysis - Model Checking STARTED BUILDINGA FUNDAMENTAL UNITOF STATIC ANALYSIS: THE BASIC BLOCK - Sequence of code that executes sequentially
8 BASIC BLOCKS BOUNDARIES REVIEW: STATIC ANALYSIS TWO DISTINGUISHED INSTRUCTIONS IN A BLOCK (MAY BE THE SAME INSTRUCTION) Leader: An instruction that begins the block Terminator: An instruction that ends the block
9 BASIC BLOCKS BOUNDARIES REVIEW: STATIC ANALYSIS TWO DISTINGUISHED INSTRUCTIONS IN A BLOCK (MAY BE THE SAME INSTRUCTION) Leader: An instruction that begins the block The first instruction in the procedure The target of a jump The instruction after an terminator Terminator: An instruction that ends the block The last instruction of the procedure A jump (ifz, goto) A call (We ll use a special LINK edge)
10 BASIC BLOCKS EXAMPLE STATIC ANALYSIS: CONTROL FLOW GRAPHS y = 0; if ( g ) { x = 1; x = 2; } else { x = 3; if (g2) { x = y; } x = 4; } z = x;
11 BENEFITS OF BASIC BLOCKS STATIC ANALYSIS: CONTROL FLOW GRAPHS AN ADDITIONAL ABSTRACTION LAYER Leader: An instruction that begins the block Loops If-stmt If-else (head) (head) (head) T T T F (True branch) (True branch) F F (body) (False branch) (after) (after) (after)
12 CFGS: A PER-FUNCTION ABSTRACTION STATIC ANALYSIS: CONTROL FLOW GRAPHS BY DEFINITION, A CFG NEVER INCLUDES MULTIPLE FUNCTIONS Call instruction simply has a special link edge to its successor CFG-Like analysis is possible on multiple functions, but requires special care to avoid infeasible paths
LECTURE OUTLINE (Local) Dataflow analysis Global dataflow analysis
14 DATAFLOW ANALYSIS: BIG IDEA DATAFLOW ANALYSIS VIEW EACH STATEMENTASA DATA TRANSFER FUNCTION - Transform a program state into a new (updated) program state - Simple idea: concrete program state into a new concrete program state state M y has the value 1 Stmt1: x = y ; state M x has the value 1 y has the value 1
15 COMPOSING TRANSFER FUNCTIONS DATAFLOW ANALYSIS STATEMENTS COMPOSE NATURALLYWITHEACHOTHER* state M y has the value 1 Stmt1: x = y ; Stmt2: z = x ; For now, we ll only think about analysis within a BBL state M x has the value 1 y has the value 1 z has the value 1
16 AN EARLY WIN DATAFLOW ANALYSIS EVENWITHTHIS VERY SIMPLE CONCEPT, MIGHTBEABLE TODETECTSOMEISSUES state M y has the value 1 Stmt1: x = y ; Stmt2: z = 0 ; Stmt3: p = 1 / z ;
17 FORMALIZING TRANSFER FUNCTIONS DATAFLOW ANALYSIS IFWEWANTTO BUILDAN AUTOMATED (LOCAL) DATAFLOWANALYSIS, WENEED PROGRAMMATIC PRECISION Need a semantics! Representation mapping (large) set of memory states to each other - Some sort of specification of what a statement does - A statement is a memory state transformer Memory state M Depend somewhat on the analysis Goals: Stmt1: k += 1 ; Memory state M - Keep states manageable - Handle the uncertainty inherent in static analysis
18 MEMORY AS VALUE SETS DATAFLOW ANALYSIS LETEACHMEMORY LOCATIONCORRESPONDTO A SETOF VALUESITMIGHT CONTAIN - Define (informally) transfer functions as mapping elements of M to elements of M ?:{3,4} Memory state M ?:{1} Stmt1: k += 1 ; Memory state M ?:{4,5} ?:{2}
19 COMPOSING VALUE SETS DATAFLOW ANALYSIS Stmt1: x = y ; Stmt2: z = 0 ; Stmt3: p = 1 / z ;
20 MODELLING UNCERTAINTY DATAFLOW ANALYSIS WECANNOWHANDLEOPAQUEDATASOMEWHATCLEANLY Stmt1: x = y ; Stmt1: x = y ; Stmt2: z = USER_INPUT ; Stmt2: z = global ; Stmt3: p = 1 / z ; Stmt3: p = 1 / z ;
LECTURE OUTLINE (Local) Dataflow analysis Global dataflow analysis
22 COMPOSING BLOCKS DATAFLOW: TRANSFER FUNCTIONS VALUE-SET MODELOFMEMORYIMPLIESANEASYWAYTO EXTENDBEYOND LOCAL ANALYSIS 01. int x = 2; 02. if ( g ){ 03. x = x - 1; 04. if ( g2 ){ 05. x = x 1; 06. } 07. } 08. return 1 / x;
23 COMPOSING BLOCKS GLOBAL DATAFLOW ANALYSIS VALUE-SET MODELOFMEMORYIMPLIESANEASYWAYTO EXTENDBEYOND LOCAL ANALYSIS 01. int x = 2; 02. if ( g ){ 03. x = x - 1; 04. if ( g2 ){ 05. x = x 1; 06. } 07. } 08. return 1 / x;
24 CHAOTIC ITERATION GLOBAL DATAFLOW ANALYSIS 01. int x = 2; 02. if ( g ){ INWHATORDERDOWEPROCESSBLOCKS? 03. x = x 1; 04. if ( g2 ){ 01. int x = 2; 02. if ( g ){ 03. x = x - 1; 04. if ( g2 ){ 05. x = x 1; 06. } 07. } 08. return 1 / x; 05. x = x -1; 06. } 07. } 08. return 1 / x;
25 TROUBLE ON THE HORIZON GLOBAL DATAFLOW ANALYSIS Loops
26 LOOPS ARE TOUGH TO HANDLE! GLOBAL DATAFLOW ANALYSIS ISSUESWITH LOOPS - Generate lots of paths - Cyclic data dependency Oh, brother! You may have some loops
LECTURE END! Local Dataflow analysis Global Dataflow analysis
