Formalizing Software Vulnerabilities with Mathematics: From ∀x S(P(x)) to Formal Verification

Writing "no vulnerabilities" in the language of mathematics

"This software has no vulnerabilities" can't be checked as long as it stays in everyday language: what inputs are we talking about, and what does "safe" actually mean? So we define the program, its inputs, and safety as symbols, and write the claim down as a logical formula. That is formalization.

First, the notation.

Σ      : the set of input symbols (bytes)
Σ*     : the set of all finite sequences over Σ (= every possible input)
P      : the program under verification
P(x)   : the result of running P on input x
S(·)   : a predicate meaning "this result is safe"

"Safe for every input" then becomes:

∀x ∈ Σ*,  S(P(x))

Read: "for any input x in Σ*, P(x) is safe." The key point is that ∀ ranges over the infinite set Σ*. Testing tens of thousands of inputs only examines a tiny slice of it.

Existence vs. non-existence of a vulnerability

Let V(P, x) return 1 if input x drives P into a dangerous state and 0 otherwise. The two claims then form a pair:

A vulnerability exists        :  ∃x  V(P, x) = 1
No vulnerability exists       :  ∀x  V(P, x) = 0

They are negations of each other (¬∃x φ ≡ ∀x ¬φ), yet the effort to establish them is wildly different.

• Existence is settled by finding one x. This is what fuzzing and penetration testing are good at.
• Non-existence requires showing the property for all of infinitely many x. Piling up tests can never get there in principle.

Dijkstra's famous remark that testing can show the presence of bugs but not their absence is exactly this asymmetry between quantifiers.

Looking at the journey, not just the output: execution traces

Even if the final output is correct, reading past a buffer or touching memory without permission along the way is still a vulnerability. So we treat an execution as a sequence of states — a trace.

Traces(P, x) : the set of possible execution traces of P on input x
τ = s₀ s₁ s₂ …  : a trace (sequence of states)
Safe         : the set of safe states

∀x ∀τ ∈ Traces(P, x) ∀s ∈ τ,  s ∈ Safe

"For every input, along every execution path, every intermediate state is safe." Traces is a set because thread scheduling and external interrupts can produce several paths for the same input. Properties of the form "something bad never happens" are called safety properties.

What the attacker looks for: ∃x ¬Safe(P, x)

Negate the safety claim and you get exactly what an attacker — or a vulnerability assessor — is searching for.

¬(∀x Safe(P, x))  ≡  ∃x ¬Safe(P, x)

An attack is finding a single counterexample to safety. The defender must hold the ∀; the attacker needs only one ∃. The well-known "attacker's advantage" is visible in the shape of the formula itself. Conversely, when a verification tool returns a counterexample, it is concrete evidence that a particular input really does reach a dangerous state.

Formalizing is not proving

What we've done so far is formalization: rewriting a claim as an unambiguous formula. Being able to write it does not mean we have proved it true.

That doesn't make formal verification pointless. Practical methods get around the wall in one of these ways:

• restrict the target to finitely many states (finite means exhaustively searchable)
• bound input length or loop iterations (bounded verification)
• allow approximation (anything not provably safe is reported as a warning)
• have a human supply the proof strategy (loop invariants, etc.)

The main techniques

Hoare logic

A system for stating and proving the relationship between the condition before and after each part of a program.

{ Pre }  C  { Post }
"If C runs from a state satisfying Pre and terminates, Post holds."

Example: safe array access
{ 0 ≤ i ∧ i < len(a) }  y := a[i]  { y = a[i] }

Loops need a human-supplied loop invariant — a property preserved by every iteration — which is the hard part to automate.

Model checking

Model the system as a finite state-transition system M and decide, by exhaustively exploring the state space, whether it satisfies a property φ written in temporal logic.

M ⊨ □ Safe      (□ means "always": Safe in every reachable state)

Its big advantage is that a violation comes with a concrete counterexample run. Its biggest problem is state explosion as variables are added.

