Bug 3452

Summary:

Potential Software vulnerabilities detected using ESBMC-WR tool

Product:

Portable OpenSSH

Reporter:

janislley <janislley>

Component:

ssh

Assignee:

Assigned to nobody <unassigned-bugs>

Status:

CLOSED INVALID

Severity:

security

CC:

djm

Priority:

Version:

8.8p1

Hardware:

Other

OS:

Linux

Attachments:

Description	Flags
memory property violations	none

Description janislley 2022-06-26 16:06:15 AEST

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.

Comment 1 Damien Miller 2022-06-27 09:31:51 AEST

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.

Comment 2 Damien Miller 2022-10-04 21:59:27 AEDT

Closing bugs from openssh-9.1 release cycle

Comment 3 Damien Miller 2023-03-17 13:37:02 AEDT

OpenSSH 9.3 has been released. Close resolved bugs