SMT2 formal verification of security-critical code paths
HTTP/2 header field length must be non-negative. From ngx_http_v2_state_field_len() in ngx_http_v2.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun len () Int)
(assert
(>= len 1))
(assert
(< len 0))
(check-sat)
HTTP status code must be 100-599. From ngx_http_parse_status_line() in ngx_http_parse.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun status_code () Int)
(assert
(<= status_code 599))
(assert
(>= status_code 100))
(assert
(or (< status_code 100) (> status_code 599)))
(check-sat)
Request URI length bounded to prevent memory exhaustion. From ngx_http_parse_request_line().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun uri_len () Int)
(assert
(<= uri_len 8192))
(assert
(>= uri_len 1))
(assert
(or (< uri_len 1) (> uri_len 8192)))
(check-sat)
Recognized HTTP methods in ngx_http_parse_request_line() are dispatched by switch(p-m) over method lengths 3..9; constrain method token length to that validated range.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun method_len () Int)
(assert
(<= method_len 9))
(assert
(>= method_len 3))
(assert
(or (< method_len 3) (> method_len 9)))
(check-sat)
HTTP header count bounded. From ngx_http_parse_header_line().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun header_count () Int)
(assert
(<= header_count 100))
(assert
(>= header_count 0))
(assert
(or (< header_count 0) (> header_count 100)))
(check-sat)
HTTP minor version digit 0-9. From ngx_http_parse_request_line() digit parsing.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun http_minor () Int)
(assert
(<= http_minor 9))
(assert
(>= http_minor 0))
(assert
(or (< http_minor 0) (> http_minor 9)))
(check-sat)
Request-line parser accumulates HTTP minor version and rejects values >99 in ngx_http_parse_request_line().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun http_minor () Int)
(assert
(<= http_minor 99))
(assert
(>= http_minor 0))
(assert
(or (< http_minor 0) (> http_minor 99)))
(check-sat)
HTTP major version digit 0-9. From ngx_http_parse_request_line() digit parsing.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun http_major () Int)
(assert
(<= http_major 9))
(assert
(>= http_major 0))
(assert
(or (< http_major 0) (> http_major 9)))
(check-sat)
HTTP/1.x request-line parser rejects major versions >1; model as exact major==1 in ngx_http_parse_request_line().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun http_major () Int)
(assert
(<= http_major 1))
(assert
(>= http_major 1))
(assert
(or (< http_major 1) (> http_major 1)))
(check-sat)
Status-line parser transitions after exactly three status-code digits (++status->count == 3) in ngx_http_parse_status_line().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun status->count () Int)
(assert
(<= status->count 3))
(assert
(>= status->count 3))
(assert
(or (< status->count 3) (> status->count 3)))
(check-sat)
After exactly three status-code digits, sw_space_after_status only allows {' ', '.', CR, LF}; any other byte is rejected in ngx_http_parse_status_line().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun ch () Int)
(assert
(let (($x13 (= ch 10)))
(let (($x18 (= ch 13)))
(let (($x10 (= ch 46)))
(let (($x35 (= ch 32)))
(or $x35 $x10 $x18 $x13))))))
(assert
(let (($x13 (= ch 10)))
(let (($x18 (= ch 13)))
(let (($x10 (= ch 46)))
(let (($x35 (= ch 32)))
(let (($x22 (or $x35 $x10 $x18 $x13)))
(not $x22)))))))
(check-sat)
HTTP header name length bounded. From ngx_http_parse_header_line().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun header_name_len () Int)
(assert
(<= header_name_len 1024))
(assert
(>= header_name_len 1))
(assert
(or (< header_name_len 1) (> header_name_len 1024)))
(check-sat)
Header parser rejects control bytes (<=0x20) and DEL (0x7f); model visible ASCII byte range in ngx_http_parse_header_line().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun ch () Int)
(assert
(<= ch 126))
(assert
(>= ch 33))
(assert
(or (< ch 33) (> ch 126)))
(check-sat)
Status-line parser bounds HTTP major version to 0-99. From ngx_http_parse_status_line().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun http_major () Int)
(assert
(<= http_major 99))
(assert
(>= http_major 0))
(assert
(or (< http_major 0) (> http_major 99)))
(check-sat)
Status-line parser requires first major-version digit in '1'..'9', so composed HTTP major version cannot be zero in ngx_http_parse_status_line().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun http_major () Int)
(assert
(<= http_major 99))
(assert
(>= http_major 1))
(assert
(or (< http_major 1) (> http_major 99)))
(check-sat)
Status-line parser bounds HTTP minor version to 0-99. From ngx_http_parse_status_line().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun http_minor () Int)
(assert
(<= http_minor 99))
(assert
(>= http_minor 0))
(assert
(or (< http_minor 0) (> http_minor 99)))
(check-sat)
Status-line parser composes http_version = http_major*1000 + http_minor with each component bounded to 0-99, constraining composed version to 0-99099 in ngx_http_parse_status_line().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun status->http_version () Int)
(assert
(<= status->http_version 99099))
(assert
(>= status->http_version 0))
(assert
(or (< status->http_version 0) (> status->http_version 99099)))
(check-sat)
Stream TLS config must reject OCSP+optional_no_ca invalid auth state; ngx_stream_ssl_merge_srv_conf() errors on conf->ocsp && conf->verify == 3 before enabling OCSP, preventing revocation-check bypass states.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun conf->verify () Int)
(declare-fun conf->ocsp () Int)
(assert
(or (and (= conf->ocsp 0) (= conf->verify 0)) (and (= conf->ocsp 0) (= conf->verify 1)) (and (= conf->ocsp 0) (= conf->verify 2)) (and (= conf->ocsp 0) (= conf->verify 3)) (and (= conf->ocsp 1) (= conf->verify 0)) (and (= conf->ocsp 1) (= conf->verify 1)) (and (= conf->ocsp 1) (= conf->verify 2))))
(assert
(let (($x29 (= conf->verify 3)))
(let (($x7 (= conf->ocsp 1)))
(and $x7 $x29))))
(check-sat)