I report on applications of slicing and program dependence graphs (PDGs) to software security. Moreover, I propose a framework that generalizes both data-flow analysis on control-flow graphs and slicing on PDGs. This framework can be used to systematically derive data-flow-like analyses on PDGs that go beyond slicing. I demonstrate that data-flow analysis can be systematically applied to PDGs and show the practicability of my approach.
Author(s): Martin Mohr
Publisher: Scientific Publishing
Year: 2023
Language: English
Pages: 464
Danksagung
Acknowledgments
Zusammenfassung
Abstract
1 Introduction
1.1 Applications to Software Security
1.2 Systematic Approaches to Advanced Information Flow Analysis
1.3 Main Theses and Contributions
1.4 Organization of This Thesis
2 Foundations
2.1 Sets and Relations
2.2 Complete Lattices, Fixed Point Theory Theory and Monotone Constraint Systems
2.2.1 Partial Orders and Fixed-Points
2.2.2 Monotone Constraint Systems
2.2.3 Solving Monotone Constraint Systems
2.3 Inductive Definitions
2.4 Symbol Sequences
2.5 Directed Graphs
3 Program Dependence Graphs for Object-Oriented Programs
3.1 Principles of Static Program Analysis
3.2 Data-Flow Analysis on Control-Flow Graphs
3.2.1 Control-Flow Graphs
3.2.2 Data-Flow Analysis
3.3 Slicing on Program Dependence Graphs
3.3.1 Slicing
3.3.2 Program Dependence Graphs
3.3.3 PDG-based Slicing
3.3.4 Relation of PDG-based Slicing and Data-Flow Analysis
3.4 Joana: PDG-based Information Flow Control for Java
3.4.1 Slicing and Information Flow Control
3.4.2 Dynamic Dispatch
3.4.3 Exceptions
3.4.4 Objects
4 Applications of Joana to Software Security
4.1 General Description and Motivation of RS3
4.2 The Sub-Project "Information Flow Control for Mobile Components"
4.2.1 Information Flow Properties for Concurrent Programs
4.2.2 Modeling and Analyzing Concurrency in Program Dependence Graphs
4.3 Reference Scenario "Security in E-Voting"
4.3.1 Motivation
4.3.2 CVJ Framework
4.3.3 The Hybrid Approach
4.3.4 Case Study: E-Voting Machine
4.3.5 Spec Slicing
4.4 Reference Scenario "Software Security for Mobile Devices"
4.4.1 Motivation
4.4.2 The RS3 Certifying App Store
4.4.3 Jodroid: Joana for Android
4.5 RIFL
4.5.1 Description of RIFL
4.5.2 Joana's Support for RIFL
4.6 ifspec: An Information-Flow Security Benchmark Suite
4.7 SHRIFT– System-Wide HybRid Information Flow Tracking
4.7.1 Background and Motivation
4.7.2 Approach
4.7.3 Results
4.8 Modular Verification of Information Flow Security in Component-Based Systems
4.9 Summary and Conclusion
5 A Common Generalization Of Program Dependence Graphs and Control-Flow Graphs
5.1 Nesting Properties of Symbol Sequences
5.1.1 Balanced Sequences
5.1.2 Partially-Balanced Sequences
5.1.3 Valid Sequences
5.1.4 Inductive Definitions
5.2 Interprocedural Graphs
5.3 Data-Flow Analysis on Interprocedural Graphs
5.4 Example Instances
5.4.1 Traditional Data-Flow Analyses on Interprocedural Control-Flow Graphs
5.4.2 Slicing
5.4.3 Chopping
5.4.4 Strong Bridges and Strong Articulation Points
5.4.5 Restricting to Paths With Regular Properties
5.4.6 Hammer's Approach to IFC
5.4.7 Least Distances
6 Two Approaches to Abstract Data-Flow Analysis on Interprocedural Graphs
6.1 Preliminaries
6.1.1 Syntax and Semantics
6.1.2 Correctness and Precision of Solutions
6.2 The Functional Approach
6.2.1 Constraint Systems
6.2.2 Correctness and Precision
6.3 The Call-String Approach
6.3.1 Stack Spaces
6.3.2 The Unbounded Stack Space
6.3.3 Stack Abstractions
6.3.4 Effective and Correct Approximations of the Unbounded Call-String Approach
7 A Common Generalization of Interprocedural Data-Flow Analysis and Slicing
7.1 Integrating Reachability Into the Solution Process
7.2 Integration of Interprocedural Slicing and Interprocedural Data-Flow Analysis
7.3 Functional Approach
7.3.1 Computing the Same-Level Solution
7.3.2 Computing the Ascending Solution
7.3.3 Extending the Solution Along the Non-Ascending Paths
7.3.4 Combining the Ascending Solution and the Non-Ascending Solution
7.3.5 Putting It All Together
7.3.6 Towards the Two-Phase Slicer
7.4 Call-String Approach
8 Implementation and Evaluation
8.1 Notes on the Implementation
8.1.1 Functional Approach
8.1.2 Call-string Approach
8.1.3 Complexity Considerations
8.2 Description of the Setup
8.2.1 Evaluation Environment
8.2.2 Samples
8.2.3 Instances
8.3 Performance Evaluation
8.3.1 Same-Level Problem Solvers
8.3.2 Data-Flow Solvers
8.4 Precision Evaluation
8.4.1 How to Measure the Precision of Data-Flow Analyses
8.4.2 Results
8.4.3 Discussion
9 Discussion and Related Work
9.1 The Role of Data-Flow Analysis and Slicing in Program Analysis
9.2 Simplification and Restrictions
9.2.1 Forward Analysis vs. Backward Analysis
9.2.2 Functional Level vs. Ordinary Level and Initial Values
9.2.3 Concurrency
9.2.4 Semantics
9.3 Benefits and Possible Improvements of My Approach
9.3.1 Applicability of Existing Extensions and Improvements
9.3.2 Benefits of My Framework Compared to Adhoc Approaches
9.4 Alternative Approaches to Generalize Slicing
9.4.1 Pushdown Systems
9.4.2 Recursive State Machines
9.4.3 Visibly Push-Down Languages
10 Conclusion
10.1 Summary and Main Theses
10.1.1 Applications to Software Security
10.1.2 Systematic Approaches to Advanced Information Flow Analysis
10.2 Future Work
10.2.1 Approximation of Same-Level Information
10.2.2 Further Exploration of Stack Spaces and MOVP-Correct Abstractions
10.2.3 Relation Between the Results of Data-Flow Analysis on PDGs and Program Semantics
10.2.4 Generalization of Chopping
10.2.5 Extensions to Concurrent Programs
10.2.6 Exploration of Other Generalizations of Context-Sensitive Slicing
Bibliography
A Proofs
A.1 Proof of Theorem 5.9
A.2 Proof of Theorem 5.10
A.3 Proof of Theorem 5.19
A.4 Proof of Theorem 5.20
A.5 Proof of Theorem 5.21
A.6 Proof of Lemma 5.24
A.7 Proof of Lemma 5.25
A.8 Proof of Lemma 5.26
B List of Figures
C List of Tables
D List of Listings
E List of Algorithms
