← nischoy.ai

curl Verification

SMT2 formal verification of security-critical code paths

ALL VERIFIED

Overall

Properties Checked

Verified

Failed

Port Number Bounds (0-65535)

🌳 tree-sitter VERIFIED

Function: Curl_parse_port · Z3 solved in 0.2ms

Ensures that a parsed port number strictly falls between 0 and 65535. Extracted from Curl_parse_port() which uses curlx_str_number(..., 0xffff) to enforce the bound.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun port () Int)
(declare-fun u->portnum () Int)
(assert
 (<= port 65535))
(assert
 (>= port 0))
(assert
 (let ((?x30 (mod port 65536)))
 (= u->portnum ?x30)))
(assert
 (or (< u->portnum 0) (> u->portnum 65535)))
(check-sat)

IPv6 Bracket Integrity

🌳 tree-sitter VERIFIED

Function: ipv6_parse · Z3 solved in 0.0ms

Proves that any IPv6 address starting with '[' must terminate with ']'. Extracted from hostname_check → ipv6_parse delegation in the real curl URL parser.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun hostname () String)
(assert
 (let (($x31 (= (str.substr hostname (- (str.len hostname) 1) 1) "]")))
 (let (($x38 (= (str.substr hostname 0 1) "[")))
 (=> $x38 $x31))))
(assert
 (let (($x31 (= (str.substr hostname (- (str.len hostname) 1) 1) "]")))
(let (($x38 (= (str.substr hostname 0 1) "[")))
(and $x38 (not $x31)))))
(check-sat)

No CRLF in Credentials (Header Injection)

🌳 tree-sitter VERIFIED

Function: parse_hostname_login · Z3 solved in 0.0ms

Verifies that HTTP headers cannot be injected via username or password fields. In curl, Curl_junkscan rejects all control chars from the URL before parse_hostname_login runs.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun user () String)
(declare-fun password () String)
(assert
 (let (($x38 (str.contains user "\u{d}")))
 (not $x38)))
(assert
 (let (($x128 (str.contains user "\u{a}")))
 (not $x128)))
(assert
 (let (($x95 (str.contains password "\u{d}")))
 (not $x95)))
(assert
 (let (($x125 (str.contains password "\u{a}")))
 (not $x125)))
(assert
 (let (($x125 (str.contains password "\u{a}")))
(let (($x95 (str.contains password "\u{d}")))
(let (($x128 (str.contains user "\u{a}")))
(let (($x38 (str.contains user "\u{d}")))
(or $x38 $x128 $x95 $x125))))))
(check-sat)

Hostname Character Validation (SSRF)

🌳 tree-sitter VERIFIED

Function: hostname_check · Z3 solved in 0.0ms

Prevents SSRF by rejecting dangerous chars in hostnames. Extracted from hostname_check() which uses strcspn() with the actual rejection charset from the curl source.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun hostname () String)
(assert
 (let (($x38 (str.contains hostname " ")))
 (not $x38)))
(assert
 (let (($x111 (str.contains hostname "\u{d}")))
 (not $x111)))
(assert
 (let (($x45 (str.contains hostname "\u{a}")))
 (not $x45)))
(assert
 (let (($x27 (str.contains hostname "\u{9}")))
 (not $x27)))
(assert
 (let (($x65 (str.contains hostname "/")))
 (not $x65)))
(assert
 (let (($x35 (str.contains hostname ":")))
 (not $x35)))
(assert
 (let (($x20 (str.contains hostname "#")))
 (not $x20)))
(assert
 (let (($x86 (str.contains hostname "?")))
 (not $x86)))
(assert
 (let (($x58 (str.contains hostname "!")))
 (not $x58)))
(assert
 (let (($x81 (str.contains hostname "@")))
 (not $x81)))
(assert
 (let (($x98 (str.contains hostname "{")))
 (not $x98)))
(assert
 (let (($x100 (str.contains hostname "}")))
 (not $x100)))
(assert
 (let (($x107 (str.contains hostname "[")))
 (not $x107)))
(assert
 (not (str.contains hostname "]")))
