SMT2 formal verification of security-critical code paths
DSA signature DER decoding requires non-negative length. Extracted from ossl_dsa_sign_int() in dsa_sign.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun len () Int)
(assert
(>= len 0))
(assert
(< len 0))
(check-sat)
EVP cipher key length must be 1-64 bytes. From EVP_CIPHER_CTX_set_key_length() in evp_enc.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun key_len () Int)
(assert
(<= key_len 64))
(assert
(>= key_len 1))
(assert
(or (< key_len 1) (> key_len 64)))
(check-sat)
BIGNUM bit count bounded to prevent excessive computation. From BN_num_bits() in bn_lib.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun num_bits () Int)
(assert
(<= num_bits 16384))
(assert
(>= num_bits 0))
(assert
(or (< num_bits 0) (> num_bits 16384)))
(check-sat)
X.509 version: v1=0, v2=1, v3=2. From X509_set_version() in x509_set.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun x509_version () Int)
(assert
(<= x509_version 2))
(assert
(>= x509_version 0))
(assert
(or (< x509_version 0) (> x509_version 2)))
(check-sat)
TLS wire version: SSL3.0=0x0300 through TLS1.3=0x0304. From tls_process_server_hello() in statem_clnt.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun tls_version () Int)
(assert
(<= tls_version 772))
(assert
(>= tls_version 768))
(assert
(or (< tls_version 768) (> tls_version 772)))
(check-sat)
TLS record type constrained to CCS(20), Alert(21), Handshake(22), AppData(23), Heartbeat(24). From ssl3_read_bytes() in rec_layer_s3.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun record_type () Int)
(assert
(<= record_type 24))
(assert
(>= record_type 20))
(assert
(or (< record_type 20) (> record_type 24)))
(check-sat)
TLS record length bounded to 2^14 payload plus protocol overhead to limit malformed oversized records. From ssl3_get_record() in rec_layer_s3.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun record_len () Int)
(assert
(<= record_len 18432))
(assert
(>= record_len 0))
(assert
(or (< record_len 0) (> record_len 18432)))
(check-sat)
ServerHello session ID length constrained to 0-32 bytes per TLS limits to prevent malformed session parsing paths. From tls_process_server_hello() in statem_clnt.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun session_id_len () Int)
(assert
(<= session_id_len 32))
(assert
(>= session_id_len 0))
(assert
(or (< session_id_len 0) (> session_id_len 32)))
(check-sat)
TLS alert level constrained to warning(1) or fatal(2) to reject malformed alert records and unreachable alert handling paths. From ssl3_read_bytes() in rec_layer_s3.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun alert_level () Int)
(assert
(<= alert_level 2))
(assert
(>= alert_level 1))
(assert
(or (< alert_level 1) (> alert_level 2)))
(check-sat)
ServerHello compression method constrained to null(0) to reject deprecated compression and reduce CRIME-style attack surface in modern TLS paths. From tls_process_server_hello() in statem_clnt.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun compression () Int)
(assert
(<= compression 0))
(assert
(>= compression 0))
(assert
(and (distinct compression 0) true))
(check-sat)
Consecutive warning-alert counter constrained to 0-5 (MAX_WARN_ALERT_COUNT) to model OpenSSL's anti-alert-flood guardrail before hard failure. From ssl3_read_bytes() in rec_layer_s3.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun s->rlayer.alert_count () Int)
(assert
(<= s->rlayer.alert_count 5))
(assert
(>= s->rlayer.alert_count 0))
(assert
(or (< s->rlayer.alert_count 0) (> s->rlayer.alert_count 5)))
(check-sat)
TLS alert description constrained to the 8-bit wire domain (0-255) before alert-specific branching, preventing out-of-domain values from propagating through alert handling logic. From ssl3_read_bytes() in rec_layer_s3.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun alert_descr () Int)
(assert
(<= alert_descr 255))
(assert
(>= alert_descr 0))
(assert
(or (< alert_descr 0) (> alert_descr 255)))
(check-sat)
ServerHello legacy_version (sversion) constrained to SSL3.0..TLS1.3 wire range (0x0300-0x0304) before version negotiation logic, preventing out-of-domain protocol values from entering client-version selection paths. From tls_process_server_hello() in statem_clnt.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun sversion () Int)
(assert
(<= sversion 772))
(assert
(>= sversion 768))
(assert
(or (< sversion 768) (> sversion 772)))
(check-sat)
DTLS HelloVerifyRequest cookie length constrained to uint8 wire domain (0-255) from PACKET_get_length_prefixed_1 before copy into state, preventing oversized/out-of-domain cookie handling paths. From dtls_process_hello_verify() in statem_clnt.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun cookie_len () Int)
(assert
(<= cookie_len 255))
(assert
(>= cookie_len 0))
(assert
(or (< cookie_len 0) (> cookie_len 255)))
(check-sat)
Server-selected ciphersuite must exist in the client-advertised cipher stack; sk_SSL_CIPHER_find() index is constrained to be non-negative before acceptance, preventing unadvertised/unknown cipher selection paths. From set_client_ciphersuite() in statem_clnt.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun i () Int)
(assert
(>= i 0))
(assert
(< i 0))
(check-sat)
TLS 1.3 NewSessionTicket processing requires a positive handshake digest size before converting to size_t for HKDF label expansion, preventing invalid/zero digest-length resumption-nonce paths. From tls_process_new_session_ticket() in statem_clnt.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun hashleni () Int)
(assert
(>= hashleni 1))
(assert
(< hashleni 1))
(check-sat)