[Bug 3452] New: Potential Software vulnerabilities detected using ESBMC-WR tool

[bugzilla-daemon at mindrot.org]

https://bugzilla.mindrot.org/show_bug.cgi?id=3452

            Bug ID: 3452
           Summary: Potential Software vulnerabilities detected using
                    ESBMC-WR tool
           Product: Portable OpenSSH
           Version: 8.8p1
          Hardware: Other
                OS: Linux
            Status: NEW
          Severity: security
          Priority: P5
         Component: ssh
          Assignee: unassigned-bugs at mindrot.org
          Reporter: janislley at gmail.com

Created attachment 3599
  --> https://bugzilla.mindrot.org/attachment.cgi?id=3599&action=edit
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.

-- 
You are receiving this mail because:
You are watching the assignee of the bug.