djbsort

djbsort includes tools that, given an array size, automatically verify correctness of djbsort's output for all possible input arrays of that size. These tools have three parts:

The time to run the whole sequence of tools gradually increases with the array size. For array size 512, running the whole sequence of tools to verify int32/avx2 takes about 35 seconds on one core of kizomba, a 3GHz Kaby Lake Intel Xeon E3-1220 v6. More than 90% of this time is for symbolic execution.

Internally, the verifier has two components:

Installing angr and verifying djbsort

The patches contributed by djbsort to angr (see below) have not yet been integrated into angr, so you must install angr from source.

The following instructions were tested on a virtual machine (created with xen-create-image) running the latest release ("unstable") of Debian.

As root, install various libraries and development packages:

    dpkg --add-architecture i386
    apt update
    apt dist-upgrade -y
    apt install \
      man wget strace psmisc screen vim time git tig \
      build-essential clang gdb valgrind nasm cmake \
      libffi-dev libssl-dev libxml2-dev libxslt1-dev \
      libreadline-dev libpixman-1-dev libqt4-dev \
      libglib2.0-dev python-dev python2.7-dev pypy \
      python3 python-pip virtualenvwrapper pypy-dev \
      libtool debootstrap debian-archive-keyring \
      binutils-multiarch libc6:i386 libgcc1:i386 \
      libstdc++6:i386 libtinfo5:i386 zlib1g:i386 \
      multiarch-support gcc-multilib \
      -y

As the user that compiled djbsort, install the latest version of angr:

    cd
    git clone https://github.com/angr/angr-dev.git
    cd angr-dev
    mkvirtualenv -p /usr/bin/pypy angr
    workon angr
    setsid -w sh -c ./setup.sh < /dev/null

The angr installation takes under 10 minutes and finishes with a comforting "All done!" announcement.

Apply the djbsort patches to angr:

    cd $HOME/angr-dev/angr
    wget https://sorting.cr.yp.to/angrpatch1.txt
    patch -p1 < angrpatch1.txt
    cd $HOME/angr-dev/claripy
    wget https://sorting.cr.yp.to/angrpatch3.txt
    patch -p1 < angrpatch3.txt

Run the verifymany script to verify sorting for all small sizes:

    workon angr
    pip install pyparsing
    cd
    version=$(cat sorting.cr.yp.to/djbsort-latest-version.txt)
    cd djbsort-$version/verif
    ./verifymany

The verifymany script stops with an error message if it encounters any failures.

The angr patches

Description of the patches contributed by djbsort to angr:


Version: This is version 2018.07.17 of the "Verification" web page.