Post-Quantum Software Research Center

attackntrw-20220829.tar.gz browse

For usage instructions, see README in the package.

libsecded-20220828.tar.gz browse

For usage instructions, see README in the package.

nttcompiler-20220411.tar.gz browse

For usage instructions, see nttcompiler page.

saferewrite-20211125.tar.gz browse

For usage instructions, see README in the package.

Archives and changelog

saferewrite-20211125.tar.gz browse

Renamed int32_{negative,nonzero,positive,smaller}mask as int32_{negative,nonzero,positive,smaller}_mask. Added int32_equal_mask, int32_unequal_mask, int32_zero_mask. Added int32_min, int32_max.

Added int32_sort2/openssh implementation (to check some code from OpenSSH), int32_positive_mask/shift4 implementation, 10 int32*/supercop implementations.

Added uint32_zero_mask, uint32_nonzero_mask, uint32_equal_mask, uint32_unequal_mask, uint32_smaller_mask, uint32_min, uint32_max, and uint32_sort2, with ref and supercop implementations.

saferewrite-20210915.tar.gz browse

Important workaround for angr issue: Set claripy.Solver timeout of 4294967295 milliseconds. The issue is that angr's satisfiable treats z3.unknown as False (along with treating z3.unsat as False and treating z3.sat as True), triggering equals in cases that Z3 has not verified. By default Z3 will return z3.unknown after a timeout of 300000 milliseconds.

Disable most of the claripy simplifiers to speed up unrolling.

If random tests fail, skip SMT solving by default; controlled by internal satvalidation1 option.

Introduce internal maxsplit to limit number of universes for unrolling; reaching the limit will trigger unrollerror. Current limit is 100.

More serious, but still preliminary, support for simulation as double-check on unrolling.

Preliminary Rust support. Simplest example is int32_sort2/rust.

Add sha256_200bytes and sha512_300bytes examples, including sha512_300bytes/rust_sha2_097 to see the tests automatically catching the recent SHA-512 AVX2 bugs in version 0.9.7 of the Rust sha2 crate. Beware that on some machines the sha256 example will trigger angr decoding failures for SHA instructions.

Add int32_sort2/compilebug and int32_sort2/linkbug examples as tests of failure cases.

Move some slow examples out of the way for now: core_{weight,wforce}* and decode_*{1531,4591}.

Support divisions. Add divmod14 and divsigned examples.

Add warning-mul and warning-div.

saferewrite-20210904.tar.gz browse

If assertions are triggered in evaluation double-check, generate warning-valuesfailed and continue into Z3 rather than stopping.

Add various src/*/README reflecting further successes after the angr updates in

saferewrite-20210903.tar.gz browse

Original release.

Version: This is version 2022.08.29 of the "Downloads" web page.