saferewrite-20250228.tar.gz browse
For usage instructions, see README in the package.
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.
Archives and changelog
saferewrite-20250228.tar.gz browse
Added elfulator option to be able to handle sparc32 for C code.
Added README-elfulator to explain installation.
Switched to handling all cross-compilation targets in a single run, including equivalence tests across targets. List of compilers now covers amd64, arm64 (aarch64), arm32 (armeabi), mips64, x86, and sparc32 (sparcv8).
More documentation changes:
added README-analysis to explain how to interpret results;
added README-resources with notes on resource consumption;
improved README.
Turned on satvalidation1,
so SMT solving is used to find differences
(as a test of SMT solving)
even when differences are found by random tests.
Added self-test for first implementation-compiler pair, as another test of SMT solving.
Added analysis/passed-valgrind.
Added some support for architectures files.
Switched to binary formats (with same endianness as target, auto-detected from compiler test)
for inputs and outputs to analysis-angr and analysis-execute.
Switched from multiprocessing to os.fork() for unrolling and equivalence testing.
Switched to passing unrolled through disk instead of RAM.
Ported to newer angr version (9.2.102), and pinned that version for now.
Adjusted options passed to angr,
notably to enable unicorn
(but, to work around unicorn engine bugs,
stopping unicorn as soon as there's a read from stdin).
Switched to .merge for state merging.
Disabled maybe-uninitialized warnings for analysis-valgrind.
Built in memcmp and bcmp.
Added support for Reverse.
Increased maxsplit to 300.
Added automatic increase of RLIMIT_NOFILE.
Bumped to cryptoint 20250228.
Simplified bottomzeros_num/ref.
Synchronized signedness between cmp_64xint16/api and cmp_64xint16/bitopscpp/verify.cc.
Added .note.GNU-stack for cmp_64xint16/openssl/memcmp.s.
Added architectures for cmp_64xint16/openssl.
saferewrite-20241004.tar.gz browse
Bumped to cryptoint 20241003.
Added load_bigendian and store_bigendian functions.
saferewrite-20240807.tar.gz browse
Bumped to cryptoint 20240806.
Added _01 functions.
Added _topbit functions.
Added support for return values from Rust.
Added verify_8, inc128big, uint8_7bit_nonzero_mask_int16.
Renamed positive_mask/shift2 as positive_mask/shift2optbug.
saferewrite-20240622.tar.gz browse
Ported to 32-bit hosts,
and added support for TARGET=arm32 cross-compilation.
Bumped to latest development version of supercopnew functions.
saferewrite-20240620.tar.gz browse
Added preliminary support for cross-compilation, in particular TARGET=arm64.
Added more int* and uint* functions.
Added supercopnew implementations. (These are going into SUPERCOP.)
Renamed some intentionally buggy implementations to say bug in the name.
Extended unsafe-randomtest to also note the differing outputs.
Added tracking of signed vs. unsigned through data storage and prototypes.
saferewrite-20240515.tar.gz browse
Added C++ support, and a cmp_64xint16/bitopscpp example.
Included libmceliece-20240513 versions of many int* and uint* functions,
and ref versions of the functions not previously included.
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
https://github.com/angr/angr/pull/2887.
saferewrite-20210903.tar.gz browse
Original release.
Version: This is version 2025.02.28 of the "Downloads" web page.
