STATIC VERIFICATION AND DYNAMIC ANALYSIS FRAMEWORK FOR INFORMATION FLOW CONTROL

Abstract

In this thesis, we explore both static and dynamic information flow control (IFC) system. In particular, we show that static IFC need not rely on type-based system but can be modelled as a logic-driven fashion using Hoare-like logic. We then show how this system can be improved to by separating explicit and implicit influence to increase path-sensitivity. Both out security-aware and path-sensitive security-aware systems are sound and correct with respect to non-interference. Our dynamic IFC supports higher-order functions and dynamic evaluation of code similar to JavaScript ‘eval’ without the need for higher-order Hoare-logic or string analyser by implementing a dynamic inline monitor. Finally, we evaluate our systems using manually verified micro-benchmarks to increase confidence in our implementation.