用于安全信息流分析的权限依赖类型系统
编程语言
2017-09-28 v1 密码学与安全
摘要
我们引入了一种新颖的类型系统，用于在命令式语言中实施安全信息流。我们的工作动机是静态检查 Android 应用程序中潜在信息泄漏的问题。为此，我们设计了一个以 Android 权限模型为特征的轻量级类型系统，其中权限被静态分配给应用程序，并用于在应用程序中实施访问控制。我们从 Banerjee 和 Naumann (BN) 的类型系统中汲取灵感，允许安全类型依赖于应用程序的权限。我们类型系统的一个新颖特征是由权限测试引起的条件分支的定型规则，它在安全类型上引入了一个合并算子，允许实施更精确的安全策略。我们针对非干扰的概念证明了类型系统的可靠性。此外，通过将推理问题归约为安全类型格中的约束求解问题，我们为底层安全类型系统提出了一个类型推断算法。
引用
@article{arxiv.1709.09623,
title = {A Permission-Dependent Type System for Secure Information Flow Analysis},
author = {Hongxu Chen and Alwen Tiu and Zhiwu Xu and Yang Liu},
journal= {arXiv preprint arXiv:1709.09623},
year = {2017}
}
备注
48 pages