We’re sharing details about Mariana Trench (MT), a tool we use to spot and prevent security and privacy bugs in Android and Java applications. As part of our effort to help scale security through building automation, we recently open-sourced MT to support security engineers at Facebook and across the industry.
This post is the third in our series of deep dives into the static and dynamic analysis tools we rely on. MT is the latest system, following Zoncolan and Pysa, built for Hack and Python code respectively.
Facebook’s mobile applications, including Facebook, Instagram, and Whatsapp, run on millions of lines of code and are constantly evolving to enable new functionality and improve our services. To handle this volume of code, we build sophisticated systems that help our security engineers detect and review code for potential issues, rather than requiring them to rely on only manual code reviews. In the first half of 2021, over 50 percent of the security vulnerabilities we found across our family of apps were detected using automated tools.
We built MT to focus particularly on Android applications. There are differences in patching and ensuring the adoption of code updates between mobile and web applications, so they require different approaches. While server-side code can be updated almost instantaneously for web apps, mitigating a security bug in an Android application relies on each user updating the application on the device they own in a timely way. This makes it that much more important for any app developer to put systems in place to help prevent vulnerabilities from making it into mobile releases, whenever possible.
MT is designed to be able to scan large mobile codebases and flag potential issues on pull requests before they make it into production. It was built as a result of close collaboration between security and software engineers at Facebook who train MT to look at code and analyze how data flows through it. Analyzing data flows is useful because many security and privacy issues can be modeled as data flowing into a place it shouldn’t.
You can find MT on GitHub, and we’ve released a binary distribution on PyPI. We’ve also written a short tutorial to help get you started. Our teams are actively developing and continuing to improve MT. We welcome your feedback: If you are interested in collaborating with us, please open an issue or reach out to us on GitHub.
How Mariana Trench works
MT works very similarly to Zoncolan and Pysa. The main difference is that MT is optimized for analyzing Android and Java applications. We briefly cover the basics in this blog post and encourage our readers to review our previous write-ups for a more in-depth technical explanation.
Security engineers often think of vulnerabilities in terms of data flows that they don’t want to see in their applications. For example, an application should not be logging sensitive data or be subject to injection vulnerabilities that would allow attackers to insert malicious code.
In MT, a data flow can be described by:
- Source: a point of origin. This can be a user-controlled string entering the app through `Intent.getData`.
- Sink: a destination. In Android, this can be a call to `Log.w` or `Runtime.exec`.
A large codebase can contain many different kinds of corresponding sources and sinks. We can tell MT to show us specific flows by defining rules. A rule could specify, for example, that we want to find intent redirections (issues that allow attackers to intercept sensitive data) by defining a rule that shows us all traces from “user-controlled” sources to an “intent redirection” sink.
MT finds possible paths from each source to its corresponding sink. It does this by computing a model for each Java method it sees in the codebase. The models are computed using a static analysis technique called abstract interpretation.
How security engineers use Mariana Trench
MT is how security engineers scale their work as part of Facebook’s defense-in-depth application security efforts. In a typical scenario, a security engineer would start by broadly defining the boundaries of the data flows she is interested in scanning the codebase for. For example, if she wants to find SQL injections, she would need to specify where user-controlled data is entering the code (e.g., intents in Android, the filesystem, etc.) and where it is not meant to go (e.g., any API constructing SQL queries). However, this is only the start — defining a rule connecting the two is not enough. Engineers also have to review the identified issues and refine the rules until the results are sufficiently high-signal.
As with all engineering efforts, any tool that automatically scans code comes with inherent trade-offs. Traditionally, static analysis research has heavily focused on minimizing false positives. For security, that calculus can be very different. In using MT at Facebook, we prioritize finding more potential issues, even if it means showing more false positives. This is because we care about edge cases: data flows that are theoretically possible and exploitable but rarely happen in production.
To help security engineers manage and triage the output, we built MT to let them quickly determine whether an issue is in fact a true positive by letting them search through results based on criteria such as the length of a trace or the specific functions encountered on a trace.
Once the rule has been created and has proved effective, we promote it to run on every pull request. If MT finds a flow violating the rule, the flow can then be surfaced to either an on-call security engineer or directly to the software engineer who made the pull request.
Rather than relying on MT as a silver bullet, we use it as part of the broader defense-in-depth approach. As Facebook invests in improving the fidelity of signals MT generates, security engineers continually iterate to refine rules and diagnose limitations of MT in collaboration with the software engineers building our apps.
Navigating the results: Static Analysis Post Processor
In addition to building the static analysis systems themselves, we’ve created open source tooling to review and analyze the results produced by MT (as well as Pysa). We call our standalone processing tool Static Analysis Post Processor (SAPP).
We first shared our work on SAPP and how to use its command line interface (CLI) to navigate Pysa at DefCon in 2020. SAPP was purposely built to support different static analysis tools, and it supports MT out of the box.
SAPP takes the raw output from MT and makes it easy to triage the results. SAPP is designed to visually demonstrate how data can potentially flow from source to sink so it is easier for experts to quickly evaluate whether they agree with the tool’s assessment.
SAPP’s trace view illustrates the data flow step-by-step. It highlights the relevant lines of code, allowing the security engineer to walk through possible paths that eventually reach the same sink location in the code.
To give you an idea of what this looks like, here is a quick demo of how MT runs on a sample app:
As you can see, SAPP presents a list of issues, each of which is a potential vulnerability. Each issue contains one or more traces; if several traces are materially similar, they are grouped into the same issue to help evaluate whether the overall issue is valid. SAPP supports extensive filtering and search functionality to allow security engineers to focus on the results they want to explore within each list.
How to get started with Mariana Trench
MT is available on GitHub, and we’ve released a binary distribution on PyPI. We’ve also written a short tutorial to help get you started.
Our teams are actively developing MT to continue to improve it. If you have feedback or are interested in collaborating with us, please open an issue or reach out to us on GitHub.
We’d like to thank Maxime Arthaud, Amar Bhosale, Gerben Janssen van Doorn, Yuh Shin Ong, Chenguang Shen, Simran Virk, Shannon Zhu, and everyone else who worked on Mariana Trench.
