SMT2 formal verification of security-critical code paths
Max authentication tries bounded. auth_maxtries_exceeded() in auth.c checks against options.max_authtries.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun max_authtries () Int)
(assert
(<= max_authtries 100))
(assert
(>= max_authtries 1))
(assert
(or (< max_authtries 1) (> max_authtries 100)))
(check-sat)
SSH channel ID bounded. channel_by_id() in channels.c validates the ID against channels array.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun channel_id () Int)
(assert
(<= channel_id 65535))
(assert
(>= channel_id 0))
(assert
(or (< channel_id 0) (> channel_id 65535)))
(check-sat)
SSH packet length bounded to PACKET_MAX_SIZE (256*1024=262144). From ssh_packet_read_poll2() in packet.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun packet_len () Int)
(assert
(<= packet_len 262144))
(assert
(>= packet_len 5))
(assert
(or (< packet_len 5) (> packet_len 262144)))
(check-sat)
SSH key bit length bounded. sshkey_generate() in sshkey.c validates key size.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun key_bits () Int)
(assert
(<= key_bits 16384))
(assert
(>= key_bits 1024))
(assert
(or (< key_bits 1024) (> key_bits 16384)))
(check-sat)
SSH packet padding 4-255 bytes per RFC 4253 §6. From ssh_packet_read_poll2() in packet.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun padding_len () Int)
(assert
(<= padding_len 255))
(assert
(>= padding_len 4))
(assert
(or (< padding_len 4) (> padding_len 255)))
(check-sat)
KEX proposal string length bounded to prevent memory exhaustion. From kex_input_kexinit() in kex.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun kex_proposal_len () Int)
(assert
(<= kex_proposal_len 32768))
(assert
(>= kex_proposal_len 1))
(assert
(or (< kex_proposal_len 1) (> kex_proposal_len 32768)))
(check-sat)
MaxStartups bounded 1-1024 to limit concurrent unauthenticated connections. From fill_default_server_options() in servconf.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun max_startups () Int)
(assert
(<= max_startups 1024))
(assert
(>= max_startups 1))
(assert
(or (< max_startups 1) (> max_startups 1024)))
(check-sat)
LoginGraceTime defaults to 120s, bounded 1-3600 to ensure finite auth timeout. From fill_default_server_options() in servconf.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun login_grace_time () Int)
(assert
(<= login_grace_time 3600))
(assert
(>= login_grace_time 1))
(assert
(or (< login_grace_time 1) (> login_grace_time 3600)))
(check-sat)
MaxSessions defaults to 10, bounded 1-1024 to limit session multiplexing per connection. From fill_default_server_options() in servconf.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun max_sessions () Int)
(assert
(<= max_sessions 1024))
(assert
(>= max_sessions 1))
(assert
(or (< max_sessions 1) (> max_sessions 1024)))
(check-sat)
ClientAliveCountMax defaults to 3, bounded 0-256 to limit missed keepalives before disconnect. From fill_default_server_options() in servconf.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun client_alive_count_max () Int)
(assert
(<= client_alive_count_max 256))
(assert
(>= client_alive_count_max 0))
(assert
(or (< client_alive_count_max 0) (> client_alive_count_max 256)))
(check-sat)
ClientAliveInterval defaults to 0 (disabled), bounded 0-3600s to prevent excessively long keepalive intervals. From fill_default_server_options() in servconf.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun client_alive_interval () Int)
(assert
(<= client_alive_interval 3600))
(assert
(>= client_alive_interval 0))
(assert
(or (< client_alive_interval 0) (> client_alive_interval 3600)))
(check-sat)
PerSourceNetBlockSize IPv4 mask defaults to 32 (single host), bounded 0-32 to ensure valid CIDR prefix length for per-source rate limiting. From fill_default_server_options() in servconf.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun per_source_masklen_ipv4 () Int)
(assert
(<= per_source_masklen_ipv4 32))
(assert
(>= per_source_masklen_ipv4 0))
(assert
(or (< per_source_masklen_ipv4 0) (> per_source_masklen_ipv4 32)))
(check-sat)
PerSourceNetBlockSize IPv6 mask defaults to 128 (single host), bounded 0-128 to ensure valid CIDR prefix length for per-source rate limiting. From fill_default_server_options() in servconf.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun per_source_masklen_ipv6 () Int)
(assert
(<= per_source_masklen_ipv6 128))
(assert
(>= per_source_masklen_ipv6 0))
(assert
(or (< per_source_masklen_ipv6 0) (> per_source_masklen_ipv6 128)))
(check-sat)
MaxStartups rate (connection drop probability percentage) defaults to 30, bounded 0-100 to ensure valid percentage. From fill_default_server_options() in servconf.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun max_startups_rate () Int)
(assert
(<= max_startups_rate 100))
(assert
(>= max_startups_rate 0))
(assert
(or (< max_startups_rate 0) (> max_startups_rate 100)))
(check-sat)
PerSourcePenalties minimum penalty duration defaults to 15s, bounded 0-3600 to prevent negative or absurdly long minimum penalties for misbehaving clients. From fill_default_server_options() in servconf.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun penalty_min () Int)
(assert
(<= penalty_min 3600))
(assert
(>= penalty_min 0))
(assert
(or (< penalty_min 0) (> penalty_min 3600)))
(check-sat)