kokke
Software vulnerabilities detected during code analysis with ESBMC-WR tool
Hello,
One potential software vulnerability was found in code. To identify this kind of vulnerabilities I used ESBMC-WR tool: https://github.com/thalestas/esbmc-wr We detect it during code exploitation for RUFUS tool. A bug was reported at this time and the developer of RUFUS tool requested to solve this potential issue directly here in mainline code.
Bug reported at RUFUS repository code: https://github.com/pbatard/rufus/issues/1856
More about the tool: https://arxiv.org/pdf/2102.02368.pdf
Expected behavior:
Our main objective was to check memory safety properties (e.g., pointer dereference and memory leaks) while performing the verification code.
Please, check the logs of analysis:
Issue [FILE] src/re.c
State 5 file re.c line 269 function re_print thread 0 Violated property: file re.c line 269 function re_print array bounds violated: array `types' upper bound (signed long int)(pattern + (signed long int)i)->type < 17