(assert
 (let (($x122 (str.contains hostname "\")))
 (not $x122)))
(assert
 (let (($x132 (str.contains hostname "$")))
 (not $x132)))
(assert
 (let (($x150 (str.contains hostname "'")))
 (not $x150)))
(assert
 (let (($x93 (str.contains hostname """")))
 (not $x93)))
(assert
 (let (($x154 (str.contains hostname "^")))
 (not $x154)))
(assert
 (let (($x161 (str.contains hostname "`")))
 (not $x161)))
(assert
 (let (($x168 (str.contains hostname "*")))
 (not $x168)))
(assert
 (let (($x175 (str.contains hostname "<")))
 (not $x175)))
(assert
 (let (($x182 (str.contains hostname ">")))
 (not $x182)))
(assert
 (let (($x189 (str.contains hostname "=")))
 (not $x189)))
(assert
 (let (($x196 (str.contains hostname ";")))
 (not $x196)))
(assert
 (let (($x203 (str.contains hostname ",")))
 (not $x203)))
(assert
 (let (($x210 (str.contains hostname "+")))
 (not $x210)))
(assert
 (let (($x217 (str.contains hostname "&")))
 (not $x217)))
(assert
 (let (($x224 (str.contains hostname "(")))
 (not $x224)))
(assert
 (let (($x231 (str.contains hostname ")")))
 (not $x231)))
(assert
 (not (str.contains hostname "%")))
(assert
 (let (($x231 (str.contains hostname ")")))
(let (($x224 (str.contains hostname "(")))
(let (($x217 (str.contains hostname "&")))
(let (($x210 (str.contains hostname "+")))
(let (($x203 (str.contains hostname ",")))
(let (($x196 (str.contains hostname ";")))
(let (($x189 (str.contains hostname "=")))
(let (($x182 (str.contains hostname ">")))
(let (($x175 (str.contains hostname "<")))
(let (($x168 (str.contains hostname "*")))
(let (($x161 (str.contains hostname "`")))
(let (($x154 (str.contains hostname "^")))
(let (($x93 (str.contains hostname """")))
(let (($x150 (str.contains hostname "'")))
(let (($x132 (str.contains hostname "$")))
(let (($x122 (str.contains hostname "\")))
(let (($x107 (str.contains hostname "[")))
(let (($x100 (str.contains hostname "}")))
(let (($x98 (str.contains hostname "{")))
(let (($x81 (str.contains hostname "@")))
(let (($x58 (str.contains hostname "!")))
(let (($x86 (str.contains hostname "?")))
(let (($x20 (str.contains hostname "#")))
(let (($x35 (str.contains hostname ":")))
(let (($x65 (str.contains hostname "/")))
(let (($x27 (str.contains hostname "\u{9}")))
(let (($x45 (str.contains hostname "\u{a}")))
(let (($x111 (str.contains hostname "\u{d}")))
(let (($x38 (str.contains hostname " ")))
(or $x38 $x111 $x45 $x27 $x65 $x35 $x20 $x86 $x58 $x81 $x98 $x100 $x107 $x122 $x132 $x150 $x93 $x154 $x161 $x168 $x175 $x182 $x189 $x196 $x203 $x210 $x217 $x224 $x231)))))))))))))))))))))))))))))))
(check-sat)

URL Control Character Rejection (Smuggling)

🌳 tree-sitter VERIFIED

Function: Curl_junkscan · Z3 solved in 0.0ms

Proves the URL rejects all non-printable ASCII (≤31 or ==127). Extracted from Curl_junkscan() which scans every byte in a loop.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun url () String)
(assert
 (let (($x38 (str.contains url "\u{0}")))
 (not $x38)))
(assert
 (let (($x107 (str.contains url "\u{1}")))
 (not $x107)))
(assert
 (let (($x135 (str.contains url "\u{2}")))
 (not $x135)))
(assert
 (let (($x168 (str.contains url "\u{3}")))
 (not $x168)))
(assert
 (let (($x195 (str.contains url "\u{4}")))
 (not $x195)))
(assert
 (let (($x217 (str.contains url "\u{5}")))
 (not $x217)))
(assert
 (let (($x238 (str.contains url "\u{6}")))
 (not $x238)))
(assert
 (let (($x197 (str.contains url "\u{7}")))
 (not $x197)))
(assert
 (let (($x139 (str.contains url "\u{8}")))
 (not $x139)))
(assert
 (let (($x103 (str.contains url "\u{9}")))
 (not $x103)))
(assert
 (let (($x16 (str.contains url "\u{a}")))
 (not $x16)))
(assert
 (let (($x241 (str.contains url "\u{b}")))
 (not $x241)))
(assert
 (let (($x228 (str.contains url "\u{c}")))
 (not $x228)))
(assert
 (let (($x205 (str.contains url "\u{d}")))
 (not $x205)))
