cipherrun 0.3.0

// Kani Proof Harnesses for TLS Handshake Parsing
//
// These proofs verify that TLS parsing functions handle arbitrary input safely,
// without panics, buffer overflows, or integer overflows.

use crate::protocols::handshake::ServerHelloParser;
use crate::protocols::{Extension, Protocol};

/// Proof: ServerHelloParser::parse handles arbitrary input without panics
///
/// This proves that the ServerHello parser can handle any byte sequence
/// without panicking or causing undefined behavior.
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(100)]
fn proof_server_hello_parse_no_panic() {
    // Generate symbolic input of bounded size
    let len: usize = kani::any();
    kani::assume(len <= 64); // Bound input size for tractability

    let mut data: [u8; 64] = [0u8; 64];
    for i in 0..64 {
        data[i] = kani::any();
    }

    // Parser should not panic on any input
    let _ = ServerHelloParser::parse(&data[..len]);
}

/// Proof: ServerHelloParser::parse with valid TLS header structure
///
/// Verifies parsing when the first few bytes resemble a valid TLS structure.
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(100)]
fn proof_server_hello_parse_with_tls_header() {
    // Create data that looks like a TLS record
    let len: usize = kani::any();
    kani::assume(len >= 6 && len <= 64);

    let mut data: [u8; 64] = [0u8; 64];

    // TLS Handshake record type (0x16)
    data[0] = 0x16;

    // Version bytes (symbolic but constrained to valid range)
    let version_major: u8 = kani::any();
    let version_minor: u8 = kani::any();
    kani::assume(version_major == 0x03); // TLS
    kani::assume(version_minor <= 0x04); // Up to TLS 1.3

    data[1] = version_major;
    data[2] = version_minor;

    // Record length (symbolic)
    let record_len: u16 = kani::any();
    kani::assume((record_len as usize) <= len.saturating_sub(5));
    data[3] = (record_len >> 8) as u8;
    data[4] = (record_len & 0xff) as u8;

    // Fill rest with symbolic data
    for i in 5..len {
        data[i] = kani::any();
    }

    // Parser should handle this without panic
    let _ = ServerHelloParser::parse(&data[..len]);
}

/// Proof: Extension::new handles all extension types safely
///
/// Verifies that creating TLS extensions with any type and data is safe.
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(32)]
fn proof_extension_new_no_panic() {
    let extension_type: u16 = kani::any();

    // Generate symbolic extension data
    let data_len: usize = kani::any();
    kani::assume(data_len <= 16);

    let mut data: [u8; 16] = [0u8; 16];
    for i in 0..data_len {
        data[i] = kani::any();
    }

    // Extension creation should never panic
    let ext = Extension::new(extension_type, data[..data_len].to_vec());

    // Verify invariants
    kani::assert(ext.extension_type == extension_type, "Extension type must match");
}

/// Proof: Protocol conversion from u16 is total (handles all values)
///
/// Verifies that Protocol::from(u16) handles any input without panic.
#[cfg(kani)]
#[kani::proof]
fn proof_protocol_from_u16_total() {
    let value: u16 = kani::any();

    // This should never panic - it's a total function
    let protocol = Protocol::from(value);

    // Verify it returns a valid protocol (defaults to TLS 1.2 for unknown)
    let _ = protocol.name();
    let _ = protocol.as_hex();
    let _ = protocol.is_deprecated();
}

/// Proof: Protocol::as_hex is bijective for known protocols
///
/// Verifies that converting to hex and back preserves the protocol.
#[cfg(kani)]
#[kani::proof]
fn proof_protocol_hex_roundtrip() {
    // Use index to select protocol variant (avoid needing Arbitrary impl)
    let idx: u8 = kani::any();
    kani::assume(idx < 7);

    let protocol = match idx {
        0 => Protocol::SSLv2,
        1 => Protocol::SSLv3,
        2 => Protocol::TLS10,
        3 => Protocol::TLS11,
        4 => Protocol::TLS12,
        5 => Protocol::TLS13,
        _ => Protocol::QUIC,
    };

    let hex = protocol.as_hex();
    let roundtrip = Protocol::from(hex);

    // For known protocols (excluding QUIC which has non-standard hex), roundtrip should match
    match protocol {
        Protocol::SSLv2
        | Protocol::SSLv3
        | Protocol::TLS10
        | Protocol::TLS11
        | Protocol::TLS12
        | Protocol::TLS13 => {
            kani::assert(roundtrip == protocol, "Known protocol roundtrip must match");
        }
        Protocol::QUIC => {
            // QUIC uses non-standard hex, roundtrip not guaranteed
        }
    }
}

/// Proof: check_heartbeat_extension handles arbitrary data safely
///
/// This simulates the check_heartbeat_extension function behavior
/// to verify it handles all possible inputs without panic.
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(100)]
fn proof_check_heartbeat_extension_no_panic() {
    let len: usize = kani::any();
    kani::assume(len <= 32);

    let mut data: [u8; 32] = [0u8; 32];
    for i in 0..len {
        data[i] = kani::any();
    }

    // Simulate the heartbeat extension check logic
    let result = if len < 2 {
        false
    } else {
        let mut found = false;
        for i in 0..len.saturating_sub(1) {
            if data[i] == 0x00 && data[i + 1] == 0x0f {
                found = true;
                break;
            }
        }
        found
    };

    // Just verify we got a boolean result without panic
    let _ = result;
}

/// Proof: TLS version parsing handles edge cases
///
/// Verifies that version byte parsing is safe for all inputs.
#[cfg(kani)]
#[kani::proof]
fn proof_tls_version_parsing() {
    let high_byte: u8 = kani::any();
    let low_byte: u8 = kani::any();

    // Construct version as u16 (big-endian)
    let version = u16::from_be_bytes([high_byte, low_byte]);

    // Protocol::from should handle any version
    let protocol = Protocol::from(version);

    // Verify protocol is in valid state
    let _name = protocol.name();
    let _hex = protocol.as_hex();
}