Symbolic Execution Engine

1// Original code
2function processPayment(amount, discount) {
3  if (amount > 1000) {
4    if (discount > 50) {
5      // Vulnerability: negative amount possible
6      const final = amount - (amount * discount / 100);
7      if (final < 0) {
8        refund(-final);  // 💥 Bug: refund on purchase!
9      }
10    }
11  }
12}
13
14// Symbolic execution traces:
15// Let amount = α, discount = β (symbolic variables)
16
17// Path 1: amount ≤ 1000
18//   Constraint: α ≤ 1000
19//   Result: No bug (early return)
20
21// Path 2: amount > 1000 AND discount ≤ 50
22//   Constraint: α > 1000 ∧ β ≤ 50
23//   Result: No bug (discount check fails)
24
25// Path 3: amount > 1000 AND discount > 50 AND final ≥ 0
26//   Constraint: α > 1000 ∧ β > 50 ∧ (α - α*β/100) ≥ 0
27//   Result: No bug (no refund)
28
29// Path 4: amount > 1000 AND discount > 50 AND final < 0 ⚠️
30//   Constraint: α > 1000 ∧ β > 50 ∧ (α - α*β/100) < 0
31//   Solving: β > 100 needed for final < 0
32//   Solution: α = 2000, β = 150
33//   EXPLOIT: processPayment(2000, 150) triggers bug!

1// Bloodhound Vulnerability Report
2
3━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
4CRITICAL: SQL Injection in getUserData()
5File: src/api/users.ts:47
6━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
7
8Symbolic execution found a path from user input to SQL query.
9
10Path constraints solved:
11  • req.query.id must be a string
12  • Length must be > 0
13  • Must contain SQL metacharacter
14
15Generated exploit:
16  GET /api/users?id=1' OR '1'='1
17
18Expected behavior:
19  Returns single user with id=1
20
21Actual behavior with exploit:
22  Returns ALL users (authentication bypass)
23
24Proof of exploitability: ✓ CONFIRMED
25━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━