Static Verification and Dynamic Analysis Framework for Information Flow Control
COM2 Level 4
Executive Classroom, COM2-04-02
Abstract:
In this thesis, we explore both static IFC for a C-like language and dynamic IFC for JavaScript-like language. In particular, we show that static IFC need not rely on type-based static IFC systems but can be modeled as a logic-driven fashion. Our proposed system uses Hoare-like logic, verifies information flow safety using inductive predicates for recursive data structures.
We show that the system is sound and correct with respect to the non-interference property. We term this a "Security-Aware IFC System". We augment the system to improve path-sensitivity by separating explicit and implicit influence. Our proposed improvements are based on the observation that implicit influence cannot be path-sensitive while explicit influence can. In particular, we develop a path-sensitive security-aware IFC system and show the soundness and correctness of the system with respect to the non-interference property.
In addition, we consider a dynamic language that mimics the JavaScript language. This dynamic language supports higher-order functions and the dynamic evaluation of code (in the manner of JavaScript 'eva'). To accommodate higher-order functions and the dynamic evaluation of code, static IFC systems require higher-order Hoare-logic and string analyzer respectively. However, any theory of string that allows string-replace operation but without straight-line restriction on the formulas is undecidable. As such, we implement dynamic inline monitor for this dynamic language. Dynamic inline monitor avoids the need for string analyzer as the input to dynamic evaluation of code can be known at run-time.
Finally, we implement our system and evaluate it using our microbenchmarks. We manually verify our micro-benchmarks to ensure correctness. Our micro-benchmarks show that improving path-sensitivity allows us to verify more safe programs with only minor slowdowns in verification time.