Information Flow Control for Java: A Comprehensive Approach Based on Path Conditions in Dependence Graphs

List of Algorithms......Page 21
List of Figures......Page 23
List of Tables......Page 27
Introduction......Page 29
Principles of Program Analysis......Page 30
Dimensions of Program Analysis......Page 31
Contributions......Page 32
Dependence Graphs and Slicing for Object-Oriented Languages......Page 35
Intraprocedural Dataflow Analysis......Page 36
Monotone Dataflow Analysis Framework......Page 37
Reaching Definitions......Page 39
Program Slicing......Page 40
Slicing in the PDG......Page 42
Interprocedural Analysis......Page 45
Points-To Analysis......Page 50
Inclusion-Based vs. Unification-Based Analysis......Page 52
Inter-procedural Analysis and Dynamic Dispatch......Page 53
Aliasing......Page 54
Exception Handling......Page 56
Objects and Fields......Page 58
Interprocedural Dataflow-Analysis......Page 60
Intraprocedural IRef and IMod Computation......Page 61
Interprocedural Analysis......Page 65
Data Dependences......Page 67
Correctness of Object Tree Algorithm......Page 69
Related Work......Page 73
The New Java Memory Model......Page 79
Slicing Concurrent Java......Page 82
Undecidability of Slicing......Page 83
Dynamic Thread Creation......Page 84
Interference Dependence......Page 90
Other Concurrency-Related Dependences......Page 91
Slicing the cSDG......Page 92
Time Travel......Page 94
Slicers Disallowing Time Travel......Page 95
Related Work......Page 97
Computer Security......Page 99
Channels and Information Flow......Page 100
Information Flow Control......Page 101
Language-Based Information Flow Control......Page 102
Dependence Graphs for Information Flow Control......Page 104
Dependence Graphs and Noninterference......Page 105
Examples for Slicing-based IFC......Page 106
Exceptions......Page 107
Context-Sensitivity and Object-Sensitivity in Action......Page 108
Analyzing Information Flow......Page 110
Fundamental Flow equations......Page 111
Solving Flow equations......Page 113
The PDG-Based Noninterference Test......Page 114
Context-Sensitive Slicing......Page 116
Backward Flow Equations......Page 121
Declassification in SDGs......Page 122
Monotonicity of Release......Page 124
Confidentiality check with declassification......Page 125
Summary Declassification Nodes......Page 126
Computation of R(d) for Summary Declassification Nodes......Page 128
Beyond PDGs......Page 131
Security type systems......Page 132
Verification and IFC......Page 133
Static analysis for security......Page 134
Introduction......Page 135
Intraprocedural Path Conditions......Page 136
Interprocedural Path Conditions......Page 139
Dynamic Type Tests......Page 141
Path Conditions for instanceof......Page 143
Dynamic Dispatch......Page 145
Exceptions......Page 148
Concurrency......Page 150
Dynamic Path Conditions in Dependence Graphs......Page 151
Program Tracing......Page 152
Dynamic Slicing......Page 154
Dynamic Path Conditions......Page 157
Related Work......Page 160
Frontends......Page 163
Stubs......Page 165
Graph Viewer......Page 166
Path Conditions......Page 167
Plugins for Information Flow Control......Page 169
Slicing Java Programs......Page 173
Evaluating Interference Dependence......Page 175
Information Flow Control......Page 177
JIF......Page 178
Slicing-Based Information Flow Control......Page 181
Flow-, Context- and Object-Sensitivity......Page 182
Case Studies......Page 183
Scalability......Page 187
Case Studies for Path Conditions......Page 191
Static Path Conditions for Java......Page 193
Dynamic Path Conditions for C......Page 195
Conclusion......Page 203
Appendix......Page 205
Bibliography......Page 209
Index......Page 229