cyruliu/dynamite

A dynamic analyzer for proving program termination and non-termination.

Dynamite

Installation

1. Install SageMath from conda (http://doc.sagemath.org/html/en/installation/conda.html)

   wget https://repo.anaconda.com/miniconda/Miniconda2-latest-Linux-x86_64.sh
   sh Miniconda2-latest-Linux-x86_64.sh
   conda config --add channels conda-forge
   conda create -n sage sage=8.8 python=2.7
   

2. conda activate sage

3. Install Java 8 from conda:

   conda install -c anaconda openjdk

   conda install openjdk=8.0.192

4. pip install lark-parser

5. pip install z3-solver

6. JavaPathFinder

   mkdir jpf
   cd jpf/
   git clone https://github.com/javapathfinder/jpf-core
   git clone https://github.com/SymbolicPathFinder/jpf-symbc
   mkdir /root/.jpf
   echo 'jpf-core = /jpf/jpf-core' >> /root/.jpf/site.properties
   echo 'jpf-symbc = /jpf/jpf-symbc' >> /root/.jpf/site.properties
   echo 'extensions=${jpf-core},${jpf-symbc}' >> /root/.jpf/site.properties
   cp /dynamo/deps/dig/src/java/InvariantListenerVu.java ../jpf-symbc/src/main/gov/nasa/jpf/symbc/
   cd jpf-core/
   git checkout java-8
   ant
   cd ../jpf-symbc/
   ant
   

7. ENV

   export JPF_HOME=/jpf
   export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:$JPF_HOME/jpf-symbc/lib
   

8. LLDB

   conda install -c conda-forge lldb
   

Note

1. Remove a conda environment: conda env remove --name myenv

2. Search a conda package: conda search sage --channel conda-forge

3. Install pip: sudo easy_install pip

4. LLDB

   breakpoint set --name main
   breakpoint set --func-regex vtrace* # BreakpointCreateByRegex('vtrace*', None)
   run
   expr -i 0 -- mainQ(1, 2)
   frame variable
   

   • https://www.nesono.com/sites/default/files/lldb%20cheat%20sheet.pdf
   • https://opensource.apple.com/source/lldb/lldb-159/www/python-reference.html
   • https://lldb.llvm.org/use/python-reference.html#
   • https://developer.apple.com/library/archive/documentation/IDEs/Conceptual/gdb_to_lldb_transition_guide/document/lldb-terminal-workflow-tutorial.html

   opt = lldb.SBExpressionOptions()
   opt.SetIgnoreBreakpoints(False)
   v = target.EvaluateExpression('mainQ(1, 2)', opt)
   

   • https://stackoverflow.com/questions/49532342/lldb-python-callback-on-breakpoint-with-sbtarget-evaluateexpression
   • To use lldb in docker:

   docker run --cap-add=SYS_PTRACE --security-opt seccomp=unconfined --security-opt apparmor=unconfined --name dynamo-dev -it letonchanh/dynamo-dev bash
   

   • LLVM-9 (http://releases.llvm.org/9.0.0/clang+llvm-9.0.0-x86_64-linux-gnu-ubuntu-18.04.tar.xz) and SageMath are incompatible on the Python six package.
   • Build LLVM

   apt-get install cmake ninja-build build-essential subversion swig libedit-dev libncurses5-dev
   unset PYTHONPATH
   git clone https://github.com/llvm/llvm-project.git
   cd llvm-project
   mkdir build
   cd build
   cmake -G Ninja -DLLVM_ENABLE_PROJECTS="clang;lldb" -DPYTHON_EXECUTABLE="/tools/SageMath/local/bin/python3" -DLLDB_CAN_USE_LLDB_SERVER=True -DCMAKE_INSTALL_PREFIX=/tools/llvm -DCMAKE_BUILD_TYPE=Release ../llvm
   ninja lldb
   ninja lldb-server
   

5. angr

   • https://breaking-bits.gitbook.io/breaking-bits/vulnerability-discovery/automated-exploit-development/analyzing-functions

Support

This work is supported by Office of Naval Research under Grant No.: N00014-17-1-2787.