SMT2 formal verification of security-critical code paths
SSL record data length ≤ MBEDTLS_SSL_IN_CONTENT_LEN (16384). From ssl_parse_record_header() in ssl_msg.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun data_len () Int)
(assert
(<= data_len 16384))
(assert
(>= data_len 0))
(assert
(or (< data_len 0) (> data_len 16384)))
(check-sat)
Ciphertext length bounded during decryption. From mbedtls_ssl_decrypt_buf() in ssl_msg.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun ct_len () Int)
(assert
(<= ct_len 16384))
(assert
(>= ct_len 0))
(assert
(or (< ct_len 0) (> ct_len 16384)))
(check-sat)
TLS major version must be 3 (covers SSL3.0 through TLS1.3). From ssl_parse_record_header().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun tls_major () Int)
(assert
(<= tls_major 3))
(assert
(>= tls_major 3))
(assert
(or (< tls_major 3) (> tls_major 3)))
(check-sat)
TLS minor version: 0=SSL3.0, 1=TLS1.0, 2=TLS1.1, 3=TLS1.2, 4=TLS1.3. From ssl_parse_record_header().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun tls_minor () Int)
(assert
(<= tls_minor 4))
(assert
(>= tls_minor 0))
(assert
(or (< tls_minor 0) (> tls_minor 4)))
(check-sat)
TLS record content type: 20=ChangeCipherSpec, 21=Alert, 22=Handshake, 23=AppData, 24=Heartbeat. From ssl_check_record_type().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun tls_content_type () Int)
(assert
(<= tls_content_type 24))
(assert
(>= tls_content_type 20))
(assert
(or (< tls_content_type 20) (> tls_content_type 24)))
(check-sat)
TLS record header is exactly 5 bytes (content_type + version_hi + version_lo + length_hi + length_lo).
; benchmark generated from python API
(set-info :status unknown)
(declare-fun record_header_len () Int)
(assert
(<= record_header_len 5))
(assert
(>= record_header_len 5))
(assert
(or (< record_header_len 5) (> record_header_len 5)))
(check-sat)
TLS handshake message uses a uint24 length field (max 16,777,215). From mbedtls_ssl_read_record().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun handshake_msg_len () Int)
(assert
(<= handshake_msg_len 16777215))
(assert
(>= handshake_msg_len 0))
(assert
(or (< handshake_msg_len 0) (> handshake_msg_len 16777215)))
(check-sat)
Handshake parsing requires at least mbedtls_ssl_hs_hdr_len(ssl) bytes before reading type/length; records shorter than 4 bytes are rejected in mbedtls_ssl_read_record() in ssl_msg.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun in_msglen () Int)
(assert
(>= in_msglen 4))
(assert
(< in_msglen 4))
(check-sat)
TLS handshake message type is validated against known message types (0..24). From mbedtls_ssl_parse_handshake_header() in ssl_msg.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun handshake_type () Int)
(assert
(<= handshake_type 24))
(assert
(>= handshake_type 0))
(assert
(or (< handshake_type 0) (> handshake_type 24)))
(check-sat)
Alert records must be exactly 2 bytes (level + description). From mbedtls_ssl_handle_message_type() in ssl_msg.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun in_msglen () Int)
(assert
(<= in_msglen 2))
(assert
(>= in_msglen 2))
(assert
(or (< in_msglen 2) (> in_msglen 2)))
(check-sat)
Alert level is validated as warning(1) or fatal(2) before alert handling logic in mbedtls_ssl_handle_message_type() in ssl_msg.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun alert_level () Int)
(assert
(let (($x5 (= alert_level 2)))
(let (($x12 (= alert_level 1)))
(or $x12 $x5))))
(assert
(let (($x5 (= alert_level 2)))
(let (($x12 (= alert_level 1)))
(let (($x18 (or $x12 $x5)))
(not $x18)))))
(check-sat)
ChangeCipherSpec records must be exactly 1 byte in TLS/DTLS. From mbedtls_ssl_handle_message_type() in ssl_msg.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun in_msglen () Int)
(assert
(<= in_msglen 1))
(assert
(>= in_msglen 1))
(assert
(or (< in_msglen 1) (> in_msglen 1)))
(check-sat)
ChangeCipherSpec payload must be exactly 0x01; any other value is rejected in mbedtls_ssl_handle_message_type() in ssl_msg.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun ccs_content_byte () Int)
(assert
(<= ccs_content_byte 1))
(assert
(>= ccs_content_byte 1))
(assert
(or (< ccs_content_byte 1) (> ccs_content_byte 1)))
(check-sat)
DTLS Connection ID API rejects CID lengths above MBEDTLS_SSL_CID_IN_LEN_MAX (32). From mbedtls_ssl_conf_cid() in ssl_tls.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun len () Int)
(assert
(<= len 32))
(assert
(>= len 0))
(assert
(or (< len 0) (> len 32)))
(check-sat)
DTLS unexpected CID policy must be ignore(0) or fail(1). From mbedtls_ssl_conf_cid() in ssl_tls.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun ignore_other_cid () Int)
(assert
(<= ignore_other_cid 1))
(assert
(>= ignore_other_cid 0))
(assert
(or (< ignore_other_cid 0) (> ignore_other_cid 1)))
(check-sat)
ECJPAKE handshake setup rejects empty passwords (pw_len == 0) in mbedtls_ssl_set_hs_ecjpake_password() in ssl_tls.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun pw_len () Int)
(assert
(>= pw_len 1))
(assert
(< pw_len 1))
(check-sat)