search

kokke / tiny-regex-c

Small portable regex in C
The Unlicense
1.21k stars 174 forks source link

Software vulnerabilities detected during code analysis with ESBMC-WR tool #76

Closed janislley closed 1 year ago

janislley commented 2 years ago

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

janislley commented 1 year ago

This issue was fixed and fix provided.