updated plugin.json

README.md

@@ -12,7 +12,7 @@ The plugin adds the following commands:
 ---
 
 More APIs can be executed through the python shell. For example, we can use the solver to _prove_ a condition for the current state:
-```
+``` python
 >>> import seninja
 >>> s = seninja.get_current_state()
 >>> s.solver.satisfiable(extra_constraints=[s.regs.eax == 3])

plugin.json

@@ -9,7 +9,7 @@
       "python3"
    ],
    "description": "Symbolic execution plugin for BinaryNinja",
-   "longdescription": "# SENinja - Symbolic Execution Plugin for Binary Ninja\n![](https://raw.githubusercontent.com/borzacchiello/seninja/master/pictures/screenshot.png)\nThis is a binary ninja plugin that implements a symbolic execution engine based only on z3, highly inspired by the _angr framework_ (https://angr.io/). \nThe plugin is implemented as an emulator of LLIL instructions that builds and manipulates z3 formulas. \n\nSENinja simulates a debugger: the execution is _path driven_, only one state is _active_ and executes instructions. The other states, generated at branches, are saved in a _deferred queue_. At any time, the active state can be changed with a deferred one.\n\nRefer to [this survey](https://arxiv.org/pdf/1610.00502.pdf) if you want to know more about symbolic execution.\n\n### Commands\n![](https://raw.githubusercontent.com/borzacchiello/seninja/master/pictures/commands.png)\n\nThe plugin adds the following commands, accessible through the GUI:\n- `Start symbolic execution`: can be executed by right-clicking on an instruction. The command creates a symbolic state at the current address. By default, the uninitialized registers and memory locations are considered symbolic (this can be changed in the settings). This new state becomes the active state, highlighted in green on the disassembly graph.\n- `Change current state`: can be executed by right-clicking on a deferred state (highlighted in red on the disassembly graph). The deferred state becomes the new active state. If more than one state is at that address, the last one that reached the address becomes the active state.\n- `Step`: when executed, the active state executes one instruction.\n- `Continue until branch`: when executed, the active state executes instructions until a _symbolic_ branch is reached, i.e., until the state _forks_ in two states.\n- `Continue until address`: can be executed by right-clicking on an address. The active state will execute instructions until it reaches the target address. Notice that there is no search algorithm implemented: the active state will simply follow _true_ branches (if it can choose). If you use this command, be sure that the state will actually reach the instruction, otherwise it will loop.\n- `Merge states`: can be executed by right-clicking on the active state. The command will _merge_ all the deferred states that share the same instruction pointer with the active state. Note that the solver can become significantly slower while reasoning on a merged state. \n- `Reset symbolic execution`: this command resets symbolic execution. It clears the GUI and releases active and deferred states.\n\n---\n\nMore APIs can be executed through the python shell. For example, we can use the solver to _prove_ a condition for the current state:\n```\n>>> import seninja\n>>> s = seninja.get_current_state()\n>>> s.solver.satisfiable(extra_constraints=[s.regs.eax == 3])\n```\nthe code will check the satisfiablity of `eax == 3` given the path constraint of the active state.\n\n### Settings\n\nSENinja gives to the user the possibility to configure many parts of the symbolic engine (e.g. dimension of pages, symbolic memory access strategy, etc.). \nAll the available settings can be accessed and modified by clicking on `Edit/Preferences/Settings` and selecting `SENinja` in the left widget.\n\n### UI Widgets\n\nSENinja comes with two widgets that can be used to visualize the registers and a portion of memory of the active state. The widgets are disabled by default, but can be activated by clicking on `View/Show SENinja Registes` and `View/Show SENinja Memory`. \n\n#### Register View\n![](https://raw.githubusercontent.com/borzacchiello/seninja/master/pictures/register_view.png)\n\nThe Register View can be used to visualize the value of the registers of the active state. The value of a register can be modifyied by double-clicking on it. The right-click menu allows to:\n- Copy the content of the register\n- Concretize the value of the register\n- Evaluate the value of the register using the solver\n- Inject symbols\n- Show the register expression\n\n#### Memory View\n![](https://raw.githubusercontent.com/borzacchiello/seninja/master/pictures/memory_view.png)\n\nThe Memory View can be used to visualize the value of a portion of memory of the active state. By clicking on \"monitor memory\", the user can specify a memory address to monitor. The widget will show 512 bytes starting from that address. \nThe memory view is splitted in two sections: an hexview and an ascii view. The hexview shows the hex value of each byte only if the byte is mapped and concrete. If the byte is unmapped, the characted `_` is shown; if the byte is symbolic, the widget shows the character `.`. \n\nDouble-clicking on a byte allows the user to modify its value in the active state.\nThe right-click menu allows to:\n- Copy the selection (in various format, e.g. little-endian, binary, etc.)\n- Concretize the value of the selection\n- Evaluate the value of the selection using the solver\n- Inject symbols\n\n#### Use Case - FLARE-ON 6, Challenge 11 (AVX2 Virtual Machine)\n\nThis section shows how _SENinja_ can be used to solve challenge 11 of  _flare-on 6_ challenge in an automatic way. \nThe challenge can be downloaded at [flare-on 2019](https://www.fireeye.com/blog/threat-research/2019/09/2019-flare-on-challenge-solutions.html).\n\nThe challenge implements a `base64` decoder, obfuscated with a virtual machine based on `AVX2`. \n\nThe `main` function of the binary can be found at the address `0x140001220`. \nAfter checking whether the cpu supports `AVX2`, the binary reads two command line arguments:\n- the first one with a length between 5 and 32 bytes\n- the second one with a length of exactly 32 bytes.\n\nLooking at `0x1400016cd`, we can see that the first argument must be equal to `FLARE2019`. \nWe can use SENinja to compute the 32 bytes of the second argument.\n\nWe can start by creating a new state in `main` function, just after the `cpuid` checks at address `0x140001293` (right click on the address, `SENinja/Start symbolic execution`).\n\nThen, we can setup argv from the python shell:\n``` python\nimport seninja\ns = seninja.get_current_state()\n\ninp0 = seninja.BVV(0x464c4152453230313900, 10*8)  # create concrete string FLARE2019\ninp1 = seninja.BVS('inp', 32*8).Concat(seninja.BVV(0, 8))  # create symbolic string of 32 bytes\n\nargv = s.mem.allocate(24)  # allocate argv\ninp0_p = s.mem.allocate(10)  # allocate argv[1]\ninp1_p = s.mem.allocate(32)  # allocate argv[2]\ns.mem.store(argv+8, seninja.BVV(inp0_p, 64), 'little')\ns.mem.store(argv+16, seninja.BVV(inp1_p, 64), 'little')\ns.mem.store(s.regs.rsp+0x1488, seninja.BVV(argv, 64), 'little')\ns.mem.store(inp0_p, inp0)\ns.mem.store(inp1_p, inp1)\n```\n\nNow, we can limit `inp1` to have only alphanumeric characters:\n``` python\nfor i in range(1, 33):\n    b = inp1.Extract((i+1)*8-1, i*8)\n    s.solver.add_constraints(seninja.Or(\n        seninja.And(\n            ord(\"a\") <= b, b <= ord(\"z\")\n        ),\n        seninja.And(\n            ord(\"A\") <= b, b <= ord(\"Z\") \n        ),\n        seninja.And(\n            ord(\"0\") <= b, b <= ord(\"9\")\n        )\n    ))\n```\n\nWe have set up the state. We can continue symbolic execution until a symbolic branch is reached (right click, `SENinja/Continue until branch`).\nAfter a few seconds (~20), SENinja will stop at `0x14000178a`. As we can see, the engine generated a deferred state at `0x14000169d` with a reference to the string `This is correct`.\n![](https://raw.githubusercontent.com/borzacchiello/seninja/master/pictures/flareon-11.png)\n\nWe can select this state (right click, `SENinja/Select current state`) and, from the shell, we can compute the correct command line argument:\n``` python\ns = seninja.get_current_state()\nseninja.int_to_str(s.solver.evaluate(inp1).value)\n```\n\nwhich is\n```\ncHCyrAHSXmEKpyqoCByGGuhFyCmy86Ee\n```\n\nIndeed, running the program with\n\n`$ wine vv_max.exe FLARE2019 cHCyrAHSXmEKpyqoCByGGuhFyCmy86Ee`\n\nwe obtain the flag:\n```\nThat is correct!\nFlag: [email protected]\n``` \n\n[here](https://drive.google.com/open?id=13qFmoFow9OA-l3v4TpS7_4YM88drxM5P), you can download a video that shows the process.\n\n#### Limitations\nOne main limitation of the plugin is the fact that the _status register_ is not explicitly modeled for every instructions, but is computed only when the analyses of binary ninja discovers that its value is needed for the computation of a certain condition. \nWhile this approach works for the vast majority of situations, the emulation becomes inaccurate if the stautus register is used in a way that binary ninja does not predict (e.g., if the value of the status register is used accross function boundaries).\nThis is a limitation of LLIL. To fix this, SENinja should use the LiftedIL instead of LLIL, implementing architecture-dependent status-flag handlers for every instructions.\n\n\nAnother main limitation of the plugin is given by the fact that system calls and external functions must be handled with handly written models (similarly to angr). While I have implemented some models (you can find them in the `models` subfolder), they are far from being complete. When SENinja reaches an unmodeled syscall or external function, it raises an exception.\n\n\nFinally, even if most of the code is architecture-independent, to support a new architecture SENinja needs some information that must be manually specified (e.g., list of registers, calling conventions, etc.). You can find examples in the `arch` subfolder. Furthermore, some instructions are not modeled by LLIL (e.g. most AVX2 instructions), so that instructions must be handled in an architecture-dependent way. You can find the models for AVX2 instructions as a reference in `arch/arch_x86_64_sph.py`.\nCurrently, SENinja (partially) supports `x86`, `x86_64` and `ARMv7`.\n\n#### Version and Dependencies\nTested with \n- binary ninja `1.2.2001-dev` with personal license\n- python `3.6.9` \n- z3 `4.8.7`\n\nTo make it work, you need to install z3 with pip:\n`$ pip3 install z3-solver`\n",
+   "longdescription": "# SENinja - Symbolic Execution Plugin for Binary Ninja\n![](https://github.com/borzacchiello/seninja/raw/master/pictures/screenshot.png)\nThis is a binary ninja plugin that implements a symbolic execution engine based only on z3, highly inspired by the _angr framework_ (https://angr.io/). \nThe plugin is implemented as an emulator of LLIL instructions that builds and manipulates z3 formulas. \n\nSENinja simulates a debugger: the execution is _path driven_, only one state is _active_ and executes instructions. The other states, generated at branches, are saved in a _deferred queue_. At any time, the active state can be changed with a deferred one.\n\n### Commands\nThe plugin adds the following commands:\n![](pictures/commands.png)\n\n---\n\nMore APIs can be executed through the python shell. For example, we can use the solver to _prove_ a condition for the current state:\n\n``` python\n>>> import seninja\n>>> s = seninja.get_current_state()\n>>> s.solver.satisfiable(extra_constraints=[s.regs.eax == 3])\n```\n\nthe code will check the satisfiablity of `eax == 3` given the path constraint of the active state.\n\nConsult the [wiki](https://github.com/borzacchiello/seninja/wiki) to have more info about the commands.\n\n### Settings\n\nSENinja gives to the user the possibility to configure many parts of the symbolic engine (e.g. dimension of pages, symbolic memory access strategy, etc.). \nAll the available settings can be accessed and modified by clicking on `Edit/Preferences/Settings` and selecting `SENinja` in the left widget.\n\n### UI Widgets\n\nSENinja comes with two widgets that can be used to visualize the registers and a portion of memory of the active state. The widgets can be activated by clicking on `View/Show SENinja *`. \n\n#### Buffers View\n![](https://github.com/borzacchiello/seninja/raw/master/pictures/buffers_view.png)\nThis widget allows the creation of buffers containing symbolic data.\n\n#### Register View\n![](https://github.com/borzacchiello/seninja/raw/master/pictures/register_view.png)\n\nThe Register View can be used to visualize the value of the registers of the active state. The value of a register can be modifyied by double-clicking on it. The right-click menu allows to:\n- Copy the content of the register\n- Concretize the value of the register\n- Evaluate the value of the register using the solver\n- Inject symbols\n- Show the register expression\n- Set the register to the address of a buffer created with the buffer view\n\n#### Memory View\n![](https://github.com/borzacchiello/seninja/raw/master/pictures/memory_view.png)\n\nThe Memory View can be used to visualize the value of a portion of memory of the active state. By clicking on \"monitor memory\", the user can specify a memory address to monitor. The widget will show 512 bytes starting from that address. \nThe memory view is splitted in two sections: an hexview and an ascii view. The hexview shows the hex value of each byte only if the byte is mapped and concrete. If the byte is unmapped, the characted `_` is shown; if the byte is symbolic, the widget shows the character `.`. \n\nDouble-clicking on a byte allows the user to modify its value in the active state.\nThe right-click menu allows to:\n- Copy the selection (in various format, e.g. little-endian, binary, etc.)\n- Concretize the value of the selection\n- Evaluate the value of the selection using the solver\n- Inject symbols\n\n#### Version and Dependencies\nTested with \n- binary ninja `2.1` with personal license\n- python `3.6.9` \n- z3 `4.8.7`\n\nTo make it work, you need to install z3 with pip:\n`$ pip3 install z3-solver`\n",
    "license": {
       "name": "2-Clause BSD",
       "text": "Copyright 2019 Luca Borzacchiello\n\nRedistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:\n\n1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.\n\n2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.\n\nTHIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS \"AS IS\" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE."
@@ -24,6 +24,6 @@
       "Windows": "Install `z3-solver` using pip: `pip install z3-solver`",
       "Linux": "Install `z3-solver` using pip: `pip install z3-solver`"
    },
-   "version": "0.1",
-   "minimumbinaryninjaversion": 2001
+   "version": "0.2",
+   "minimumbinaryninjaversion": 2100
 }