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:
unroll: An unroller that, given the compiled djbsort library, produces a fully unrolled program for arrays of the specified size. This converter is a small Python script built on top of the angr symbolic-execution tool introduced in the following paper: Yan Shoshitaishvili, Ruoyu Wang, Christopher Salls, Nick Stephens, Mario Polino, Audrey Dutcher, John Grosen, Siji Feng, Christophe Hauser, Christopher Kruegel, Giovanni Vigna, "SoK: (State of) The Art of War: Offensive Techniques in Binary Analysis", IEEE Symposium on Security and Privacy, 2016. This tool, in turn, builds upon the VEX library inside Valgrind.
minmax: A peephole optimizer that converts the fully unrolled program to a sequence of "min" and "max" operations. To simplify this optimizer, djbsort has contributed some optimization patches to angr.
decompose: A verifier that proves that the min-max program is a sorting program.
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
takes about 35 seconds
on one core of
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:
Decompose the min-max program into presumed 2-way-merging programs. The tool does not require the merge to be a merge of inputs on the left with inputs on the right; it allows arbitrary interleaving of the two lists of inputs (and djbsort uses interleaving for vectorizability). However, the 2-way-merging structure is essential; more general sorting programs cannot be verified with the current tool.
Verify each presumed 2-way-merging program, by testing the program on a linear-size list of inputs. For example, a min-max program correctly merges all sequences of 3 inputs with all sequences of 5 inputs if and only if it correctly merges 0 1 2 with 3 4 5 6 7; 0 1 7 with 2 3 4 5 6; 0 6 7 with 1 2 3 4 5; and 5 6 7 with 0 1 2 3 4.
The fact that a quadratic-size list of test bits is enough for a merging network (whereas the best known methods to test a general sorting network are much slower) is noted in Knuth's Art of Computer Programming. The fact that larger test inputs allow a linear-size list (analogously to an older speedup by Yao for general sorting networks) was pointed out in the following paper: Moon Jung Chung, B. Ravikumar, "Bounds on the size of test sets for sorting and related networks", Discrete Mathematics, 1990. However, the test set stated in that paper is too small (off by one). A correct test set appears in the following paper: Guy Even, Tamir Levi, Ami Litman, "Optimal conclusive sets for comparator networks", Theoretical Computer Science, 2009. Both of these papers consider only the balanced case, merging n/2 inputs with n/2 inputs, but the idea generalizes immediately to other cases.
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
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
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
verifymany script stops with an error message
if it encounters any failures.
The angr patches
Description of the patches contributed by djbsort to angr:
angrpatch1.txt: Support the AVX2
vpunpckinstructions. Otherwise angr will crash on djbsort.
angrpatch2.txt: Superseded by
angrpatch3.txt: Various peephole optimizations. Specifically: C idiom for signedmin; C idiom for signedmax;
concat(y,x)if lengths are multiples of 8;
concat(0,x)if lengths are multiples of 8; same for any combinations of reversals and zeros;
loware multiples of 8;
concat(a,b) ^ concat(c,d)⇒
concat(a^c,b^d)if sizes match;
concat(a,b) & concat(c,d)⇒
concat(a&c,b&d)if sizes match;
Version: This is version 2018.07.17 of the "Verification" web page.