trailofbits / manticoreui Goto Github PK

Acceptance Criteria:

• The plugin should call the GetMessageList and GetStateList rpcs at appropriate intervals
• The state_list_widget and binja log should be appropriately updated

Right now hooks are tied to a specific address, but manticore also supports adding hooks that apply to all instructions executed.

Example:

# None: The hook will be applied to all the instructions
@m.hook(None)
def record_trace(state):
    pass

This would get MUI's feature set closer to that of manticore and should be useful to users as well.

Why:

Evelyn needs to know what Manticore detected and wants this data presented in MUI

Acceptance Criteria:

• Evelyn is able to right-click on a completed Manticore state and can select view the results for that state
• The summary results viewer of that state is opened
• The results of a detector (example: Integer overflow) are shown in a scrollable window
• The results viewer shows the ID of the state and you can copy the ID
• Evelyn can close the result viewer when she's done

From: trailofbits/manticore#2434

Manticore has models for common library functions. These help to improve performance, as opposed to symbolically executing the instructions of the original function.

Adding a command to apply these models would be helpful to expose these features to users less familiar with manticore.

Additionally, we could leverage on the Binary Ninja analysis API to try to apply these function models automatically (perhaps with a warning/prompt for the user).

Documentation for usage of function models: https://github.com/trailofbits/manticore/blob/master/docs/native.rst#function-models

As of commit c6b9ac5 the MUI Server now uses protobuf version ~=3.20

