AdaEdge engine reference.

AdaEdge is a multi-layer network fingerprinting and bot detection engine that operates at the TLS/TCP level — before any JavaScript execution or cookie exchange. It combines four distinct signal layers into a deterministic scoring system with mathematically proven correctness guarantees.

The engine processes every connection through a <strong class="text-slate-100">connection pipeline</strong> with 7-step scoring — from TCP SYN to verdict — in under 500μs. All scoring logic runs in SPARK-verified Ada code with zero heap allocations in the hot path.

AdaEdge uses a layered architecture where Go handles I/O, networking, and orchestration while Ada/SPARK handles all security-critical computation. Communication between layers happens through CGO with zero-copy buffer sharing.

The core engine is implemented in Ada with SPARK annotations for formal verification. It contains the scoring algorithm, classifier, decision pipeline, and all fingerprint computation logic.

Fingerprint Input

Each connection produces a <code class="text-cyan-400 bg-cyan-400/10 px-1.5 py-0.5 rounded text-xs font-mono">Fingerprint_Input</code> record with 106 fields across 5 analysis layers:

JA3/JA4 Fingerprinting

The TLS module parses raw ClientHello bytes to extract cipher suites, extensions, supported groups, EC formats, signature algorithms, SNI, and ALPN. GREASE values are filtered before fingerprint computation.

Section A (10 chars): protocol + version + SNI + counts + ALPN
Section B (12 chars): SHA256(sorted ciphers) truncated
Section C (12 chars): SHA256(sorted exts + sig_algs) truncated

Example: t13d1517h2_8daaf6152771_b0da82dd1658

Browser Classification

A 32-entry lookup table maps JA4 Section A to browser families. The classifier also cross-references User-Agent with TLS fingerprint to detect spoofing.

Scoring Engine

The scoring engine produces a composite score in range [0, 100] with SPARK-proven bounds. Each layer contributes a weighted partial score:

TLS Deep     : 40%
TCP Passive  : 20%
Timing       : 15%
HTTP         : 25%

-- H2 Deep provides bonus/penalty on top of HTTP weight
-- Reputation and rate context applied as multipliers

Decision Pipeline

The pipeline state machine enforces forward-only transitions with a secure default (Drop). 7-step scoring with Kill Switch and Primary Decision:

Init | Reputation | TCP | KnownBot | CH_Received |
PreScore | Handshake | HTTP | Routed | Active | Closing

7-step scoring: kill switch then primary decision
Verdicts: Real | Clean | Drop

Known Bot Database

Pre-classified ASN table (64 entries max) with categories for search engines, social media crawlers, SEO tools, AI scrapers, monitoring services, and CDNs. Each entry includes ASN number, rDNS suffix for verification, and default action.

A complete TLS 1.3 cryptographic library implemented in pure Ada/SPARK — zero FFI dependencies, no OpenSSL. Every algorithm is formally verified with SPARK proofs.

Symmetric Encryption

Hash Functions & KDF

Key Exchange & Signatures

TLS 1.3 Record Layer

Full RFC 8446 Section 5 implementation with AEAD protection, nonce construction (IV XOR padded sequence number), and key update support.

-- AEAD encryption (RFC 8446 section 5.2)
Inner_Plaintext = Content followed by Content_Type_Byte
AAD             = Outer_Header (5 bytes)
Output          = Header(5) + Ciphertext + Tag(16)

-- Nonce construction (RFC 8446 section 5.3)
nonce[i] = IV XOR pad(seq_no, 12 bytes, big-endian)

-- Ghost lemma: nonce uniqueness proven for different seq numbers
-- Key update: max 2^24 records before rekeying (birthday bound)

X.509 Certificate Chain

Pure-Ada ASN.1 DER parser with zero heap allocation. Supports certificate chain validation, issuer matching, validity windows, Extended Key Usage (EKU) policy checking, and ECDSA/RSA signature verification.

