Created attachment 3599 [details] memory property violations Hello, We found some potential code failures that might cause a security vulnerability. To identify this kind of vulnerability I used tool ESBMC-WR: https://github.com/thalestas/esbmc-wr More about the tool: https://arxiv.org/pdf/2102.02368.pdf Our main objective was to check memory safety properties (e.g., pointer dereference and memory leaks) while performing the verification code. Failures found: Bug 01: packet.c, ssh_set_newkeys, ssh_set_newkeys , line 948 ,division by zero State 40 file packet.c line 948 function ssh_set_newkeys thread 0 ---------------------------------------------------- Violated property: file packet.c line 948 function ssh_set_newkeys division by zero (unsigned long int)enc->block_size != 0 Bug 02: logintest.c, main, main , line 288 ,dereference failure: array bounds violated State 5 file logintest.c line 288 function main thread 0 ---------------------------------------------------- Violated property: file logintest.c line 288 function main dereference failure: array bounds violated Bug 03: cipher-chachapoly.c, chachapoly_get_length, chachapoly_get_length , line 135 ,dereference failure: invalid pointer State 1 file cipher-chachapoly.c line 135 function chachapoly_get_length thread 0 ---------------------------------------------------- Violated property: file cipher-chachapoly.c line 135 function chachapoly_get_length dereference failure: invalid pointer Bug 04: sshkey.c, fingerprint_bubblebabble, fingerprint_bubblebabble , line 1081 ,dereference failure: array bounds violated State 6 file sshkey.c line 1081 function fingerprint_bubblebabble thread 0 ---------------------------------------------------- Violated property: file sshkey.c line 1081 function fingerprint_bubblebabble dereference failure: array bounds violated If you need any other information, please ask me. I also attached a file containing others property violations found using our tool. But it will need time to check if it is all false positives.
Most of these are completely obvious false positives. E.g. > State 6 file sshkey.c line 1081 function fingerprint_bubblebabble thread 0 > ---------------------------------------------------- > Violated property: > file sshkey.c line 1081 function fingerprint_bubblebabble > dereference failure: array bounds violated The array is allocated to be sufficiently sized literally in the previous line. Please forgive my bluntness, but low quality reports like this do nothing but waste our time - there is no discernable signal among the noise. Please do not submit more unless they have been assessed by a human.
Closing bugs from openssh-9.1 release cycle
OpenSSH 9.3 has been released. Close resolved bugs