目录导航
Mariana Trench[马里亚纳海沟]–此Mariana Trench是由Facebook出品的安全工具!
什么是Mariana Trench
马里亚纳海沟是一个针对 Android 的专注于安全的静态分析平台。
该工具提供了一个可扩展的全局污点分析,类似于Python 的Pysa等预先存在的工具。
该工具利用了构建在Redex之上的现有静态分析基础设施(例如,SPARTA)。

默认情况下,Mariana Trench 会分析dalvik 字节码,并且可以在访问或不访问源代码的情况下工作。
入门
本指南将引导您在您的机器上设置马里亚纳海沟,并让您在一个小型示例应用程序中找到您的第一个远程代码执行漏洞。
先决条件
马里亚纳海沟需要最新版本的Python。
在 MacOS 上,您可以通过homebrew获取当前版本:
brew install python3
在 Debian 风格的 Linux(Ubuntu、Mint、Debian)上,您可以使用apt-get
进行安装:
sudo apt-get install python3 python3-pip python3-venv
本指南还假设您已安装Android SDK,并且环境变量$ANDROID_SDK
指向 SDK 的位置。
对于本指南的其余部分,我们假设您在虚拟环境中工作。你可以设置这个
$ python3 -m venv ~/.venvs/mariana-trench
$ source ~/.venvs/mariana-trench/bin/activate
(mariana-trench)$
shell 提示前面的虚拟环境名称表示虚拟环境处于活动状态。
安装马里亚纳海沟
在您的虚拟环境中安装马里亚纳海沟就像运行一样简单
(mariana-trench)$ pip install mariana-trench
运行马里亚纳海沟
我们将使用一个小应用程序,它是我们文档的一部分。你可以通过运行如下命令得到它
(mariana-trench)$ git clone https://github.com/facebook/mariana-trench
(mariana-trench)$ cd mariana-trench/documentation/sample-app
我们现在准备运行分析
(mariana-trench)$ mariana-trench \
--system-jar-configuration-path=$ANDROID_SDK/platforms/android-30/android.jar
--apk-path=sample-app-debug.apk \
--source-root-directory=app/src/main/java
# ...
INFO Analyzed 68886 models in 4.04s. Found 4 issues!
# ...
分析在我们的示例应用中发现了 4 个问题。分析的输出是应用程序的每种方法的一组规范。
后处理
规范本身并不适合人类阅读。我们需要一个额外的处理步骤,以使结果更具表现力。我们使用为我们安装的SAPP PyPi 来执行此操作:
(mariana-trench)$ sapp --tool=mariana-trench analyze .
(mariana-trench)$ sapp --database-name=sapp.db server --source-directory=app/src/main/java
# ...
2021-05-12 12:27:22,867 [INFO] * Running on http://localhost:5000/ (Press CTRL+C to quit)
输出的最后一行告诉我们 SAPP 启动了一个本地网络服务器,让我们查看结果。打开链接,您将看到分析人员发现的 4 个问题。
探索结果
让我们关注在示例应用程序中发现的远程代码执行问题。您可以通过它的问题代码1
(对于所有远程代码执行)和 callable来识别它void MainActivit.onCreate(Bundle)
。只需查看 4 个问题,就可以轻松手动识别问题,但是一旦运行更多规则,页面右上角的过滤器功能就会派上用场。

该问题告诉您,Mariana TrenchMainActivit.onCreate
在数据来自Activity.getIntent
一个调用的地方发现了一个远程代码执行,并流入了ProcessBuilder
3 个调用的构造函数。单击问题右上角的“跟踪”以查看示例跟踪。
马里亚纳海沟浮出水面的痕迹由三部分组成。
所述源跟踪表示其中数据是来自。在我们的示例中,跟踪非常短:直接Activity.getIntent
调用MainActivity.onCreate
。

所述迹线的根表示其中源跟踪满足水槽跟踪。在我们的示例中,这是活动的onCreate
方法。

跟踪的最后一部分是接收器跟踪:这是来自源的数据向下流入接收器的地方。在我们的示例中,从onCreate
、到onClick
、到execute
,最后进入 的构造函数ProcessBuilder
。

