Static Analysis of Non-interference in Expressive Low-Level Languages

4 years 10 months ago
Static Analysis of Non-interference in Expressive Low-Level Languages
Early work in implicit information flow detection applied only to flat, procedureless languages with structured control-flow (e.g., if statements, while loops). These techniques have yet to be adequately extended and generalized to expressive languages with interprocedural, exceptional and irregular control-flow behavior. We present an implicit information flow analysis suitable for languages with conditional jumps, dynamically dispatched methods, and exceptions. We implement this analysis for the Dalvik bytecode format, the substrate for Android. In order to capture information flows across interprocedural and exceptional boundaries, this analysis uses a projection of a small-step abstract interpreter’s rich state graph instead of the control-flow graph typically used for such purposes in weaker linguistic settings. We present a proof of termination-insensitive non-interference. To our knowledge, it is the first analysis capable of proving non-trivial non-interference in a l...
Peter Aldous, Matthew Might
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where SAS
Authors Peter Aldous, Matthew Might
Comments (0)