(assert
 (let (($x192 (str.contains url "\u{e}")))
 (not $x192)))
(assert
 (let (($x179 (str.contains url "\u{f}")))
 (not $x179)))
(assert
 (let (($x156 (str.contains url "\u{10}")))
 (not $x156)))
(assert
 (let (($x116 (str.contains url "\u{11}")))
 (not $x116)))
(assert
 (let (($x130 (str.contains url "\u{12}")))
 (not $x130)))
(assert
 (let (($x92 (str.contains url "\u{13}")))
 (not $x92)))
(assert
 (let (($x73 (str.contains url "\u{14}")))
 (not $x73)))
(assert
 (let (($x52 (str.contains url "\u{15}")))
 (not $x52)))
(assert
 (let (($x67 (str.contains url "\u{16}")))
 (not $x67)))
(assert
 (let (($x12 (str.contains url "\u{17}")))
 (not $x12)))
(assert
 (let (($x96 (str.contains url "\u{18}")))
 (not $x96)))
(assert
 (let (($x222 (str.contains url "\u{19}")))
 (not $x222)))
(assert
 (let (($x173 (str.contains url "\u{1a}")))
 (not $x173)))
(assert
 (let (($x124 (str.contains url "\u{1b}")))
 (not $x124)))
(assert
 (let (($x84 (str.contains url "\u{1c}")))
 (not $x84)))
(assert
 (let (($x145 (str.contains url "\u{1d}")))
 (not $x145)))
(assert
 (let (($x47 (str.contains url "\u{1e}")))
 (not $x47)))
(assert
 (let (($x125 (str.contains url "\u{1f}")))
 (not $x125)))
(assert
 (let (($x257 (str.contains url "\u{7f}")))
 (not $x257)))
(assert
 (let (($x257 (str.contains url "\u{7f}")))
(let (($x125 (str.contains url "\u{1f}")))
(let (($x47 (str.contains url "\u{1e}")))
(let (($x145 (str.contains url "\u{1d}")))
(let (($x84 (str.contains url "\u{1c}")))
(let (($x124 (str.contains url "\u{1b}")))
(let (($x173 (str.contains url "\u{1a}")))
(let (($x222 (str.contains url "\u{19}")))
(let (($x96 (str.contains url "\u{18}")))
(let (($x12 (str.contains url "\u{17}")))
(let (($x67 (str.contains url "\u{16}")))
(let (($x52 (str.contains url "\u{15}")))
(let (($x73 (str.contains url "\u{14}")))
(let (($x92 (str.contains url "\u{13}")))
(let (($x130 (str.contains url "\u{12}")))
(let (($x116 (str.contains url "\u{11}")))
(let (($x156 (str.contains url "\u{10}")))
(let (($x179 (str.contains url "\u{f}")))
(let (($x192 (str.contains url "\u{e}")))
(let (($x205 (str.contains url "\u{d}")))
(let (($x228 (str.contains url "\u{c}")))
(let (($x241 (str.contains url "\u{b}")))
(let (($x16 (str.contains url "\u{a}")))
(let (($x103 (str.contains url "\u{9}")))
(let (($x139 (str.contains url "\u{8}")))
(let (($x197 (str.contains url "\u{7}")))
(let (($x238 (str.contains url "\u{6}")))
(let (($x217 (str.contains url "\u{5}")))
(let (($x195 (str.contains url "\u{4}")))
(let (($x168 (str.contains url "\u{3}")))
(let (($x135 (str.contains url "\u{2}")))
(let (($x107 (str.contains url "\u{1}")))
(let (($x38 (str.contains url "\u{0}")))
(or $x38 $x107 $x135 $x168 $x195 $x217 $x238 $x197 $x139 $x103 $x16 $x241 $x228 $x205 $x192 $x179 $x156 $x116 $x130 $x92 $x73 $x52 $x67 $x12 $x96 $x222 $x173 $x124 $x84 $x145 $x47 $x125 $x257)))))))))))))))))))))))))))))))))))
(check-sat)

URL Input Length Bounds (CURL_MAX_INPUT_LENGTH)

🌳 tree-sitter VERIFIED

Function: Curl_junkscan · Z3 solved in 0.0ms

Verifies URL length never exceeds CURL_MAX_INPUT_LENGTH (8,000,000 bytes). Extracted from the length check at the top of Curl_junkscan().

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun urllen () Int)
(assert
 (<= urllen 8000000))
(assert
 (>= urllen 0))
(assert
 (or (< urllen 0) (> urllen 8000000)))
