A Permission-Dependent Type System for Secure Information Flow Analysis
This work addresses secure information flow for Android application developers, offering a lightweight and incremental improvement over existing type systems.
The authors tackled the problem of statically checking information leakage in Android applications by introducing a novel type system that incorporates the Android permission model, proving its soundness with respect to noninterference and providing a type inference algorithm.
We introduce a novel type system for enforcing secure information flow in an imperative language. Our work is motivated by the problem of statically checking potential information leakage in Android applications. To this end, we design a lightweight type system featuring Android permission model, where the permissions are statically assigned to applications and are used to enforce access control in the applications. We take inspiration from a type system by Banerjee and Naumann (BN) to allow security types to be dependent on the permissions of the applications. A novel feature of our type system is a typing rule for conditional branching induced by permission testing, which introduces a merging operator on security types, allowing more precise security policies to be enforced. The soundness of our type system is proved with respect to a notion of noninterference. In addition, a type inference algorithm is presented for the underlying security type system, by reducing the inference problem to a constraint solving problem in the lattice of security types.