Nischoy — libsodium Verification Results

KDF Blake2b Subkey Length Bounds (16-64)

🌳 tree-sitter VERIFIED

Function: crypto_kdf_blake2b_derive_from_key · Z3 solved in 0.1ms

Subkey length must be 16-64 bytes. From crypto_kdf_blake2b_derive_from_key() in kdf_blake2b.c.

View SMT2 Constraints

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

KDF Blake2b Subkey ID uint64 Domain

🌳 tree-sitter (partial) VERIFIED

Function: crypto_kdf_blake2b_derive_from_key · Z3 solved in 0.0ms

Subkey ID must fit uint64. From crypto_kdf_blake2b_derive_from_key().

View SMT2 Constraints

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

Secretbox Message Length Bounds

🌳 tree-sitter (partial) VERIFIED

Function: crypto_secretbox_easy · Z3 solved in 0.0ms

Message length ≤ SODIUM_SIZE_MAX - MACBYTES. From crypto_secretbox_easy().

View SMT2 Constraints

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

Secretbox Ciphertext Includes MAC (≥16)

🌳 tree-sitter (partial) VERIFIED

Function: crypto_secretbox_open_easy · Z3 solved in 0.0ms

Ciphertext must be ≥ crypto_secretbox_MACBYTES (16). From crypto_secretbox_open_easy().

View SMT2 Constraints

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

Secretbox Plaintext Length Non-Negative

🌳 tree-sitter (partial) VERIFIED

Function: crypto_secretbox_open_easy · Z3 solved in 0.0ms

After stripping MACBYTES, plaintext length must not underflow. From crypto_secretbox_open_easy().

View SMT2 Constraints

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

Secretbox Open-Easy Return Code Domain (-1/0)

🌳 tree-sitter VERIFIED

Function: crypto_secretbox_open_easy · Z3 solved in 0.0ms

crypto_secretbox_open_easy should only expose canonical return codes: -1 on auth/length failure, 0 on authenticated decrypt.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun ret () Int)
(assert
 (let (($x28 (= ret 0)))
 (let (($x14 (= ret (- 1))))
 (or $x14 $x28))))
(assert
 (and (and (distinct ret (- 1)) true) (and (distinct ret 0) true)))
(check-sat)

Secretbox Open-Detached Return Code Domain (-1/0)

🌳 tree-sitter VERIFIED

Function: crypto_secretbox_open_detached · Z3 solved in 0.1ms

crypto_secretbox_open_detached should only expose canonical return codes: -1 on authentication failure, 0 on successful verification/decrypt.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun ret () Int)
(assert
 (let (($x37 (= ret 0)))
 (let (($x38 (= ret (- 1))))
 (or $x38 $x37))))
(assert
 (and (and (distinct ret (- 1)) true) (and (distinct ret 0) true)))
(check-sat)

Secretbox Detached First-Block Copy Clamp (≤32)

🌳 tree-sitter (partial) VERIFIED

Function: crypto_secretbox_detached · Z3 solved in 0.0ms

crypto_secretbox_detached clamps mlen0 to 64-ZEROBYTES (32) before copying into block0.

View SMT2 Constraints

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

Secretbox Open-Detached First-Block Copy Clamp (≤32)

🌳 tree-sitter (partial) VERIFIED

Function: crypto_secretbox_open_detached · Z3 solved in 0.0ms

crypto_secretbox_open_detached clamps mlen0 to 64-ZEROBYTES (32) before preloading block0.

View SMT2 Constraints

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

Curve25519 Box Open-Detached Afternm First-Block Copy Clamp (≤32)

🌳 tree-sitter (partial) VERIFIED

Function: crypto_secretbox_open_detached · Z3 solved in 0.0ms

crypto_box_open_detached_afternm delegates to crypto_secretbox_open_detached(), which clamps mlen0 to 32 before block0 preload.

View SMT2 Constraints

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

Curve25519 Box Open-Detached Return Code Domain (-1/0)

🌳 tree-sitter VERIFIED

Function: crypto_box_open_detached · Z3 solved in 0.0ms

crypto_box_open_detached should only expose canonical return codes: -1 on key setup failure, 0 on successful authenticated decrypt.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun ret () Int)
(assert
 (let (($x34 (= ret 0)))
 (let (($x26 (= ret (- 1))))
 (or $x26 $x34))))
(assert
 (and (and (distinct ret (- 1)) true) (and (distinct ret 0) true)))
(check-sat)

Curve25519 Box Open-Easy Return Code Domain (-1/0)

🌳 tree-sitter VERIFIED

Function: crypto_box_open_easy · Z3 solved in 0.0ms

crypto_box_open_easy should only expose canonical return codes: -1 on length/auth failure, 0 on successful authenticated decrypt.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun ret () Int)
(assert
 (let (($x14 (= ret 0)))
 (let (($x9 (= ret (- 1))))
 (or $x9 $x14))))
(assert
 (and (and (distinct ret (- 1)) true) (and (distinct ret 0) true)))
(check-sat)

Curve25519 Box Message Length Bounds

🌳 tree-sitter (partial) VERIFIED

Function: crypto_box_easy · Z3 solved in 0.0ms

Box message length ≤ SODIUM_SIZE_MAX - MACBYTES. From crypto_box_easy().

View SMT2 Constraints

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

Curve25519 Box Afternm Message Length Bounds

🌳 tree-sitter (partial) VERIFIED

Function: crypto_box_easy_afternm · Z3 solved in 0.0ms

Afternm box path enforces message length ≤ SODIUM_SIZE_MAX - MACBYTES. From crypto_box_easy_afternm().

View SMT2 Constraints

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

Curve25519 Box Ciphertext Includes MAC (≥16)

🌳 tree-sitter (partial) VERIFIED

Function: crypto_box_open_easy · Z3 solved in 0.0ms

Box ciphertext must be ≥ crypto_box_MACBYTES (16). From crypto_box_open_easy().

View SMT2 Constraints

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

Curve25519 Box Plaintext Length Non-Negative

🌳 tree-sitter (partial) VERIFIED

Function: crypto_box_open_easy · Z3 solved in 0.0ms

After stripping MACBYTES, plaintext length must not underflow. From crypto_box_open_easy().

View SMT2 Constraints

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

Curve25519 Box Afternm Ciphertext Includes MAC (≥16)

🌳 tree-sitter (partial) VERIFIED

Function: crypto_box_open_easy_afternm · Z3 solved in 0.0ms

Afternm decrypt path requires ciphertext ≥ crypto_box_MACBYTES (16) before detached handoff.

View SMT2 Constraints

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

Curve25519 Box Afternm Plaintext Length Non-Negative

🌳 tree-sitter (partial) VERIFIED

Function: crypto_box_open_easy_afternm · Z3 solved in 0.0ms

Afternm detached handoff uses clen - crypto_box_MACBYTES; subtraction must not underflow.

View SMT2 Constraints

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