de
en
Schliessen
Detailsuche
Bibliotheken
Projekt
Impressum
Datenschutz
Schliessen
Publizieren
Besondere Sammlungen
Digitalisierungsservice
Hilfe
Impressum
Datenschutz
zum Inhalt
Detailsuche
Schnellsuche:
OK
Ergebnisliste
Titel
Titel
Inhalt
Inhalt
Seite
Seite
Im Werk suchen
Validation of data flow results for program modules / Karsten Klohs. 2009
Inhalt
1 Introduction
1.1 Methodical Contributions
1.2 Limitations
1.3 Road Map
2 Application Scenarios
2.1 Security Policies and Mobile Code
2.2 Program Optimisation and Partial Analyses
2.3 Modular Results and Partial Analysis
2.4 Validation of Data Flow Results as an Assisting Technique
3 Foundations
3.1 Iterative Data Flow Analysis and Equation Systems
3.1.1 Elements of Data Flow Problems
3.1.2 The Flow Graph Model and Equation Systems
3.1.3 The Iterative Worklist Algorithm
3.1.4 Elimination Methods
3.1.5 Advanced Scenarios of Program Analysis
3.2 Model Checking and Abstract Interpretations
3.2.1 Model Checking and the Relationship to Program Analysis
3.2.2 Validation of Program Analysis Results
4 Fundamental Validation Principles
4.1 Intraprocedural Validation
4.1.1 The General Validation Principle
4.1.2 The Intentional Under-Approximation Principle
4.2 Interprocedural Validation
4.2.1 Review of Interprocedural Analysis
4.2.2 Validation of Summary Functions
4.2.3 Validation of Data Flow Values
4.2.4 Method Invocation Semantics
4.2.5 The Interprocedural Validation Principle
4.3 Program Modules and Sophisticated Validation Scenarios
4.3.1 The Safe Lower Bound Principle
4.3.2 Incremental Validation
4.3.3 Partial Validation
4.4 Summary and Comparison
5 A Generic Model for Summary Functions
5.1 Summary Function Definition
5.1.1 Summary Functions and Data Flow Expressions
5.1.2 Function Operations
5.1.3 Specification of Instruction-Level Summary Functions
5.1.4 Relationship to IDFS-problems
5.2 Function Application Expressions and Elementary Transfer Functions
5.2.1 Properties of Function Application Expressions
5.2.2 Nesting Depth and Fix-Point Properties
5.2.3 Relationship to IDE-problems
5.3 Normalisation and Properties of Summary Functions
5.3.1 Normalisation of Data Flow Expressions
5.3.2 Properties of Data Flow Expressions
5.3.3 Properties of the Summary Function Model
5.3.4 Summary Functions and the Inducing Data Flow Problem
5.4 Modular Results and Incremental Validation
5.4.1 Invocation Contexts and Data Flow Variables
5.4.2 External Callees and Function Variables
5.4.3 Intraprocedural Analysis is an Application of the Safe Lower Bound Principle
5.4.4 Open Summary Functions and the Incremental Validation Scenario
5.4.5 Properties of Open Summary Functions
5.4.6 Function Variables in the Expression Model
5.5 Method Invocation and Parameter Passing
5.5.1 Local Variables, Parameters, and Global Variables
5.5.2 Parameter Passing and the Call-Function
5.5.3 Method Return
5.5.4 Properties of Call- and Return-Function
5.5.5 Related Approaches
5.6 Summary and Comparison
5.6.1 Capabilities of the Summary Function Model
5.6.2 Limitations of the Summary Function Model
6 Optimisation of the Validation Process
6.1 Reduction of the Certificate
6.1.1 The KVM Approach
6.1.2 The Difference Certificate Approach
6.2 Lifetime of Data Flow Facts in the Validation Process
6.2.1 Dependency Model
6.2.2 Reuse and Check
6.2.3 Optimisation Goals
6.3 Safe Lower Bounds
6.3.1 Lattice Strength Reduction
6.3.2 Intentional Under-Approximation and Demand-Driven Analysis
6.4 Reinterpretation in the Interprocedural Scenario
6.4.1 Dependencies in the Interprocedural Result
6.4.2 Difference Certificates
6.4.3 Intermediate Results
6.4.4 Modular Results and the Dependence Graph
6.5 Summary and Related Work
7 Validatable Program Analyses
7.1 Bit-Vector Analyses and the Power-Set Lattice
7.1.1 Separable Bit-Vector Analyses: Reaching Definitions
7.1.2 Non-Separable Bit-Vector Analyses: Faint Variables
7.2 Constant Propagation
7.2.1 Arbitrary Lattices: Copy Constant Propagation
7.2.2 Elementary Functions: Linear Constant Propagation
7.3 Object Oriented Aspects: Type Inference and Call Graph Construction
7.3.1 Data Flow Based Type Inference
7.3.2 Type Inference and Flow Graph Construction
7.3.3 Validation of Interprocedural Flow Graphs
7.3.4 Type Inference for Software Modules
7.3.5 Summary and Comparison to Existing Algorithms
8 LUPUS - A Framework for Validatable Data Flow Analysis
8.1 System Overview
8.2 Implementation of Data Flow Problems
8.2.1 Elements of a Data Flow Problem
8.2.2 Specification of a Concrete Analysis
8.2.3 Flow Graphs and Program Points
8.2.4 Data Flow Values, Data Flow Expressions and Environments
8.2.5 Summary Function Implementation
8.3 The Program Analysis Framework
8.3.1 Intraprocedural Analysis
8.3.2 Interprocedural Analysis
8.3.3 Solution Analysis and Preparation of the Certificate
8.4 LUPULUS - An Efficient and Flexible Validator
8.4.1 Reusable Infrastructure
8.4.2 Complete Result Validator
8.5 Summary and Comparison to Existing Frameworks
8.5.1 SOOT and INDUS
8.5.2 PAG
8.5.3 SafeTSA
8.5.4 Code Surfer
8.5.5 Abstraction Carrying Code
9 Evaluation
9.1 Evaluation Setting
9.1.1 Evaluated Analysis
9.1.2 Analysed Software
9.2 Evaluation of the Analysis Phase
9.2.1 Intraprocedural Summary Computation
9.2.2 Interprocedural Summary Computation
9.2.3 Invocation Context Computation
9.3 Size of the Certificate
9.3.1 Interprocedural Summary Functions
9.3.2 Size of the Program State
9.4 Evaluation of the Validation Phase
9.4.1 Memory Requirements
9.4.2 Runtime Requirements
9.5 Summary
10 Conclusion
10.1 Contributions
10.2 Future Directions
A Proofs
B Bibliography
Die detaillierte Suchanfrage erfordert aktiviertes Javascript.