SAT / SMT solvers

Encode an execution path together with the condition "a dangerous state is reached" as one formula, and ask a solver whether any assignment satisfies it.

φ = Path(P, x) ∧ ¬Safe
φ satisfiable (SAT)     → a satisfying x is an input that triggers the vulnerability
φ unsatisfiable (UNSAT) → no vulnerability on that path (within the explored bounds)

SMT extends SAT with theories such as integers, arrays, and bit-vectors, and powers symbolic execution and bounded model checking.

Theorem proving

In proof assistants such as Coq (Rocq), Isabelle, or Lean, you write the program and its specification and prove ∀x S(P(x)) with human and machine working together. It gives the strongest guarantees at the highest cost. The verified seL4 microkernel and the verified C compiler CompCert are flagship examples.

Abstract interpretation

Compute with abstract values — ranges, signs — instead of concrete ones, over-approximating every possible state.

concrete reachable states ⊆ abstract reachable states γ(A)
γ(A) ⊆ Safe  ⇒  concrete reachable states ⊆ Safe   (sound)

Because it over-approximates, anything judged safe really is safe (soundness), but false positives — warnings on code that is actually fine — are unavoidable. Facing the halting problem, it chooses to always terminate at the price of some precision.

Each vulnerability class changes the formula

What "Safe" means depends heavily on the class of vulnerability. Some representative ones:

Memory safety (buffer overflows, etc.)	∀ access a[i] : 0 ≤ i < len(a) Every array or pointer access stays within allocated bounds. Expressible as a property of each state on a trace.
Integer overflow	∀ operation a + b : MIN ≤ a + b ≤ MAX The mathematical result and the fixed-width machine result agree.
Injection (SQL, command, etc.)	∀x : structure of parse(query(x)) = structure the developer intended Input stays in "data" positions and never changes the "command" structure. Usually handled with taint analysis.
Information leakage (confidentiality)	∀ s₁, s₂ : low(s₁) = low(s₂) ⇒ obs(P, s₁) = obs(P, s₂) Two runs differing only in secret values look the same from outside. This compares two runs — a hyperproperty — and cannot be stated about a single trace.
Side channels (timing, etc.)	∀ secret₁, secret₂ : time(P, secret₁) = time(P, secret₂) Running time does not depend on secret values (constant-time code). Also a hyperproperty.
Denial of service	∀x : cost(P, x) ≤ f(|x|) Cost stays within the expected bound for the input size — closer to a liveness property, requiring that things eventually finish.
Authorization & access control	∀ operation op, principal u : perform(u, op) ⇒ allowed(u, op) Every operation performed is one the policy permits.

"No vulnerability" takes very different logical shapes: some need only each state of one run, some compare two runs, some reason about infinite runs. That shape decides which tools apply.

Where it pays off in practice

• Small, critical, long-lived components — crypto libraries, kernels, hypervisors — justify theorem proving or SMT-based verification
• For whole applications, combine abstract-interpretation static analysis with fuzzing: sound warnings from one side, concrete counterexamples from the other
• Protocols and state machines (such as login flows) suit model checking well
• Simply writing down what "Safe" means as a formula is often the cheapest way to find holes in a specification

Summary

• "Safe for every input" formalizes as ∀x ∈ Σ*, S(P(x)); including intermediate behavior means writing it over traces
• Existence (∃) is shown by one counterexample; non-existence (∀) cannot be shown by testing alone
• An attack is a search for the x in ∃x ¬Safe(P, x)
• Formalizing is not proving; proof in general is undecidable by the halting problem and Rice's theorem
• Hoare logic, model checking, SAT/SMT, theorem proving, and abstract interpretation each sidestep that wall differently
• Different vulnerability classes change the very shape of the formula: safety, hyperproperty, or liveness

Which of these formulas famous real-world vulnerabilities violated is covered in "What Is a CVE? Learning from Log4Shell, Heartbleed, EternalBlue, and XZ Utils".