CDroid: practically implementation a formal-analyzed CIFC model on Android

Decentralized information flow control (DIFC) operating systems provide mechanisms for applications to handle the secrecy and integrity of their data by themselves. DIFC adapts to the distributed systems well, but not for the centralized authorization systems where an administrator manages all the privileges. For example, Android is full of untrusted third-party applications. A phone user may want to specify what kind of application can deal with what kind of private data by enforcing information flow control. To address this, we proposed a novel formal-described and security-proofed centralized information flow control (CIFC) model. In CIFC, taint tag of private data and capability label of applications are designed to support fine-grained and user-defined information flow control. Differs from DIFC and classic information flow control models, CIFC model controls information flow according to the relation between tag and label rather than the relation between two labels of applications. We use Value-passing Security Process Algebra (VSPA) to clarify the formal semantics of CIFC model. The verification of system equivalence proves that the model guarantees the noninterference security property in virtue of Checker of Persistent Security (CoPS) tool. We also implemented CDroid, a prototype of the CIFC model which can track and control information flow at runtime. CDroid is demonstrated to be an accurate system to achieve the security goal through several function test experiments. Furthermore, CDroid has 5% lead in memory consumption and 17% overhead of runtime performance compared to Android.