This means that we can safely support Explicit Field Presence (https://github.com/protocolbuffers/protobuf/blob/main/docs/field_presence.md) - most notably by denoting specific fields as optional - this helps make the proto spec clearer for devs, and exposes the HasField API method so we don't have to manually set defaults to make them unambiguous

Implement the features in #67 and #70 but for mui server

What:

Natalie needs some guidance for running MUI and exploring it's features

Acceptance Criteria:

• TBD once a several initial issues are complete

What:

Ghidra is written in Java, which presents a challenge for interaction with Manticore written in Python.

We want to first develop a prototype Ghidra plugin that will appear similarly to the Binary Ninja plugin but written for Ghidra in Java.

This will initially exist as a separate repository because it's a prototype. The features will be very light in terms of MUI capabilities, but will at least support starting Manticore with an arbitrary command line argument list from a Ghidra UI component and then piping Manticore's output to a Ghidra UI component. The user will also be able to stop Manticore.

Acceptance Criteria:

• A Ghidra plugin repository that has basic documentation for building, running, and deploying MUI-Ghidra
• A plugin menu item to open a window for Manticore initialization
• A window popup to write a CLI argument list for Manticore, pre-populated with the path to the currently opened binary, and also has a "Run" button to start execution
• A logging UI screen that pops into existence after hitting "Run" to show Manticore's output
• A stop button in the logging UI screen that will kill the Manticore process
• George is able to complete the above on his Linux machine (native binaries will need to appear at os/linux_x86_64 )
• N/A George is able to complete the above on his Mac machine (native binaries will need to appear at os/mac_x86_64) Removing this because supporting the running of Linux binaries on Mac detracts from other important goals. Manticore also can't process Mach-o binaries.

Shiv might be useful for packaging Manticore into an executable.

From #1

Similar to how pause is implemented (#67), it could be helpful if we could kill/abandon a state through the UI while manticore is solving.

This should be useful in scenarios where we've identified undesired states that are:

• In infinite loops / long loops
• In "bad" code paths, but we don't want to stop a long running manticore instance to add an avoid hook
• Hogging resources

Why:

Natalie can provide concrete data so that Manticore doesn't waste time

AC:

• Natalie can provide a serialized state and seed the run with it in the configuration dialog
• When Natalie click run, Manticore will start with the initial seed in its state list
• The seed state is validated to ensure the appropriate/matching binary is loaded in MUI, otherwise Natalie sees an error pop-up stating why it isn't possible to run

NOTES

Natalie can write a Manticore script that raises a SerializeState exception to generate the initial state seed that should be loaded.

Natalie could also choose a state from a previous MUI run to use as the seed.

From: trailofbits/manticore#2441

Right now, find and avoid hooks in ghidra will highlight the disassembly green/red accordingly. But this is not done for custom hooks. Without highlighting it's less obvious to the user that a custom hook exists at that disassembly line.

What

Natalie needs to be able to pause and restart a state

AC

• Natalie can right-click on a running state in the side-bar and click pause
• When she clicks pause the state is paused and is moved to a paused state list
• The state should be flagged as paused
• If Natalie right-clicks on a paused state it she is given the option to restart the state
• When she clicks restart the state is moved to waiting list

From: trailofbits/manticore#2436

What:

Natalie would like some guidance on where to start with MUI's features

Acceptance Criteria:

• Natalie can refer to the README to have an idea of what features are available
• The features that Natalie should explore first are highlighted to her
• Natalie has a few selected screenshots for reference

Closed by #24

Currently when we use the Solve with manticore functionality, manticore will start and the background process indicator will show in the bottom right corner, but this is not very obvious when looking at the logs. Similarly, when manticore exits without hitting any find/avoids, it will just quietly stop the worker threads with not much information to the user.

I think it would be beneficial to add the following logging messages:

1. Start of manticore solve
2. End of manticore solve
   • After hitting a find
   • WITHOUT hitting a find

I think timestamps could be useful as well (so that we can track how long manticore has been running), but I'm not sure if we want that.

Supersedes #81

Discussed with @lordidiot and agreed that implementing the ability to:

• Create multiple custom hooks on the same address, and
• Edit custom hooks via right-click menu in the hook list
  (similar to what was implemented in #77)

would be useful

There is a mismatch between the behaviour of the Ghidra and Binary Ninja plug-ins.

Ghidra
If a custom hook exists at address A, creating a custom hook at A again creates a new custom hook at the same address.

Binary Ninja
If a custom hook exists at address A, trying to create a custom hook at A again will edit the old custom hook.

I think the way binary ninja does it is more convenient for the user as they can edit their past mistakes/update their custom hooks. However, it may be useful to also support adding multiple hooks on the same address to partition out functionally different custom hooks that are needed on the same address.

What:
A minimal implementation such that the Binja plugin can interact with a running MUICore binary on localhost and a hardcoded port, and Start/Terminate a single instance of Manticore.

Acceptance Criteria:

• The plugin should include generated protobuf/grpc code based off the proto spec in the MUI-Ghidra repo on build
• The plugin should include a MUICore binary on build
• The plugin should call the StartNative rpc when attempting to start Manticore execution on a native binary
• The plugin should call the StartEVM rpc when attempting to start Manticore execution on a smart contract
• The plugin should call the Terminate rpc when attempting to stop Manticore execution

Once chess branch logging changes have been merged into master, the Binja plugin on master will need some edits - the current state will not successfully log output.

You can refer to this PR trailofbits/ManticoreUI-Ghidra#21 on how the logging updates should work. Specifically, a custom handler may have to be created and attached to the manticore logger object.

It would be helpful to have an additional window in MUI that would list the find/avoid/hooks that have been added to the project. Currently, users have to search through the disassembly to find existing hooks that have been implemented. This overall view should improve usability of the tool.

Basic features:

• Listing of find/avoid/hooks
• Double click to reach the address in disassembler view

Additional(?) features:

• Remove individual find/avoid/hooks
• Enable/disable to temporarily pause specific find/avoid/hooks

What:

MUI exists as a Binary Ninja plugin that can be installed from the plugin manager

Acceptance Criteria:

• Evelyn can open Binary Ninja, navigate to the plugin manager and find MUI listed and install (see #16)
• The plugin will automatically install Manticore upon installation from Binary Ninja plugin manager (see above)
• A menu for configuring MUI appears under the "Tools" menu
• Evelyn can do this on her Mac machine
• Evelyn can do this on her Linux machine

From: trailofbits/manticore#2431

What

Natalie can keep track of state explosion and have an overall view of progress

AC

• At the top of the MUI sidebar Natalie can view summary of the current state conditions
• Natalie can view a counter of the
  • Number of completed states
  • Number of errored states
  • Number of running states
  • Number of waiting states

See: trailofbits/manticore#2435

Allow hooks to be named, this will aid hook management when the db complexity starts to increase.

Why

Evelyn needs to know where manticore is executing in a given state

AC

• When Evelyn double clicks on a running state the instruction currently being executed is highlighted
• When she clicks on a paused, waiting, or completed state the last instruction executed is highlighted
• When she double clicks on a errored state a pop up saying we have no instruction info

From: trailofbits/manticore#2438

Acceptance Criteria:

• the TargetAddress rpc service should be called when selecting addresses to find/avoid in the Binja context menu
• the hooks should be appropriately reflected in the Hook List widget and in the disassembly view

Notes:

• current MUICore implementation of find/avoid probably won't play well with bndb, at this point I'd prefer modifying MUICore's implementation to have instance-specific hooks (or maybe hooks passed alongside the Start rpc?)

Why:

George wants to better understand the state exploration

AC:

• George can right-click on a state and asks for its provenance tree
• A graph is shown of all its ancestor states in a single list (because we only care about the number of forks)
  • The nodes are the ID and the current instruction
• George can click the ancestor state node to navigate to that instruction that caused the fork

Questions

Do we know the next instruction of a forked state?

From: trailofbits/manticore#2439

From #5

as per #61 (comment)

Why

George needs to know where manticore is executing in a given state

AC

• When George double clicks on a running state the instruction currently being executed is highlighted
• When he clicks on a paused, waiting, or completed state the last instruction executed is highlighted
• When he double clicks on a errored state a pop up saying we have no instruction info

From #6

Why:

Evelyn wants to be confident that her analysis has covered the important parts of her target.

AC:

• Evelyn can right-click on any non-errored state and select view coverage
• Binary Ninja will clear all previous coverage highlights
• Binary Ninja will highlight the basic blocks that have been executed
• Evelyn is navigated to the last executed instruction

Implementation Question

• Should we only clear highlights that MUI added?

From: trailofbits/manticore#2440

During initial exploration of a target, it is easier to specify points of interest with the UI, but if a user wants to write additional logic or even just have the ability to run the same logic from the command-line, then they should be able to do that.

One way to do this would be to export a sort of human-readable configuration file that represents the state of the current Manticore configuration, as specified through the UI.

The configuration file could be passed to a new tool that would do some Python code generation to create a Manticore script that would be used as a starting point for writing more logic. The layout and fields of the configuration file should probably follow closely with the upcoming MUICore messages in the hope that eventually a UI could also be initialized.

The implementation for the codegen isn't decided but there are templating engines that would be good to look at first, like Jinja.

What:

George would like sensible defaults so that he can run MUI with as little clicks as possible

Acceptance Criteria:

• George can launch a UI
• In the UI, he can launch a new Manticore project
• A configuration dialog pops up
• The configuration dialog has sensible defaults for all supported Manticore options
• The configuration dialog allows George to customize Manticore's input
• After clicking OK (without changing anything), Manticore runs
• After clicking OK (with changing Manticore's input), Manticore runs
• After clicking OK (with changing Manticore's input to an invalid value), a relevant error message is shown to George

What:

Natalie would like to easily see the vulnerability locations from a detector result

Acceptance Criteria:

• Natalie can select a result and is brought to the relevant vulnerability location(s)
• Natalie can see the vulnerability location(s) are highlighted

Design:

TBD

What:

Evelyn would like sensible defaults so that she can run MUI with as little clicks as possible

Acceptance Criteria:

• Evelyn can launch a UI
• In the UI, she can launch a new Manticore project
• A configuration dialog pops up
• The configuration dialog has sensible defaults
  • The EVM contract is loaded in the UI already
• After clicking OK (without changing anything), Manticore runs

Design:

TBD

To be discussed:

• What happens with multiple contracts?
• What are good defaults for EVM?

From: trailofbits/manticore#2430

Implement the feature in #58 but for the mui server - Ghidra/Binja-integration support can come in a subsequent PR

Why:

Natalie needs to know what's running and its status.

Acceptance Criteria:

• When Manticore is running, a MUI side-panel is shown
• The side-panel shows a list of states and their status
  • We show what is currently being executed by Manticore as an "Active" state in the list
  • We show a queued state as "Waiting" in the list
  • We show a forked state as "Forked" in the list
  • We show a state that has exited normally as "Complete"
  • We show a state that has exited in any other way as "Errored"
• Natalie can see the ID of the state in the list
• The status and states are updated at an interval
• Natalie can scroll to see all of the states

Note:

We have some initial implementation for Manticore introspection for the TUI feature.

From: trailofbits/manticore#2433

We would like to set up MUI with a relatively normal Python package directory structure, but Binary Ninja plugin manager can't be configured to use a subdirectory in a Git repo.

We should open an issue to see how difficult it would be to do this.

Ethersplay also has this issue and directs users to install it manually.

What

Currently, Binja plugin users are restricted to the options presented in the Run Dialogs. There should be an additional field where users who are more familiar with Manticore can choose to supply CLI arguments for greater control over Manticore execution.

This issue is chiefly for the muicore integration branch, but may also be relevant to the existing master implementation.

Acceptance Criteria - MUICore

• An additional text field in the respective Run Dialogs for Native / EVM analysis
• The cli-style additional arguments should be passed to the StartNative/StartEVM rpc services
• Docs: update README images to show and explain the new field

Acceptance Criteria - master

• An additional text field in the respective Run Dialogs for Native / EVM analysis
• The cli-style additional arguments should be appropriately parsed, likely directly through the argparsing code in Manticore or through a modified copy that will be included with the plugin
• Docs: update README images to show and explain the new field

What:

George would like some guidance on where to start with MUI's features

Acceptance Criteria:

• George can refer to the README to have an idea of what features are available
• The features that George should explore first are highlighted to him
• George has a few selected screenshots for reference

What:

Natalie would like sensible defaults so that she can run MUI with as little clicks as possible

Acceptance Criteria:

• Natalie can launch a UI
• In the UI, she can launch a new Manticore project
• A configuration dialog pops up
• The configuration dialog has sensible defaults
• The configuration dialog allows Natalie to customize Manticore's input
• After clicking OK (without changing anything), Manticore runs
• After clicking OK (with changing Manticore's input), Manticore runs
• After clicking OK (with changing Manticore's input to an invalid value), a relevant error message is shown to Natalie

Design:

TBD

To be discussed:

• Constrained symbolic input interface

Why:

George needs to know what's running and its status.

Acceptance Criteria:

• When Manticore is running, a MUI side-panel is shown
• The side-panel shows a list of states and their status
  • We show what is currently being executed by Manticore as an "Active" state in the list
  • We show a queued state as "Waiting" in the list
  • We show a forked state as "Forked" in the list
  • We show a state that has exited normally as "Complete"
  • We show a state that has exited in any other way as "Errored"
• George can see the ID of the state in the list
• The status and states are updated at an interval
• George can scroll to see all of the states

Note:

We have some initial implementation for Manticore introspection for the TUI feature.

We are going to need to generate Java code from the protobuf specification for Manticore's introspection data

From: #2

As of the change that introduces the Hook List component as part of the MUI Setup component, on a fresh install of the plugin the component looks like this:

The current layout is patched together by a series of borderlayouts and gridbaglayouts. We should overhaul this so that it's more easily maintainable and the component is more appropriately laid out and sized

George is presented a right-click menu option to either 'find' or 'avoid' and instruction, which will color the instruction in a color to represent the selection.

To keep the PRs smaller, this issue is only for the UI component. Upon clicking, George should be presented with an "Unimplemented" message.

What

Natalie can pause and restart manticore or stop the manticore run

AC

• Natalie can go to the tools menu and all states not running are moved to the pause list and all currently running states finish
• When Natalie attempts to pause all states a pop up dialog shows to confirm
• She can go to the tools menu and select restart to move all states from the pause list to the waiting list
• Natalie can select stop from the tools menu to
  • Forcefully kill all running states
  • Move waiting and paused states to error
  • Nothing happens to completed states
  • The timer is stopped
  • The UI remains open after this process is complete
• When Natalie attempts to stop all states a pop up dialog shows to confirm

From: trailofbits/manticore#2437

Ensure that configurable Manticore settings like find/avoid instruction are able to be saved in a Binary Ninja Database so that when Binary Ninja is saved and closed, it can reopened and loaded with the same Manticore state to continue where you left off.

This would make it easier to share databases between people.

What:

Natalie is notified that MUI does not support her Mac machine when trying to run a native binary.

Acceptance Criteria

• When Natalie tries to launch a native application for MUI, it notifies her that Mac is not supported and that operation is only currently supported on Linux platforms

Notes

Related to #1 (trailofbits/manticore#2431)

From: trailofbits/manticore#2432

Why:

Evelyn wants to better understand the state exploration

AC:

• Evelyn can right-click on a state and asks for its provenance tree
• A graph is shown of all its ancestor states in a single list (because we only care about the number of forks)
  • The nodes are the ID and the current instruction
• Evelyn can click the ancestor state node to navigate to that instruction that caused the fork

Questions

Do we know the next instruction of a forked state?

From: trailofbits/manticore#2439

Closed by #22

MUI was initially developed for Binary Ninja, but with Ghidra support, we will need some way to reduce the duplication of data constants like colors, data structures, and supported interaction commands.

The implementation should be easily supported across various languages and ideally support code generation for those languages (for data structure definitions).

During development of Ghidra, we should note any of these features that are shared with Binary Ninja.

After completion of #35 we need to implement the backend logic that Manticore will use to process the 'find' and 'avoid' commands.

This backend will likely be a grpc service.

Upon reaching a 'find' instruction, Manticore will print the solution to all symbolic variables in that state and then kill all remaining states. A state that reaches an 'avoid' instruction will terminate itself (which helps with state explosion).

See this code snippet for more info on Manticore handling