(check-sat)

Scheme Length Bounds (MAX_SCHEME_LEN)

🌳 tree-sitter VERIFIED

Function: Curl_get_scheme_handler · Z3 solved in 0.0ms

Proves the URL scheme is between 1 and MAX_SCHEME_LEN (40) characters. Extracted from Curl_is_absolute_url() for-loop with the real constant from urlapi.c.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun scheme_len () Int)
(assert
 (<= scheme_len 40))
(assert
 (>= scheme_len 1))
(assert
 (or (< scheme_len 1) (> scheme_len 40)))
(check-sat)

Redirect Counter Bounds (Open Redirect DoS)

🌳 tree-sitter VERIFIED

Function: curl_follow_redirect · Z3 solved in 0.0ms

Ensures redirect counters stay within type bounds. Verified against curl's setopt handling.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun followlocation () Int)
(declare-fun maxredirs () Int)
(assert
 (<= followlocation 65535))
(assert
 (>= followlocation 0))
(assert
 (<= maxredirs 32767))
(assert
 (>= maxredirs (- 1)))
(assert
 (or (or (< followlocation 0) (> followlocation 65535)) (or (< maxredirs (- 1)) (> maxredirs 32767))))
(check-sat)

Timeout Value Bounds (Overflow Prevention)

🌳 tree-sitter VERIFIED

Function: Curl_setopt · Z3 solved in 0.0ms

Proves timeout values are non-negative and ≤2,147,483 seconds to prevent overflow in sec→ms conversion.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun connect_timeout () Int)
(declare-fun transfer_timeout () Int)
(assert
 (<= connect_timeout 2147483))
(assert
 (>= connect_timeout 0))
(assert
 (<= transfer_timeout 2147483))
(assert
 (>= transfer_timeout 0))
(assert
 (or (or (< connect_timeout 0) (> connect_timeout 2147483)) (or (< transfer_timeout 0) (> transfer_timeout 2147483))))
(check-sat)

DNS Name Length Bounds (RFC 1035)

🌳 tree-sitter VERIFIED

Function: Curl_resolv · Z3 solved in 0.0ms

Verifies hostname length is 1-253 chars per RFC 1035.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun hostname_len () Int)
(assert
 (<= hostname_len 253))
(assert
 (>= hostname_len 1))
(assert
 (or (< hostname_len 1) (> hostname_len 253)))
(check-sat)

DNS Label Length Bounds (RFC 1035 §2.3.4)

🌳 tree-sitter VERIFIED

Function: Curl_resolv · Z3 solved in 0.0ms

Proves each DNS label is 1-63 octets per RFC 1035 §2.3.4.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun label_len () Int)
(assert
 (<= label_len 63))
(assert
 (>= label_len 1))
(assert
 (or (< label_len 1) (> label_len 63)))
(check-sat)

Content-Length Value Bounds (Integer Overflow Prevention)

🌳 tree-sitter VERIFIED

Function: http_response_headers · Z3 solved in 0.0ms

Verifies Content-Length header value is non-negative and ≤ CURL_OFF_T_MAX (2^63-1). Extracted from http_response_headers() where curlx_str_numblanks returns STRE_OVERFLOW for out-of-range values.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun content_length () Int)
(assert
 (<= content_length 9223372036854775807))
(assert
 (>= content_length 0))
(assert
 (or (< content_length 0) (> content_length 9223372036854775807)))
(check-sat)

Cookie Line Length Bounds (Heap Overflow Prevention)

🌳 tree-sitter VERIFIED

Function: Curl_cookie_add · Z3 solved in 0.0ms

Proves cookie lines are rejected if >5000 bytes (MAX_COOKIE_LINE), preventing heap overflow in Curl_cookie_add.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun cookie_line_len () Int)
(assert
 (<= cookie_line_len 5000))
(assert
 (>= cookie_line_len 0))
(assert
 (or (< cookie_line_len 0) (> cookie_line_len 5000)))
(check-sat)

Chunk Hex-Length Bounds (Buffer Overflow Prevention)

🌳 tree-sitter VERIFIED

Function: Curl_httpchunk_read · Z3 solved in 0.0ms

Proves chunked transfer-encoding hex-length string is bounded to CHUNK_MAXNUM_LEN (16 chars), preventing hexbuffer overflow and ensuring parsed chunk size fits curl_off_t.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun chunk_hexindex () Int)
(assert
 (<= chunk_hexindex 16))
