作者 | 陈泓旭
整理 | 编程语言 Lab
陈泓旭 华为可信实验室高级工程师，南洋理工大学博士。研究领域是程序分析、软件安全、编程理论等。
视频回顾：
Android 权限的一个类型系统模型

---

本文主要和大家分享一下我读博期间做的和类型系统相关一篇文章，发表在 CSF 2018 上的工作 (https://ieeexplore.ieee.org/document/8429307)，合作者包括深圳大学的许智武老师，以及我当时的两位导师 Alwen Tiu 和 Yang Liu。这个工作主要是利用类型系统来静态检查 Android 系统上可疑的信息泄露，它的一个主要优势是我们可以对独立的 Android app 进行类型检查以确认它没有带来任何可能导致信息泄露的安全隐患。
原文的标题是 “A Permission-Dependent Type System for Secure Information Flow Analysis” ，首先简单解释一下。

1. 我们分析的是信息流问题：即在一个系统里信息从一个变量传递到另一个变量的安全性。最典型的是信息泄露问题：一个高机密性的变量 (可标识为 $H$)，被错误地赋值给一个低机密性的变量 (可标识为 $L$)，导致攻击者可以通过观察机密性低的变量内容而了解到高机密的信息。
2. 这里的类型 (Type) 和编程语言使用的结构类型 (structural type) 不一样：结构类型是通常意义下我们使用的类似 int,String,Object 这样的类型；而我们这里讨论的是和这些类型独立并存的另一套体系，它用于标识变量 (数据) 的机密性等级。区别于结构类型，它一般被称为安全类型(security type)。
3. 这里定义的类型是依赖于权限 (permission-dependent) 的。从类型系统理论来看，这对应的是结构类型中的依赖类型(dependent type，类型由 term 来决定）。需要说明的是，安全类型系统可以不考虑权限；但如果没有它那么类型系统的实用性会降低。在我们分析的 Android 信息流模型里，考虑权限对判断是否存在信息泄露至关重要。

Pokémon GO的一个小例子

我们先来看一下 Android apps 信息流安全的具体场景。

这是一个叫 Pokémon GO 的一个 Android 应用，在 2017 年左右是一个比较火的游戏，能对现实世界中出现的宝可梦进行探索捕捉、战斗以及交换。基于这款游戏的特征，它可以获取用户的联系人信息、和手机的位置信息，它可以使用手机的拍照功能，它可以向 Twitter, LINE 等 app 传送数据，它可以向互联网发送一些信息，同时它还可以从存储卡中读取或写入相关信息。这些信息有很多是敏感的，比如用户联系人信息，如果被其他 app 所获取或被上传到网络上，会严重侵犯用户的隐私。因此，需要有一种机制来保护敏感的信息不被泄露。Android 是通过 manifst 文件中指定 app 所需要的权限，在执行时我们检查当前 app 是否已经拥有该权限。

信息流安全的一点理论

为了讨论如何利用安全类型系统来解决 Android 的信息流问题，我们先看一下一些相关理论。

我们一般给变量加下标来表征变量的机密性等级。不同的机密性等级在偏序关系 ($<$) 之下形成数学意义上的格 (lattice)。为方便描述，我们使用仅包含 $H,L$ 两个元素且 $L<H$ 的格来简化我们的描述。那么，$x_H$ 表明 $x$ 是一个机密性高(high) 的变量，其包含了仅可以被获得授权的主体访问的敏感信息；而 $y_L$ 表明 $y$ 是一个机密性低 (low) 的变量，它可以被任何主体访问。这里的 $H$ 和 $L$，在这里就被称作安全类型。我们先来看两个例子。

int $x_H$;

int $y_L$;

$y_L:=x_H$;

对于上面的程序片段，由于 $y_L:=x_H$ 这条语句的影响，机密性高的 $x_H$ 的值被付给了机密性低的 $y_L$。一个没有授权的主体（如攻击者）可以通过观察 $y$ 的值来判断 $x$ 的值，这事实上就泄露了机密性高的数据；因此一个安全的程序片段应该杜绝这种 显式的信息流(explicit flow)。

if (($x_H$%2)==0) {

$y_L:=0$;

} else {

$y_L:=1$;

}

对于上面的程序片段，尽管这里没有直接的从 $x$ 到 $y$ 的赋值，但是我们仍然可以通过观察 $y$ 是 0 或 1 来判断 $x$ 的奇偶性 (事实上，上述片段等价于 $y_L:=x_H\%2$)，从而造成一定程度的信息泄露；因此一个安全的程序片段应该杜绝这种 隐式的信息流(implicit flow)。

我们注意到信息流需要对程序片段做很细粒度的分析，而可以基于一些特定的类型推导规则通过判断对应的程序片段可以被类型化 (typable) 而验证程序片段是安全的。如对于显式信息流，我们可以给定推导规则，仅在赋值语句的左值安全等级高于右值的情况下才可以满足我们的类型检查规则要求（则 $y_L:=x_H$ 语句在我们的类型系统中无法通过检查）；由此，我们给定了相应的规则，就可能保证只要符合我们的规则的程序片段在不造成信息泄露的意义下是安全的。

不考虑权限的安全类型系统的缺陷

下面我们分析一下有权限模型的 Android app 情形。

对于这样一个抽象化的程序片段，$A.f$ 表明这是一个 Android app A 的一个函数 $f$，而 checkPermission(CONTACT) 用来检查调用 app $A$ 的另一个 Android app 是否有 CONTACT 权限。注意：这里的 “调用” 可以是广义上的 RPC，如体现在 Android 的 intent 机制。程序本身的语义为，当调用 app (calling app) 有 CONTACT 权限时，则 app $A$ 提供联系人信息；否则不提供相关机密信息。直观而言，如果调用 app $A$ 的这个 app 有 CONTACT，那它能够获取联系人信息；因此这里并不存在信息泄露。然而，当我们对这一段代码进行应用安全类型系统分析时，我们会发现 它不能被类型化。

我们看一下上面的这种调用情形，由 App $B$ 通过函数 $h$ 来调用 $A.f$。我们假定变量 “r” 是一个机密性低的变量 (任何人可以观察到该变量的值)。由于 info(name) 是一个敏感数据其安全类型为 $H$，并且由前面得知 res := info(name) 这样的赋值导致 res 不可能为 $L$，因此它必然为 $H$；对于 if-else 语句，对于类型系统而言，它需要保证两个分支有同样的类型，因此 if-else 分支之后，res 的类型为 $H$，从而 $A.f$ 返回的类型也为 $H$。但是这会导致 r := A.f("Bob")成为一个不被允许的显式信息流(从类型系统而言它不可以类型化)；但如前所述这段代码不存在信息泄露。这就是说，如果我们不特别对待这里的包含权限检查 checkPermission 的 if-else 语句，我们会因为类型推导规则能力不强而不能验证一些不存在信息泄露的程序片段；因此这样的类型系统，尽管它仍然能够验证“凡是能够被类型化的程序片段都不存在信息泄露问题”，但往往只有极少数的程序片段能够被类型化。我们的目标是来改良类型系统和推到规则，使得我们可以通过类型系统来验证更多的程序片段。

安全类型系统

如何改良呢？最直接的，我们需要区别对待带 checkPermission 的 if-else 语句——而这正是权限检查带来的信息泄露判断的差异。接下来我们沿着这个思路来建立类型系统。

**首先我们定义我们的安全类型。**上述的安全类型，本身是一个对变量安全等级的一个标签，并且所有的安全类型形成了一个格结构。在有权限的条件下，我们将之泛化：我们将基础 (安全) 类型定义成一个 从权限到安全标签的一个映射。下图中给出了相应的定义：

• 基于安全标签的偏序关系，我们定义了安全类型的偏序关系。在这个一一下，这样的安全类型仍然形成一个格。

• 对于函数类型，我们则定义为函数参数到返回值类型的一个映射。

接下来我们定义基本类型的 “升级” 和“降级”，这是基于调用 app 是否已经有某权限 $p$ 来区分的。

为了突出我们基于权限的安全类型系统这一主要贡献，我们将被分析的程序语言抽象为如下类似于 WHILE 的指令式语言，其由表达式、语句及函数组成。特别地，这里包含了独特的 test($p$) $c$ else $c$ 语句用于检查权限，这对应 Android 中的 checkPermission，它表示如果调用的 app 包含权限 $p$ 则执行前一个分支、否则执行后一分支。同时，对于普通调用和 IPC 调用，我们都将之抽象为 $x:=$call $A.f(\bar{e})$ 语句。同时，根据类型检查的特殊性，我们将相关结构形式做了调整，本身的 (操作) 语义是显而易见的。值得注意的是，这里的调整主要用于方便描述问题，其表达能力和图灵完备的指令式语言并无差异；同时，Android 等真实程序也可以通过抽象书写成我们提供的语言的形式。

此外我们定义了 “合并类型”，用于描述有无特定权限 $p$ 条件下的类型。不难发现，这一类型正是用于表述 test($p$) $c$ else $c$ 语句在有权限 $p$ 和无权限 $p$ 的类型情况。

有了这些新定义的类型，我们定义了与之适配的考虑了权限的类型系统。我们可以证明本类型系统的 soundness：

可被类型化的类型系统一定是 non-interferent。

non-interferent 这一特性保证了攻击者无法了解任何敏感的机密信息，它大概的意思是如果程序片段的两个初始状态是不可以被观察者所区分的，在执行当前的某条语句 (command) 之后，观察者仍然无法区分这两者状态上的差异。在 non-interference 的条件下，程序片段的行为自然是是安全的——同一安全等级的观察者不会无法通过发现差异来获得或猜测到相关信息，因而不存在信息泄露。由于这里涉及到较多的证明和概念，不再赘述；可参考论文内容。

类型系统下的安全类型检查

下面描述了前述的 Android IPC 情况下，这段程序片段在我们的类型系统之下是可以被类型化的，进而可以验证它是 non-interferent。可以发现，对于 (T-CP) 这条 test 语句的类型检查规则，我们使用了 “合并类型”，从而权限的信息在推导规则中得以保留。对于 app $B$ 有权限 $p$ 的情形($p\in P$) 和没有权限 $p$ 的情形 ($p\notin P$) 都是可以被类型化的。因此我们的类型系统可以描述这样的安全行为。这是我们的类型系统相对没有考虑权限下的优越性所在。

安全类型系统的非单调特性

当然也有一些其他类型系统考虑了权限，下面的例子表明，我们的类型系统可以表述 “非单调” 的安全策略，而现有的其他类型系统不具备这一能力。“单调” 的意思是指，如果调用 app 有了更多的权限，它可以获得的信息越多。不少场景下单调性是可以保证的；但是在有些场景中会遇到不满足这一特性的案例。

对于上图的例子，我们用 $p$ 来守护 Android 设备 ID 的信息，它对应的是 Android 中的 READ_PHONE_STATE 的权限；同时我们使用 $q$ 来守护设备的位置信息，它对应的是 Android 中的 ACCESS_FINE_LOCATION。假定有一个 app 需要使用位置信息来获得广告 ID，而该广告 ID 可用于推送基于位置信息的广告。这里的广告 ID 仅用于广告目的，我们的安全策略要求使用该服务的 app 不应当基于广告 ID 信息和设备 ID 信息来建立关联——例如当广告 ID 信息和设备 ID 信息同时被调用 app 所观察到，这种隐私泄露可能通过基于广告的信息定位到个人，引发安全隐患。因此，当调用该服务的 app 同时申请获取设备 ID 信息的权限 p 和获取设备位置信息 q 的权限时，事实上应当少暴露一些信息。例如基于这一安全准策略抽象而来的如下程序片段。在 p 和 q 都已经被申请的条件下，我们只暴露了位置信息；但当仅申请了位置信息的权限 $q$ 时，可以同时暴露广告 ID 和位置信息。我们使用 $l_1$ 作为广告 ID 的安全标签，$l_2$ 作为位置信息的安全标签，$L$，$H$ 分别是 $l_1$ 和 $l_2$ 的最小上界和最大下界。可以经过类型推到将这个程序片段类型化。其中，在 $p,q$ 权限都申请的情况下，我们的类型系统可以将对应的安全标签直接表述为 $l_2$。但其他考虑权限的安全类型系统却受单调性制约，例如 Banerjee 和 Naumann 在 2005 年的论文 Stack-based access control and secure information flow [1]里，只能将 $p,q$ 权限都已经申请的情况下，将对应的安全标签表述为 $H$，从而带来了不准确。

结语

此外，由于 Android 中权限检查的语义只能检查 直接调用 当前 app 的 app 权限，这造成了权限是不可以在调用链上传递下来的；现有的类型系统通常只考虑了权限传递的情形，而我们的类型系统的类型检查和推导规则通过 “类型投影” 的方式准确表达了这一机制。同时，我们还结合约束生成和约束求解形成了一套类型推断规则，并证明了我们的类型推断系统是可决定 (decidable) 的。

关于利用带权限的安全类型系统来做信息流验证，本文只是冰山一角，验证了一个高度抽象的 Android 程序片段上的信息流安全。由于涉及到的概念和证明比较多，部分内容难以通过本文来描述清楚，读者可以通过阅读原论文加深理解。

最后想和大家说一下我对类型研究的一点微末见解。一方面，我们想到类型系统，需意识到不仅可以依赖于 “结构类型” 来保证编程语言本身的一些良好特性 (事实上现代的编程语言如 Rust/Julia/Go 等都会借助类型来禁止一些犯错误的可能)，而且能够作为标签来解决一些可通过推导规则进行泛化特性(如机密性) 检查的手段。例如信息流上的安全类型，尽管有些非主流，但是确实是可以建立进行相关验证并得到一些好的性质。另一方面，类型理论 (typpe theory) 可能更加有趣且更具有深远意义：事实上类型论可以规避“罗素悖论” ，且在绝大多数计算机证明辅助系统中被用作集合论的替代理论。如今我们的生活已经和计算机息息相关，因此或许在不久的将来类型论会比集合论更加为人熟知。

参考

[1]: Stack-based access control and secure information flow https://www.cambridge.org/core/journals/journal-of-functional-programming/article/stackbased-access-control-and-secure-information-flow/27C5A3345D3CE01E733207F1BF9BF363