Mantiserve¶
Important
Users interact with Mantiserve via the the MATE REST API. See the documentation here.
Mantiserve is a service included with MATE that serves a REST API to start, check, and kill Manticore tasks. Mantiserve uses the MATE-built target binary and associated CPG to perform its analyses.
Manticore is a symbolic execution tool for analysis of binaries. It executes a target program to explore its behavior as related to user-controlled input. Manticore provides a rich API to write plugins that can detect and report on program properties like all possible values of an input at a certain point during execution. When paired with MATE and the CPG, Manticore plugins can perform deep inspection of the program during execution to detect the potential for and impact of various forms of memory corruption, violation of memory safety, and other issues.
Usage¶
The primary usage of Mantiserve is through the REST API located at http://localhost:8666/api/v1/, which you can visit on your browser for a nicely formatted FastAPI help page where you can hit the endpoints and peruse the different message schemas.
Each Mantiserve task kind requires a build_id (listed next to each target on the MATE Dashboard
at http://localhost:8050/build). This build ID is used to determine Manticore’s target
binary, as well as the Docker image to isolate Manticore’s execution within (unless
overridden by docker_image).
Within the message request body you may also optionally specify a memory limit, in MB, to impose when using Manticore within a Docker container (docker_memory_limit_mb).
Important
It is highly recommended to provide a Docker image that is representative of the deployed execution environment for the target program. Not only will this provide all of the necessary files, environment variables, and dependencies, but Docker provides system isolation for each run which is crucial for accurate and repeatable results.
Manticore executes a program just as the program itself would run. Because
Manticore does not perfectly isolate program behavior and side-effects,
Manticore execution could make permanent changes1 to the filesystem or
even the operating system itself. This could interfere with simultaneous runs
of a Mantiserve task and affect reproducibility of results. Without providing
a docker image, all runs execute in the mate_executor container and could
potentially disrupt other tasks and processes that run on that container.
- 1
By “permanent changes,” we mean to say that Manticore does not totally isolate execution side-effects of the target program. If the target issues a deletion of a file during normal execution, then that file is likely to really be deleted on the computer running Manticore. By running Manticore in a new Docker container every time, we rely on Docker’s isolation mechanisms as a good-enough solution for more deterministic analysis when Manticore is run multiple times.
Running a task¶
There are two kinds of tasks with corresponding endpoints:
Reachability - reachability - Guide Manticore along a path that you’d like to execute, and upon completion of the final
Waypoint, Manticore will return a concrete input that leads to that location. If Manticore is unable to follow your path, it will continue to execute until it has exhausted all possible paths. This task can also be done with aDetectorenabled.
Exploration - exploration - Choose a
Detectorand allow Manticore to execute and explore the binary given only initial command-line arguments,stdinparameters, or information related to the respectiveDetector. Manticore will continue exploring until it has found something2.
See the FastAPI webpage and Detectors for more details about the kinds of messages and structures that are expected.
- 2
Unfortunately, Manticore is not perfect and could be missing implementations of system calls, assembly instruction semantics, or encountered an implementation bug. Furthermore, Manticore could exhaust any one of a host machine’s resources, like RAM or storage. If Manticore is unable to recover, the Mantiserve task will attempt to save any log output from the run as an
artifact(which can be downloaded from the artifacts MATE REST endpoint) and set the task status accordingly. If you find that Manticore returns an error, please save and send us the logs!
Status of a Task¶
To check on the status, locate your unique task id (or query the status of the build id) and send a REST request to the tasks/{task_id} Mantiserve REST endpoint.
Furthermore, the logs for a task will be saved when the task stops execution. The artifact ID for the log is included during querying of a task status.
Killing a Task¶
To kill a Manitserve task, you must have the unique task id and then send an
HTTP PATCH request to the stop
Mantiserve REST endpoint.
See Strategies for Activating Mantiserve for deciding when it might be appropriate to kill a task.
Mantiserve Request Fields¶
{
"docker_image": "<docker_image>",
"docker_memory_limit_mb": 64,
"explore_msg": {
"command_line_flags": ["arg0", "arg1"],
"concrete_start": "",
"stdin_size": 256,
"env": {"ENV_VAR": "VAL"}
}
}
{
"docker_image": "<docker_image>",
"docker_memory_limit_mb": 64,
"reach_msg": {
"command_line_flags": ["arg0", "arg1"],
"concrete_start": "",
"stdin_size": 256,
"env": {"ENV_VAR": "VAL"}
"waypoints": [
{
"start": {
"va": 0
},
"end": {
"va": 0
},
"asserts": [
{
"location": {
"va": 0
},
"constraint": [
{
"expr": "string",
"id": [
{}
]
}
]
}
],
"replacements": [
{
"location": {
"va": 0
},
"model": {
"python_code": "string"
}
}
]
}
],
"constraint_vars": [
{
"name": "string",
"value": "string",
"expr": "string"
}
]
}
}
"docker_image": This optional field specifies the docker image that will be pulled where Mantiserve will insert a Manticore instance. This image must be valid with adocker pull <docker_image>. It is HIGHLY recommended to use a Docker image to isolate Manticore’s side-effects.If an image is not specified in the request, Mantiserve will use the corresponding CPG build’s Docker image, if the CPG build was performed within a Docker container. If the corresponding build does not have an image, Mantiserve will execute the request within the
mate_executorcontainer itself. (See Usage)
"docker_memory_limit_mb": This field specifies the memory limit, in MB, to impose when using Manticore within a Docker container. It will be set by default to 64 GB if no value is specified. (See Usage)"explore_msg"or"reach_msg": This field specifies the message with details for Explore and Reachability modes. (See Running a Task)
"command_line_flags": Arguments passed to the program (argv) at time of execution."stdin_size": When executing Manticore has a maximum number of purely symbolic (can be any value) bytes it can read from the stdin. This field specifies that number. If this is not specified the field defaults to 256. It is recommended to set this to a smaller number than 256 at the discretion of the user based on the program."concrete_start": This field specifies a string of readable concrete bytes the symbolic executor reads before any purely symbolic bytes are read (see"stdin_size"). If this is not specified only symbolic bytes are read."env": This field specifies a dictionary of environment variables that are available to the program of interest during execution."waypoints": This field contains a list ofWaypoints. EachWaypointcontainsAssertionsandReplacementsfor a block of code defined byva_startandva_end."constraint_vars": This field contains a list of initial declarations for symbolic variables.
Detectors¶
To use a detector with either the Exploration or
Reachability modes, add the "detector_options"
field to the request
"detector_options": {
"fast": true,
"detector": "UseAfterFree",
"poi_info": []
}
There are 3 types of Detectors available to Mantiserve tasks:
Variable Bounds Access Detector: Specify
"detector": "VariableBoundsAccess"within"detector_options"to use this field.
The Variable Bounds Access Detector searches for out of bounds memory access on the stack.
If specified, the detector will only look at given function to variable pairs, otherwise the detector will search for every possible out of bounds stack use and detect the first out of bounds access on each given path. When a vulnerability is found on a given path, the detector will return the function name, variable name, and file/line/binary address location information.
Uninitialized Stack Variable Detector: Specify
"detector": "UninitializedVariable"within"detector_options"to use this field.
The Uninitialized Stack Variable Detector searches for variables allocated on the stack and used prior to initialization.
If specified, the detector will only look inside a given function at a given variable, otherwise the detector will search the program for every possible uninitialized stack variable use, and only detect the first uninitialized use on each path. Thus, it’s best to specify this information if a target is in mind. When a vulnerability is found on a given path a detector will return the function name, variable name, and file/line/binary address location information.
Use After Free Detector: Specify
"detector": "UseAfterFree"within"detector_options"to use this field.
The Use After Free (UAF) Detector searches for and validates UAF vulnerabilities from calls to malloc and free.
If specified the detector will only search for UAF at a given free to use site pairs, otherwise the detector will detect the first UAF reachable in each path. When a vulnerability is found on a given path the detector will create a Manticore testcase with information about the allocation’s use, free, and allocation file/line/binary address location information.
Detector Target (POI) Information - If no target information (variable to function or use to free site) is specified, the detector will search for the first found vulnerability it is intended to detect on each path.
The "poi_info" field in a Mantiserve request specifies this
information. It accepts a list of dictionary objects specifying targets (See
Examples and Using a Detector with a POI Result). If omitted from the json request or specified as
"poi_info" : [] the detector will search with no target.
Detector Fast Mode - If specified the detector will stop and create a testcase and stop after the first vulnerability detection, otherwise Manticore will continue to search until the symbolic execution engine has finished (meaning all possible program paths have been explored).
The "fast" field in a Mantiserve request specifies this information. It
a boolean value; true to end on first detection and false to have
Mantiserve search until completion.
It is recommended to leave "fast" as true so that you get immediate
feedback when a detector detects something.
Using a Detector with a POI Result¶
The "poi_info" field specifies information to be shared with a detector for
validation of POI results. This can be used with an Exploration or
Reachability Mantiserve request.
For VariableBoundsAccess and UninitializedVariable Detectors this
field will look like a list of function to variable pairs
"poi_info": [
{
"function_name": "syscall_adjtimex",
"variable_name": "txc"
},
{
"function_name": "overflow_field",
"variable_name": "auth"
}
]
For UseAfterFree this field will look like a list of free to use sites
"poi_info": [
{
"use_file": "tmpp96vvx_w.c",
"use_line": 24,
"free_file": "tmpp96vvx_w.c",
"free_line": 20
},
{
"use_file": "tmpp96vvx_w.c",
"use_line": 25,
"free_file": "tmpp96vvx_w.c",
"free_line": 20
}
]
Example Queries¶
Explore Request with no Detector
{
"explore_msg": {
"path": "/tmp/UninitializedVariable",
"command_line_flags": [],
"concrete_start": "",
"stdin_size": 0,
"env": {}
}
}
Uninitialized Stack Variable Detector in Exploration Mode without POI Information
{
"explore_msg": {
"path": "/tmp/UninitializedVariable",
"command_line_flags": [],
"concrete_start": "",
"stdin_size": 0,
"env": {},
"detector_options": {
"fast": true,
"detector": "UninitializedVariable",
}
}
}
Uninitialized Stack Variable Detector in Exploration Mode with POI Information
{
"explore_msg": {
"path": "/tmp/UninitializedVariable",
"command_line_flags": [],
"concrete_start": "",
"stdin_size": 0,
"env": {},
"detector_options": {
"fast": true,
"detector": "UninitializedVariable",
"poi_info": [
{
"function_name": "syscall_adjtimex",
"variable_name": "txc"
}
]
}
}
}
Use After Free Detector in Exploration Mode with POI Information
{
"explore_msg": {
"path": "/tmp/UAF",
"command_line_flags": [],
"concrete_start": "A00000000ABCDEFGH.ppm\nB00000000ABCDEFGH.ppm\n",
"stdin_size": 0,
"env": {},
"detector_options": {
"fast": true,
"detector": "UseAfterFree",
"poi_info": [
{
"use_file": "tmpp96vvx_w.c",
"use_line": 166,
"free_file": "tmpp96vvx_w.c",
"free_line": 54
}
]
}
}
}
Example in Progress Request¶
When requesting the status of a running task a response similar to the following will return:
{
"task_id": "f3636f90a2de4293b0b6c7bfe35f89c9",
"build_id": "d01e95ffe06b44e78f391b2cd20e603a",
"state": "running",
"kind": "Explore",
"request_msg": {
"env": {},
"path": "/tmp/UAF",
"stdin_size": 0,
"concrete_start": "A00000000ABCDEFGH.ppm\nB00000000ABCDEFGH.ppm\n",
"detector_options": {
"fast": true,
"detector": "UseAfterFree",
"poi_info": []
},
"command_line_flags": []
},
"artifact_ids": [],
"response_msg": null,
"docker_image": null
}
The key things to note here are that the "state" field is "running"
and the "response_msg" field is null since Manticore is still in progress.
Example Query Results¶
When requesting the status of a completed task the
"state" field in the response will be set to "completed" and the
"response_msg" field will have the following fields:
"response_msg": {
"path": "/tmp/UAF",
"cases": []
}
where "path" is the to the binary being executed (inferred from the CPG build)
and "cases" is a list of the results. If the "cases" list is empty (like above) then
no results were found, otherwise it will contain a list of results with
"description", "symbolic_inputs", and "detector_triggered" fields. See
ExploreRet or ReachabilityRet for more details.
Successful Uninitialized Stack Variable with a result Detection
{
"task_id": "682c20e875eb4159890d35406be90b30",
"build_id": "350f6e0ffd714313b8d6c9a864c75158",
"state": "completed",
"kind": "Explore",
"request_msg": {
"env": {},
"path": "/tmp/UninitializedVariable",
"stdin_size": 0,
"concrete_start": "",
"detector_options": {
"fast": true,
"detector": "UninitializedVariable",
"poi_info": [
{
"function_name": "syscall_adjtimex",
"variable_name": "txc"
}
]
},
"command_line_flags": []
},
"artifact_ids": [
"d7b7bc165b1c4d379ea11c73562e5ee9"
],
"response_msg": {
"path": "/tmp/UninitializedVariable",
"cases": [
{
"description": "Found stack variable use before initialization txc.tai@'syscall_adjtimex' @ 0x4014b6! (/tmp/tmppisodovc.c:115)",
"symbolic_inputs": [],
"detector_triggered": "UninitializedVariable"
}
]
},
"docker_image": null
}
Successful Use After Free Run with a result Detection
{
"task_id": "a448ba792f434bb0be38e8d65a0aeb58",
"build_id": "0b314d269ee34f84a69981478bf4ecbe",
"state": "completed",
"kind": "Explore",
"request_msg": {
"env": {},
"path": "/tmp/UAF",
"stdin_size": 0,
"concrete_start": "A00000000ABCDEFGH.ppm\nB00000000ABCDEFGH.ppm\n",
"detector_options": {
"fast": true,
"detector": "UseAfterFree",
"poi_info": []
},
"command_line_flags": []
},
"artifact_ids": [
"339463dc77f54b22acec6e6036f56e1c"
],
"response_msg": {
"path": "/tmp/UAF",
"cases": [
{
"description": "Found use after free when reading address 0x425b00 @ 0x40160d (/tmp/tmpwy5w117e.c:166)! Allocated @ 0x4011f5 (/tmp/tmpwy5w117e.c:44). Deallocated @ 0x401273 (/tmp/tmpwy5w117e.c:54).",
"symbolic_inputs": [],
"detector_triggered": "UseAfterFree"
}
]
},
"docker_image": null
}
Completed Mantiserve Run with no Detections
{
"task_id": "31d16591696d44d9b0aa0cd98c892d5a",
"build_id": "d01e95ffe06b44e78f391b2cd20e603a",
"state": "completed",
"kind": "Explore",
"request_msg": {
"env": {},
"path": "/tmp/UAF",
"stdin_size": 0,
"concrete_start": "A00000000ABCDEFGH.ppm\nB00000000ABCDEFGH.ppm\n",
"detector_options": {
"fast": true,
"detector": "UseAfterFree",
"poi_info": [
{
"use_file": "badfile.c",
"use_line": 166,
"free_file": "badfile.c",
"free_line": 54
}
]
},
"command_line_flags": []
},
"artifact_ids": [
"303d53ae09464498816ad7806ca64bca"
],
"response_msg": {
"path": "/tmp/UAF",
"cases": []
},
"docker_image": null
}
Mantiserve Final States¶
Mantiserve tasks will have an associated state field in the returned object
from the tasks/{task_id}
Mantiserve REST endpoint. You will know that a task has stopped running when any
of the following states appear.
Failed - Mantiserve task was killed by a REST request (See Killing a Task) or Manticore encountered an unrecoverable error
Completed - Mantiserve either finished execution normally or found a detector result with
fastmode and exited early
Strategies for Activating Mantiserve¶
Using Fast Mode with a Detector
Mantiserve requests can be time consuming on large binaries, particularly if
using a detector with purely symbolic input. Specifying fast to true will
allow Manticore to notify immediately when a detection is made, instead
searching indefinitely.
Kill Mantiserve Tasks
After a significant amount of time has passed it might be advantageous to kill a Mantiserve task, view the logs, and give a more specific or different kind of request.
Mantiserve tasks can utilize a large amount of resources on large programs, so it is important to be aware the number of tasks currently running.
Specify a Target (POI Information) with a Detector
Providing detectors with a target (poi_info) ensures that a detector will
only look for that target or set of targets on a specific path, not returning
early with results that are not of interest. Additionally, in the case of the
Uninitialized Stack Variable Detector and the Variable Bounds Access Detector
specifying a target helps limit the functions and variables that are watched,
reducing overhead.
Developer Python API Documentation¶
See mantiserve for Python package documentation.