大多数软件开发团队依赖动态测试方法，检测软件中的缺陷和运行时错误。动态测试需要工程师编写和执行大量测试用例。由于动态测试不能穷尽所有情形，单靠它还不足以确保软件安全可靠。
静态应用程序安全测试 (SAST) 或静态分析应用在软件开发生命周期 ( SDLC ) 的早期以及不要求执行代码，而是通过分析源代码实现质量、可靠性和安全性提升的目的。使用静态分析，可以发现使应用程序容易受到攻击的安全漏洞。静态分析不产生测试用例编写和代码检测配置的开销，因此可以较为经济地衡量和跟踪软件质量指标。
基于服务端已有Checkmarx、INSIDER CLI和Argon等较为成熟的SAST工具，而基于移动端，在FlowDroid之外，Mariana Trench也凭借其较快的检测速度进入我们的视野。
Mariana Trench是Facebook推出的，一个面向Android的以安全为中心的静态分析工具，该工具提供可扩展的全局污点分析，用来发现和防止Android中的安全和隐私漏洞。
-
指定自定义的"source" 和 "sink"
（1）编写一个或多个基于模型生成器领域特定语言 (model generator Domain Specific Language)的 json 文件，该文件表达了如何从方法生成模型，因此被称为 “模型生成器（model generators）”。
模型生成器（model generators）示例
（2）指示Mariana Trench从自定义的模型生成器中读取数据。
-
通过解释模型生成器生成的模型在运行 Mariana Trench之前表达了每种函数的"source" 和 "sink"。基于这些模型，Mariana Trench 将在运行时自动为每个函数推断新模型。
-
在mariana-trench/tree/main/configuration/model-generators路径下添加自定义的 json 模型生成器，已指示Mariana Trench 从自定义的 json 模型生成器中读取数据。
（3）更新“规则”。
规则示例
-
在Android 应用程序项目的存储库上运行 Mariana Trench
命令如下：
-
从网络浏览器查看分析结果
使用SAPP PyPi来执行对结果的处理操作，命令如下：
输出的最后一行告诉我们 SAPP 启动了一个本地网络服务器，让我们查看结果，打开链接：
示例的Issue2的意思是，Mariana Trench发现了一个远程代码执行漏洞，MainActivit.onCreate中的数据来自Activity.getIntent的调用，并流入ProcessBuilder构造函数的调用。
SAST一般的实现过程为：首先构建IR(Intermediate Representation)，根据IR生成Basic Blocks和Call Graph，最后依据Basic Blocks构建的intra-procedural Control-Flow Graph与Call Graph构成inter-procedural Control-Flow Graph，在此之上进行数据流分析。
Mariana Trench利用了建立在 Redex 之上的现有静态分析基础设施。生成IR和Basic Blocks，以及构建intra-procedural Control-Flow Graph都是基于Redex实现的。
-
IR
在生成IR之前，Redex使用Mark and Sweep算法对dex文件进行了消除Dead code的操作。此处的字节码优化操作，笔者认为是Mariana Trench检测速度较快的原因之一。
消除Dead code的函数remove_unreachable()的部分代码如下：
Redex生成的IR 与 Dalvik 指令集非常相似，但进行了一些调整以使其更易于分析和操作。主要区别在于：
-
可以寻址任意大小的寄存器。
-
IROpcode 中不存在 2addr 操作码。
-
IROpcode 中不存在范围指令。
-
invoke-* 指令不再引用宽寄存器的两半。
-
任何既可以抛出也可以写入 dest 寄存器的操作码在IR 中被分成两个独立的部分：一个可以抛出但不写入 dest 的部分，以及一个写入到 dest 但不抛出的 move-result-pseudo 指令。
-
check-cast也有一个move-result-pseudo后缀。
-
有效载荷指令不再存在。
-
只有一种类型的开关。Sparse switches和packed switches都表示为单个“switch”IR 操作码。
-
intra-procedural Control-Flow Graph
intra-procedural Control-Flow Graph是Basic Blocks的有向图。
每个“Block”都有一定数量的继任者和前任者。`Block`通过指定连接类型的`Edge`连接到它们的前任和后继。
现在有可编辑和不可编辑这两种类型的 CFG。不可编辑的 CFG 块具有指向 IRCode 内的大线性 IRList 的开始和结束指针。而每个可编辑的 CFG 块都有一个小的 IRList（MethodItemEntries 取自 IRCode）。
可编辑模式是 CFG 的新版本。将来，它将完全取代 IRCode 作为主要代码表示形式。要构建可编辑的 CFG，可以调用函数`code->build_cfg(true)`。
部分相关代码如下：
-
Call Graph
Call Graph允许用户在他们的程序中查看父子程序之间的关系。本质上，Call Graph中的每个节点都代表一个函数（f），每条边代表被（f）调用的函数（g）。一个节点可以被认为是“父函数”，每个节点都是“子函数”。
Mariana Trench使用class hierarchy analysis（CHA）算法构建Call Graph。CHA 的优点是速度快，因为它仅考虑在调用点声明的接收器（receiver）变量类型及其继承层次结构和忽略数据和控制流信息。但相应地，它的缺点是不精确，容易引入虚假的目标方法。
部分相关代码如下：
-
inter-procedural Control-Flow Graph
结合intra-procedural Control-Flow Graph和Call Graph形成inter-procedural Control-Flow Graph，Mariana Trench在此基础上进行污点分析，此处涉及不动点等相关数学理论。
部分相关代码如下：
尽管Mariana Trench目前不支持最新的dex版本，但是有它自身的显著优势：对Android平台的友好特性、较短的扫描时间和较为灵活的规则定制。其底层使用的Redex也被一些公司二次开发用于优化apk包，也是比较值得注意的一个点。总之，笔者认为Mariana Trench是一款不错的静态分析工具，如果在使用前进行一定的定制化，会在使用上产生显著的效果。
参考文献：
[1] 《Mariana Trench Documentation》：https://mariana-tren.ch/docs/overview/
[2] 《Optimizing Android bytecode with ReDex》：https://engineering.fb.com/2015/10/01/android/optimizing-android-bytecode-with-redex/
[3] 《Static Application Security Testing》：https://www.synopsys.com/glossary/what-is-sast.html
[4] 《Call Graph》：https://microchipdeveloper.com/mplabx:call-graph
[5] 《Fixed point (mathematics)》：https://en.wikipedia.org/wiki/Fixed_point_(mathematics)
[6] 《基于 ReDex 的 DEX 优化落地实践》：https://www.51cto.com/article/710484.html
[7] 《Redex源码分析》：http://yourbay.me/all-about-tech/2020/05/12/redex-1-arch/
[8] 《浅谈 Android Dex 文件》：https://tech.youzan.com/qian-tan-android-dexwen-jian/
原文始发于微信公众号（vivo千镜）：Android静态分析平台Mariana Trench分析
- 左青龙
- 微信扫一扫
-
- 右白虎
- 微信扫一扫
-
评论