自定义源和接收器
概述
在马里亚纳海沟的背景下,我们从方法的角度谈论源和汇。例如,我们可以说一个方法的返回值是一个源(或一个接收器)。我们也可以说方法的第二个参数是一个源(或一个接收器)。对方法的这种描述称为“模型”。有关模型和编写模型的更多详细信息,请参阅模型。
要定义未包含在默认的sources和sinks集合中的源或汇,用户需要:
- 编写一个或多个符合我们的模型生成器领域特定语言 (DSL) 的JSON 文件,这些文件表达了如何从方法生成模型,因此被称为 “模型生成器”。
- 例如,模型生成器可能会说,对于名称为 的所有方法(将由马里亚纳海沟分析)
onActivityResult
,将其第二个参数指定为源。
- 例如,模型生成器可能会说,对于名称为 的所有方法(将由马里亚纳海沟分析)
{
"model_generators": [
{
"find": "methods",
"where": [
{
"constraint": "name",
"pattern": "onActivityResult"
},
],
"model": {
"sources": [
{
"kind": "TestSensitiveUserInput",
"port": "Argument(2)"
}
]
}
}
}
- 指示马里亚纳海沟从您的模型生成器中读取数据,以便马里亚纳海沟在运行时生成模型。
- 直观地说,在运行马里亚纳海沟之前,通过解释模型生成器生成的模型表达了每种方法的源和汇。基于这些模型,马里亚纳海沟将在运行时自动为每个方法推断新模型。
- 要指示 Mariana Trench 从自定义 JSON 模型生成器中读取数据,请在此处添加您的 json 模型生成器。
- 在JSON 配置文件中添加模型生成器名称(即文件名)。
- 如有必要,更新“规则”。
- 背景:马里亚纳海沟将源和汇分为不同的“种类”,它们是字符串类型的。例如,一个源可能有一种
JavascriptInterfaceUserInput
. 一个接收器可能有一种Logging
. 马里亚纳海沟只发现从特定类型的源到另一种特定类型的汇的数据流,这被称为“规则”。 - 要指定默认规则集中未提及的种类或指定与默认规则不同的规则,您需要在 file 中指定新规则,
rules.json
以指示马里亚纳海沟查找与新规则匹配的数据流. - 例如,要从
TestSensitiveUserInput
上面的示例中捕获流和 sink kindLogging
,您可以将以下规则添加到 defaultrules.json
:
- 背景:马里亚纳海沟将源和汇分为不同的“种类”,它们是字符串类型的。例如,一个源可能有一种
{
"name": "TestRule",
"code": 18,
"description": "A test rule",
"sources": [
"TestSensitiveUserInput"
],
"sinks": [
"Logging"
]
}
配置
马里亚纳海沟是高度可配置的,我们建议您花时间根据您的特定用例调整工具。在 Facebook,我们有专门的安全工程师,他们将花费大量时间添加新规则和模型生成器来改进分析结果。
本页将介绍更重要、更重要的配置选项。请注意,您将花费大部分时间配置马里亚纳海沟来编写模型生成器。这些将在下一节中介绍。
命令行选项
您可以通过运行获得一整套选项mariana-trench --help
。以下是输出的缩写版本。
$ mariana-trench --help
目标参数:
--apk-path APK路径 要分析的APK
输出参数:
--output-directory 输出目录
存储结果的目录
配置参数:
--system-jar-configuration-path 系统jar的配置路径列表
一个JSON配置文件,包含到系统jar的路径列表。
--rules-paths 规则路径
由“;”分隔的规则文件列表和包含规则文件的目录。
--repository-root-directory REPOSITORY_ROOT_DIRECTORY
存储库的根目录。结果路径将相对于此
--source-root-directory SOURCE_ROOT_DIRECTORY
可以找到APK源文件的根目录。
--model-generator-configuration-paths MODEL_GENERATOR_CONFIGURATION_PATHS
一个';'分隔的路径列表,指定JSON配置文件。属性的JSON模型生成器的路径列表配置文件或CPP模型生成器的名称。
--model-generator-search-paths MODEL_GENERATOR_SEARCH_PATHS
一个';'分隔的路径列表,用于查找JSON模型生成器
--maximum-source-sink-distance MAXIMUM_SOURCE_SINK_DISTANCE
限制源和汇从痕迹入口点的距离。
--apk-path
马里亚纳海沟分析 Dalvik 字节码。您为其提供 Android 应用程序 (APK) 以进行分析。
--output-directory OUTPUT_DIRECTORY
分析的输出是一个文件,其中包含有关 JSON 格式的特定运行的元数据,以及包含 APK 中每个方法的数据流规范的分片文件。这些文件需要在分析后由 SAPP 处理(参见入门)。该标志指定这些文件的保存位置。
--system-jar-configuration-path SYSTEM_JAR_CONFIGURATION_PATH
此路径指向一个 json 文件,其中包含.jar
分析应包含在分析中的文件列表。重要的是,这至少包含android.jar
您系统上的 。此文件通常位于您的 android SDK 发行版中的$ANDROID_SDK/platforms/android-30/android.jar
. 如果没有android.jar
,Mariana Trench 将无法了解标准库中可能对您的模型生成器很重要的许多方法。
--rules-paths RULES_PATHS
一个;
分离的搜索路径指向文件,并且包含规则文件的目录。这些文件指定了马里亚纳海沟应该寻找的污点流。查看rules.json
默认提供的。它指定我们要查找从用户控制的输入 ( ActivityUserInput
) 到CodeExecution
接收器的流,这构成了远程代码执行。
--source-root-directory SOURCE_ROOT_DIRECTORY
马里亚纳海沟将在分析之前做一个源索引路径。这是因为 Dalvik/Java 字节码不包含完整的位置信息,只有文件名(不是路径)和行号。该索引稍后用于发出精确位置。
--model-generator-configuration-paths MODEL_GENERATOR_CONFIGURATION_PATHS
一组;
单独的文件,其中包含要运行的模型生成器的名称。参见default_generator_config.json
示例。
--model-generator-search-paths MODEL_GENERATOR_SEARCH_PATHS
一个;
单独的搜索路径,Mariana Trench 将在其中尝试查找生成器配置中指定的模型生成器。
--maximum-source-sink-distance MAXIMUM_SOURCE_SINK_DISTANCE
出于性能原因,限制马里亚纳海沟试图找到的轨迹的最大长度可能很有用(请注意,较长的轨迹也往往更难解释)。由于分析的模块化特性,此处指定的值限制了从跟踪根到源以及从跟踪根到汇的最大长度。这意味着找到的跟踪长度可以为2 x MAXIMUM_SOURCE_SINK_DISTANCE
.
项目地址
GitHub:github.com/facebook/mariana-trench
官网地址:https://mariana-tren.ch/