Meta’s Mariana Trench

Modeling repeated Android callbacks

An Android lifecycle callback can run more than once. A model that represents the callbacks as a single sequence can miss paths where sensitive data carries over into another invocation.

I added C++ support for defining lifecycle callbacks as a control-flow graph. The graph represents callbacks as nodes and possible transitions as successor edges, so it can express repeated invocations. I also added validation for entry points, successor references, and unreachable nodes to catch graph definitions the analyzer could not use correctly.

Passing analyzer configuration through JSON

The Python launcher previously passed configuration to the C++ analyzer as command-line arguments. I changed the launcher to write the options to a JSON file and pass the file path to the analyzer. The C++ side then reads the options from that file. This gives the launcher and analyzer a structured way to exchange configuration.