Software vulnerabilities detected during code analysis with ESBMC-WR tool
Hello,
4 potential software vulnerabilities were found in code. To identify this kind of vulnerabilities I used tool ESBMC-WR: https://github.com/thalestas/esbmc-wr
More about the tool: https://arxiv.org/pdf/2102.02368.pdf
Please, check the logs of analysis:
Expected behaviour Our main objective was to check memory safety properties (e.g., pointer dereference and memory leaks) while performing the verification code.
Issue 1
[FILE] Utilities/cmbzip2/unzcrash.c
State 3 file unzcrash.c line 86 function main thread 0
Violated property: file unzcrash.c line 86 function main dereference failure: array bounds violated
State 1 file unzcrash.c line 66 function flip_bit thread 0
byteno = -135264256 (11110111 11110000 00001000 00000000)
State 2 file unzcrash.c line 71 function flip_bit thread 0
Violated property: file unzcrash.c line 71 function flip_bit array bounds violated: array `zbuf' lower bound (signed long int)byteno >= 0
Issue 2
[FILE] Utilities/cmbzip2/bzip2.c
State 1 file bzip2.c line 942 function fileExists thread 0
tmp = 0
State 2 file bzip2.c line 943 function fileExists thread 0
exists = (unsigned char)(0 != ( struct _IO_FILE *)0)
State 4 file syserr.c line 4 function strerror thread 0
errnum = -2147483648 (10000000 00000000 00000000 00000000)
State 5 file syserr.c line 108 function strerror thread 0
Violated property: file syserr.c line 108 function strerror array bounds violated: array `sys_errlist' lower bound (signed long int)errnum >= 0
Issue 3
[FILE] Utilities/cmzstd/lib/common/xxhash.c
State 1 file xxhash.c line 84 function XXH_free thread 0
Violated property: file xxhash.c line 84 function XXH_free dereference failure: invalid pointer freed
Issue 4
[FILE] Source/cm_utf8.c
State 1 file cm_utf8.c line 46 function cm_utf8_decode_character thread 0
first = invalid-object + 1
State 2 file cm_utf8.c line 46 function cm_utf8_decode_character thread 0
Violated property: file cm_utf8.c line 46 function cm_utf8_decode_character dereference failure: invalid pointer