A Logical System For Modular Information Flow Verification

Information Flow Control (IFC) is important to ensure secure programs where secret data does not influence any public data. The pervasive standard that IFC aims to is non-interference. Current IFC systems are separated into dynamic IFC, static IFC, and hybrids between static and dynamic. With dynamic IFC suffering from high overhead and limited ability to prevent implicit flows due to the paths not taken, we propose a novel modular static IFC system. To the best of our knowledge, this is the first modular static IFC system. Unlike type-based static IFC systems, ours is logic-based. The limitation of type-based IFC systems is in the inviolability of static security label declarations for fields. As such, they suffer from transient leaks on fields. Our proposed system uses a Hoare-like logic. It verifies each function independently with the help of separation logic. Furthermore, we provide the proof of correctness for our novel IFC system with respect to termination- and timing-insensitive non-interference.