A permission-dependent type system for secure information flow analysis
Date
2018
Authors
Chen, Hongxu
Tiu, Alwen
Xu, Zhiwu
Liu, Yang
Journal Title
Journal ISSN
Volume Title
Publisher
IEEE
Abstract
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 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 non-interference. 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.
Description
Keywords
Citation
Collections
Source
Proceedings - IEEE Computer Security Foundations Symposium
Type
Conference paper
Book Title
Entity type
Access Statement
License Rights
Restricted until
2099-12-31