(assert
 (>= chunk_hexindex 0))
(assert
 (or (< chunk_hexindex 0) (> chunk_hexindex 16)))
(check-sat)

HSTS Max-Age Bounds (Integer Overflow Prevention)

🌳 tree-sitter VERIFIED

Function: Curl_hsts_parse · Z3 solved in 0.0ms

Verifies HSTS max-age expires value is bounded to [0, CURL_OFF_T_MAX]. curlx_str_number caps at TIME_T_MAX, overflow clamps to CURL_OFF_T_MAX, and expires+now addition is guarded against wraparound.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun hsts_expires () Int)
(assert
 (<= hsts_expires 9223372036854775807))
(assert
 (>= hsts_expires 0))
(assert
 (or (< hsts_expires 0) (> hsts_expires 9223372036854775807)))
(check-sat)

Cookie Name+Value Length Bounds (Buffer Overflow Prevention)

🌳 tree-sitter VERIFIED

Function: Curl_cookie_add · Z3 solved in 0.0ms

Proves individual cookie name and value are each <4095 bytes, and combined ≤4096 (MAX_NAME), preventing buffer overflow in Set-Cookie parsing.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun cookie_name_len () Int)
(declare-fun cookie_val_len () Int)
(declare-fun cookie_combined_len () Int)
(assert
 (<= cookie_name_len 4094))
(assert
 (>= cookie_name_len 0))
(assert
 (<= cookie_val_len 4094))
(assert
 (>= cookie_val_len 0))
(assert
 (<= cookie_combined_len 4096))
(assert
 (>= cookie_combined_len 0))
(assert
 (or (< cookie_name_len 0) (> cookie_name_len 4094) (< cookie_val_len 0) (> cookie_val_len 4094) (< cookie_combined_len 0) (> cookie_combined_len 4096)))
(check-sat)

ALTSVC Max-Age Bounds (Integer Overflow Prevention)

🌳 tree-sitter VERIFIED

Function: altsvc_from_header · Z3 solved in 0.0ms

Verifies Alt-Svc ma= max-age value is bounded to [0, TIME_T_MAX]. curlx_str_number caps parsing at TIME_T_MAX, and expires=maxage+secs addition is guarded against wraparound by clamping to TIME_T_MAX.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun altsvc_maxage () Int)
(assert
 (<= altsvc_maxage 9223372036854775807))
(assert
 (>= altsvc_maxage 0))
(assert
 (or (< altsvc_maxage 0) (> altsvc_maxage 9223372036854775807)))
(check-sat)

Cookie Send Amount Bounds (DoS Prevention)

🌳 tree-sitter VERIFIED

Function: Curl_cookie_getlist · Z3 solved in 0.0ms

Verifies cookies sent per request are capped at MAX_COOKIE_SEND_AMOUNT (150), preventing excessive cookie header generation that could cause request amplification or header overflow.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun cookie_send_count () Int)
(assert
 (<= cookie_send_count 150))
(assert
 (>= cookie_send_count 0))
(assert
 (or (< cookie_send_count 0) (> cookie_send_count 150)))
(check-sat)

MIME Encoder Output Length Bounds (Buffer Overflow Prevention)

🌳 tree-sitter VERIFIED

Function: escape_mime_string · Z3 solved in 0.0ms

Verifies MIME-encoded field name output is bounded to CURL_MAX_INPUT_LENGTH (8MB) via curlx_dyn_init, preventing unbounded buffer growth from crafted multipart form field names.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun mime_encode_output_len () Int)
(assert
 (<= mime_encode_output_len 8000000))
(assert
 (>= mime_encode_output_len 0))
(assert
 (or (< mime_encode_output_len 0) (> mime_encode_output_len 8000000)))
(check-sat)

MIME Filename Escape Bounds (Buffer Overflow Prevention)

🌳 tree-sitter VERIFIED

Function: escape_string · Z3 solved in 0.0ms

Verifies escape_string() output for Content-Disposition filenames is bounded to CURL_MAX_INPUT_LENGTH (8MB) via curlx_dyn_init, preventing unbounded buffer growth from crafted MIME part filenames.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun mime_filename_escape_len () Int)
(assert
 (<= mime_filename_escape_len 8000000))
(assert
 (>= mime_filename_escape_len 0))
(assert
 (or (< mime_filename_escape_len 0) (> mime_filename_escape_len 8000000)))
(check-sat)

Last verified: 2026-03-25 12:02:35 UTC · Solver: Z3 4.16.0