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