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 

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

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