Page 131 - 《软件学报》2021年第6期
P. 131

张捷  等:基于污染变量关系图的 Android 应用污点分析工具                                                1705


         确定潜在污染流;最后,在控制流图上对污染流进行验证,得到程序中真实存在的污染流.为此,我们形式化定义
         了污染变量关系图,设计了污染传播规则和验证污染流的算法.
         2.2   污染变量关系图
             我们提出污染变量关系图(tainted value graph,简称 TVG)用于描述程序中所有可能存在的污染变量、别名
         变量及变量间的污染传播关系.直观来看,所有污染变量都是由污点源传播得到的,污染变量及其别名变量通过
         各种污染传播方式不断扩散,最终传播到一个泄露点,形成一条泄露隐私数据的污染流.为准确表达这样的污染
         传播过程,我们使用图的结构记录变量及其传播关系.下面给出污染变量关系图的定义:污染变量关系图是一个
         简单有向连通图 TVG=(V,E),其中,顶点 v∈V 表示一个污染变量、污点源或泄露点,边 e∈E 表示两个变量的污染
         传播关系、变量被污点源污染或者污染变量传播给泄露点的关系.另外,我们要求 TVG 满足以下性质.
             •   有且仅有一个入度为零的顶点,即污点源顶点 SC i ;存在零或若干泄露点顶点 SK j ;
             •   除了 SC i 以外的所有顶点都至少存在一条从 SC i 到该顶点的路径;
             •   图中不含回路.
             从性质来看,每个 TVG 对应一个污点源在程序中的传播过程.当一个应用中存在多个污点源时,则可生成
         相同数量的 TVG,而污染流能否形成取决于图中是否有污染变量被泄露.例如,图 2 显示了图 1 程序中的 TVG,
         整个程序中存在许多变量,用空心圆圈表示,其中,红色空心圆圈是污染变量,红色实心圈表示污点源,蓝色实心
         圈表示泄露点.该 TVG 的顶点集 V={SC 1 ,a,b,x,y,SK 1 },边集 E={(SC 1 ,a),(a,b),(b,x),(x,y),(y,SK 1 )}.在现实中,污染变
         量之间的关系可能更加复杂,存在一对一、一对多和多对一的情况.举例来说:当某污染变量分别污染多个不同
         变量,或者作为参数传入到多个函数,此时,该变量的顶点将连接多条边到其他顶点;当两个不同的污染变量都
         作为同一参数调用某函数时,此时,两个污染变量的顶点将各自连接一条边到该函数形参的顶点上.












                                     Fig.2    An example of tainted value graph
                                          图 2   污染变量关系图示例
         2.3   污染传播规则
             我们定义了一系列污染传播规则用于发现污点源、污染变量及泄露点,并创新性地将别名规则也作为一类
         污染传播方式加入到规则中.这样,在分析中可同时寻找污染变量及其别名,并一同构成 TVG.污染传播规则采
         用类似 Datalog 的语言来定义,Datalog     [22] 是一种应用于数据库查询的语言,由于其较强的逻辑性,被广泛应用于
         各类研究领域,例如程序分析、信息提取等.一段 Datalog 程序由一套规则和一组事实组成,事实由谓词描述.每
         条规则由左右两部分构成,中间用:-符号分隔开.当右部所有谓词都成立时,左部的谓词为真.对于污染传播规则
         来说,当语句及其包含的变量满足某项规则右部的所有谓词时,左部的变量污染传播关系存在或者某个描述变
         量或方法性质的谓词成立.
             我们定义了 S,IN,Param,Return,ReturnP,Clean,hp 等谓词用于描述程序中语句或者变量的性质.S(stmt)谓词
         描述了语句 stmt 的类型,当满足特定类型的语句时,谓词为真;IN(x)为真,表示变量 x 是污染变量;Param(f,x,i)为
         真,表示函数 f 第 i 个参数被传入污染变量 x;Return(f,x)为真,表示函数 f 返回污染变量 x;ReturnP(f,x,i)为真,表示
         函数 f 第 i 个实参在函数内被变量 x 污染;Clean(x)为真,表示污染变量 x 被清除;hp(x)表示 x 为堆变量.规则中的
         Source,Sink 分别表示污点源和泄露点方法的集合,TW 表示污染封装方法集合.污染封装方法是指在 Java 和
   126   127   128   129   130   131   132   133   134   135   136