Formal methods for ensuring model security

1) Why “formal methods” are needed in adversarial ML

Empirical testing (FGSM/PGD) answers: “Did the attacks we tried succeed?”
Formal methods answer: “Can any attack succeed within a defined threat model?”

In safety/security-critical ML (autonomy, biometrics, medical decision support), you often need more than confidence from testing. Formal methods provide:

• provable guarantees (or mathematically justified bounds)
• audit-ready evidence (clear assumptions, threat model, proof artifacts)
• system-level security reasoning beyond “accuracy under attack”

2) What formal methods mean in this context

Formal methods for ML robustness/security usually involve verifying properties like:

A) Local robustness

For a specific input x, prove:

B) Safety constraints

For example:

• output must not exceed a threshold
• prediction must remain within acceptable range
• “reject” must trigger if confidence too low

C) System-level properties

ML model + preprocessing + postprocessing + controller:

• avoid unsafe actions
• satisfy invariants (e.g., “never accelerate when obstacle distance < d”)

3) Main families of formal robustness verification

3.1 Exact / complete verification

These methods can prove whether a counterexample exists (and find it if it does), under certain conditions.

Common techniques:

• MILP (Mixed-Integer Linear Programming): exact verification for ReLU networks by encoding ReLU as integer constraints.
• SMT (Satisfiability Modulo Theories) solvers: reason about network constraints, sometimes more expressive.
• Branch-and-Bound / Split-and-Refine: recursively split input region and bound outputs.

Strength:

• Strongest guarantee (if it finishes), often returns either:
  • ✅ certified robust, or
  • ❌ concrete adversarial example (counterexample)

Limitations:

• Can be very slow / not scalable to huge networks
• Often used for smaller models, smaller input sizes, or critical components

3.2 Sound but incomplete verification (over-approximation)

These methods compute upper/lower bounds on network outputs over an input region. If the bounds prove the output class cannot change, you get a certificate.

Common techniques:

• Interval Bound Propagation (IBP)
• Linear relaxations (convex outer approximations of ReLU)
• Abstract interpretation (propagate abstract domains through layers)

Strength:

• Scales better than exact verification
• “Sound”: if it certifies robust, it’s truly robust under the assumptions

Limitations:

• Bounds may be loose → many points remain “unknown”
• Often yields smaller certified radii than empirical robustness

3.3 Probabilistic certification (randomized smoothing)

Randomized smoothing provides a probabilistic guarantee (often under L2) by turning a base classifier into a smoothed one.

Strength:

• Practical for large deep nets
• Produces a certified radius per example

Limitations:

• Usually L2 not L∞
• Requires many samples to estimate class probabilities

4) Formal verification workflow in a real ML security pipeline

Step 1 — Define the property to verify

Examples:

• “Prediction label remains unchanged within ε”
• “Top-1 remains top-1”
• “Output logit for class A ≥ output logit for class B”
• “Controller action remains within safe range”

Step 2 — Define the threat model precisely

• norm: L∞, L2, etc.
• ε: perturbation size
• input constraints: valid pixel ranges, categorical constraints

Step 3 — Choose a verification strategy

• Exact if small network / high assurance needed
• Bounded (sound) if you need scalability
• Smoothing if using large nets and L2 threats are acceptable

Step 4 — Generate artifacts

• certificates (robust/not robust/unknown)
• counterexamples if found
• logs + configuration (ε, norm, model hash)

Step 5 — Integrate into CI/CD (MLOps)

• verify on a critical slice of inputs each release
• track certified accuracy / certified radius drift over time

5) Formal methods beyond the model: ML system security

A robust model alone doesn’t guarantee a safe system. Formal methods are also used to verify ML-enabled pipelines, such as:

• preprocessing invariants (normalization is correct, no integer overflow)
• postprocessing safety rules (reject if low confidence)
• runtime monitors (out-of-distribution detection triggers safe fallback)
• controller constraints in robotics/autonomy (e.g., bounded acceleration)

Best practice: Use formal guarantees for the most safety-critical decision points, and empirical testing for the rest.

6) Mini-demo: “verification as constraints” intuition (toy example)

Below is a toy illustration of what many formal methods do: they reason about bounds to prove one class always wins.

This isn’t a full verifier—just a teaching snippet showing why bounds matter.

import numpy as np

def certify_linear_classifier(w, b, x, eps, norm="linf"):
    """
    Toy certificate for a binary linear classifier: sign(w·x + b).
    For L∞: worst-case change in w·x is eps * ||w||_1.
    If margin is larger than worst-case shift, prediction is certified.
    """
    margin = np.dot(w, x) + b
    if norm == "linf":
        worst_shift = eps * np.sum(np.abs(w))   # ||w||_1
    elif norm == "l2":
        worst_shift = eps * np.linalg.norm(w, 2)
    else:
        raise ValueError("norm must be 'linf' or 'l2'")

    # If margin cannot cross zero under worst-case perturbation, certified
    certified = (margin > worst_shift) or (margin < -worst_shift)
    return certified, margin, worst_shift

# Example usage:
w = np.array([0.8, -0.4, 0.2])
b = 0.1
x = np.array([0.5, 0.5, 0.5])

cert, margin, shift = certify_linear_classifier(w, b, x, eps=0.1, norm="linf")
print("Certified:", cert, "margin:", margin, "worst_shift:", shift)

Learner takeaway:
Formal verification often reduces to: “Can the margin flip sign under any allowed perturbation?”
For deep nets, the math is harder, so we use MILP/SMT or bound propagation.

7) Strengths and limitations (what ELMS learners must understand)

Strengths

• Gives provable robustness within defined threat model
• Helps avoid false confidence from weak attack evaluation
• Produces audit-friendly artifacts (certificates/counterexamples)

Limitations

• Scalability challenges for large models (especially exact methods)
• Guarantees are only as good as assumptions (norm choice, ε, input constraints)
• Many real-world threats are not well captured by small-norm perturbations (patches, lighting, semantic edits)