invd

Ultimate crashes with OOM for array[8192]

2

When re-testing the code described in #366 with * `svcomp-DerefFreeMemtrack-32bit-Automizer_Bitvector.epf` * `AutomizerMemDerefMemtrack.xml` settings with the newest Ultimate 6392f50fb9ff6daa998daa33f79eb2c3746cdafb, Ultimate subprocesses run into an **out of memory** condition: ``` * Results...

SMTLIBException: std::bad_alloc in singletracecheck.TraceCheck

6

This issue is likely strongly related to #414. When run against a version of the #366 program with an array size of `4096` and settings of * `svcomp-DerefFreeMemtrack-32bit-Automizer_Bitvector.epf` * `AutomizerMemDerefMemtrack.xml`...

cvc4 can grow to consume all system memory

1

Even for short programs, cvc4 can spiral out of control and consume all system memory, leading to general system instability, since Ultimate does not enforce (or periodically check) any cvc4...

lack of padding model for unpacked structs leads to soundness issues

2

After some short tests and discussion with @danieldietsch, I have the impression that Ultimate currently has no model in place to calculate the actual memory contents and memory footprint of...

MemorySanitizer reports `use-of-uninitialized-value`. Shortened report, obtainable with `-fsanitize=memory -fsanitize-memory-track-origins`: ``` ==12522==WARNING: MemorySanitizer: use-of-uninitialized-value #0 0x505817 in nsvg__minf /nanosvg/src/./nanosvg.h:228:64 #1 0x5025f5 in nsvg__curveBounds /nanosvg/src/./nanosvg.h:573:14 #2 0x4f6fb5 in nsvg__addPath /nanosvg/src/./nanosvg.h:1069:3 #3 0x4c1510...

Undefined Behavior in nsvg__pathArcTo()

1

During fuzzing, UndefinedBehaviorSanitizer reports an issue at https://github.com/memononen/nanosvg/blob/07a5e2a33c999c759490c2ca452e18ec24c0bfb3/src/nanosvg.h#L2166 ``` nanosvg.h:2175:10: runtime error: nan is outside the range of representable values of type 'int' SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior nanosvg.h:2175:10 in ``` I...

Consider using stack canaries via -fstack-protector* flags

2

From what I can see in the Nitrokey Pro source code, the firmware currently does not use or support the ARM GCC provided standard functionality to mitigate certain stack buffer...

undefined behavior: signed integer overflow in minmea_scan()

9

Fuzzing with libFuzzer shows that the following multiplication can lead to undefined behavior: https://github.com/kosma/minmea/blob/06ad5a18406c6219290be8c82f966ab585571858/minmea.c#L186 UndefinedBehavior Sanitizer warning: ``` minmea.c:186:39: runtime error: signed integer overflow: 1000000000 * 10 cannot be represented...

Improve trezor-crypto fuzzer

2

Improve existing fuzzer harnesses Add new fuzz testing of Monero, BIP39, segwit address and ECDH related functions Add special Memory Sanitizer checks Use new fuzzer input marking functionality Additional documentation...

Unreliable arming button in C firmware

1

First of all, @nezza thank you for the C firmware! On my unit, it's hit-or-miss whether pressing the "arming" button actually toggles the arming state as intended. In my impression,...