SPARK-verified HTTP/2 implementation for frame parsing, HPACK header compression, and client fingerprinting. Compliant with RFC 9113 (HTTP/2) and RFC 7541 (HPACK).

Frame Processing

Parses the 9-byte HTTP/2 frame header and validates per-frame RFC constraints. All 10 standard frame types are handled:

H2 Fingerprint

The fingerprint captures SETTINGS parameters, WINDOW_UPDATE values, PRIORITY frames, and pseudo-header ordering. Hashed with FNV-1a 64-bit for fast comparison.

H2_Fingerprint:
  Settings           -- browser-specific SETTINGS frame values
  Conn_Window_Update -- connection-level flow control increment
  Priority_Count     -- number of PRIORITY frames in handshake
  Pseudo_Order       -- order of :method, :scheme, :authority, :path
  Hash               -- FNV-1a 64-bit fingerprint hash

Browser Differentiation

HPACK Compression

Full RFC 7541 header compression with static table (61 entries), dynamic table, and Huffman encoding. Bounded types prevent buffer overflows — header names max 256 bytes, values max 4096 bytes, max 128 headers per block.

The Go layer handles networking, configuration, storage, and orchestration. Ada code is linked as a static library via CGO, with each goroutine owning its own Ada session (no locks needed).

CGO Bridge

The bridge exports constants for modes and verdicts, and provides methods to feed connection data into the Ada scoring engine:

NewSession(mode)                           -> Ada session handle
Feed_ClientHello(handle, data)             -> parse TLS and JA3/JA4
Feed_HTTP_Request(handle, data)            -> parse HTTP headers
Set_TCP_Info(handle, window, ttl, mss, df) -> Layer 2
Set_Timing(ack_us, hs_us)                  -> Layer 3
Set_GEO_Info(country, asn, type)           -> GeoIP context
Set_H2_Info(...)                           -> Layer 5 (H2 deep)
Compute_Score(handle, flags)               -> Scoring_Result
Get_Verdict(handle)                        -> Verdict_Action

Connection Pipeline

Policy Engine

Configuration-driven access control with lock-free reads via <code class="text-cyan-400 bg-cyan-400/10 px-1.5 py-0.5 rounded text-xs font-mono">atomic.Value</code>. Supports IP/JA4 blacklists, CIDR-based whitelists, and per-mode score thresholds. Policy reloads use clone-modify-store pattern — zero contention on reads.

Reputation System

Per-IP reputation tracking with categories (Clean, Suspicious, Scanner, Attacker), confidence scoring (0–100), verdict streak tracking, JA4 diversity analysis, and rDNS verification for known bot ASNs.

Storage

PostgreSQL schema with 140+ columns per connection, capturing all fingerprint layers, scores, verdicts, and rate context. Includes per-site analytics queries for classification distribution and verdict breakdowns.

All security-critical code is written in SPARK — a formally verifiable subset of Ada. GNATprove statically verifies absence of runtime errors, contract compliance, and functional correctness.

What is Proven

SPARK Verification Boundary

Proof Configuration

Proof Level     : 2 (of 0-4)
Timeout         : 60 seconds per VC
Max Steps       : 10,000
Counterexamples : enabled
Report          : statistics

Release build:
  -gnatp (suppress checks) only on SPARK-proven files
  -O2 optimization
  Non-SPARK files retain full runtime checks

Build & Linking

Docker multi-stage build: GNAT compiler produces static library <code class="text-cyan-400 bg-cyan-400/10 px-1.5 py-0.5 rounded text-xs font-mono">libadaedge.a</code>, which is linked into the Go binary via CGO. The final artifact is a single statically-linked executable with PIE (Position Independent Executable).

Stage 1 (builder):
  gprbuild for ada_edge_lib.gpr -> libadaedge.a
  gprbuild for h2_engine.gpr    -> libh2.a
  CGO_ENABLED=1 go build        -> adaedge binary

Stage 2 (runtime):
  Minimal Debian + GNAT shared libs
  Unprivileged user (adaedge)
  Healthcheck: GET /livez :8080