Bounded Static Analysis

Everything Everywhere All at Once

What is Bounded Static Analysis?
Abstractions
Bounded Abstract Interpretation

Questions

Why should we use abstractions when analyzing code?
What is the advantage of Galois connections?
Which cases can the Sign abstraction not catch?

What is Bounded Static Analysis? (§1)

Goal and Notation (§1.1)

p, n ⊢_{𝐁 𝐒 𝐀}^{𝗆 𝗎 𝗌 𝗍} Q ⟹ p, n ⊨^{𝗆 𝗎 𝗌 𝗍} Q

\neg (p, n ⊢_{𝐁 𝐒 𝐀}^{\neg 𝗆 𝖺 𝗒} \neg Q) \equiv p, n ⊢_{𝐁 𝐒 𝐀}^{𝗆 𝗎 𝗌 𝗍} Q

p, n ⊨^{𝗆 𝖺 𝗒} Q ⟹ p, n ⊢_{𝐁 𝐒 𝐀}^{\neg 𝗆 𝖺 𝗒} \neg Q

𝚊 𝚎 (τ) \equiv τ_{| τ | - 1} = err (‘𝚊𝚜𝚜𝚎𝚛𝚝𝚒𝚘𝚗 𝚎𝚛𝚛𝚘𝚛’)

p, n ⊨^{𝗆 𝗎 𝗌 𝗍} \neg 𝚊 𝚎 \equiv \forall τ \in {Sem}^{n} (p) . \neg 𝚊 𝚎 (τ)

\neg (p, n ⊢_{𝐁 𝐒 𝐀}^{\neg 𝗆 𝖺 𝗒} 𝚊 𝚎) \equiv p, n ⊢_{𝐁 𝐒 𝐀}^{𝗆 𝗎 𝗌 𝗍} \neg 𝚊 𝚎

The Many Step Function (§1.2)

Breath-first!

Δ_{p} (T) = {τ^{'} s | s \in Σ, τ^{'} \in T, δ_{p} ({τ^{'}}_{| τ^{'} |}, s)}

\begin{matrix} Δ_{p}^{0} & = I_{p} \\ Δ_{p}^{n} & = Δ_{p} (Δ_{p}^{n - 1}) \cup Δ_{p}^{n - 1} \end{matrix}

\begin{matrix} Δ^{𝗆 𝗎 𝗌 𝗍} (T) \subseteq Δ (T) \subseteq Δ^{𝗆 𝖺 𝗒} (T) \end{matrix}

Δ^{𝗆 𝗎 𝗌 𝗍, n} \subseteq Δ^{n} \subseteq Δ^{𝗆 𝖺 𝗒, n}

p, n ⊢_{𝐁 𝐒 𝐀}^{\neg 𝗆 𝖺 𝗒} Q \equiv \exists τ \in Δ^{𝗆 𝖺 𝗒, n} . Q (τ)

p, n ⊢_{𝐁 𝐒 𝐀}^{\neg 𝗆 𝗎 𝗌 𝗍} Q \equiv \forall τ \in Δ^{𝗆 𝗎 𝗌 𝗍, n} . Q (τ)

Abstractions (§2)

The Sign Analysis
Partially Ordered Sets (Posets)
Lattices
Galois Connection
Abstract Operations

The Sign Analysis (§2.1)

𝐒 𝐢 𝐠 𝐧 = {+, 0, -}

$α$ is the abstractor

\begin{matrix} α ({1, 2, 3}) = & {+} \\ α ({0}) = & {0} \\ α ({- 1, 3}) = & {+, -} \\ α ({- 1, 0, 3}) = & {0, +, -} \end{matrix}

Fasten your seatbelts it's going to be a bumpy night!

Partially Ordered Sets (Posets) (§2.2)

A partially ordered set $(L, ⊑)$

\begin{matrix} reflexive & \forall a \in L . a ⊑ a \\ antisymmetric & \forall a, b \in L . a ⊑ b \land b ⊑ a ⟹ a = b \\ transitive & \forall a, b, c \in L . a ⊑ b \land b ⊑ c ⟹ a ⊑ c \end{matrix}

Examples

Integers in both directions $(ℤ, \geq)$ $(ℤ, \leq)$
Sets $({𝚝 𝚝, 𝚏 𝚏}, \Rightarrow)$
Signed $(2^{𝐒 𝐢 𝐠 𝐧}, \subseteq)$

class Poset(ABC):
    @abstractmethod
    def __eq__(self, other: Self) -> bool: ...

    @abstractmethod
    def __lt__(self, other: Self) -> bool: ...

    def __le__(self, other: Self) -> bool:
        return self == other or self < other

    @abstractmethod
    def __gt__(self, other: Self) -> bool: ...

    def __ge__(self, other: Self) -> bool:
        return self == other or self > other

def is_reflexive(a: Poset):
    assert a == a

def is_antisymmetric(a: Poset, b: Poset):
    if a != b:
        assert not (a <= b <= a)

def is_transitive(a: Poset, b: Poset, c: Poset):
    if a <= b <= c:
        assert a <= c

@given(st_signset(), st_signset(), st_signset())
def test_signset_is_poset(a: ab.SignSet, b: ab.SignSet, c: ab.SignSet):
    ...
    is_transitive(a, b, c)

Why Not Total Orders?

Lattices (§2.3)

Partial orders $(L, ⊑_{L})$ ,
meet $⊓$ ,
join $⊔$ ,
and has a smallest and biggest element.

Hasse diagrams. (§2.3.1)

A Hasse diagram over the poset $(2^{𝐒 𝐢 𝐠 𝐧}, \subseteq)$ . By I, KSmrq, CC BY-SA 3.0 (with edits)

Back to the Sign Abstraction (§2.3.2)

$⊑_{𝐒 𝐢 𝐠 𝐧} = \subseteq$ , $⊥ = \emptyset$ , and $⊤ = {+, -, 0}$

Galois Connection (§2.4)

\forall a \in C, b \in A . a ⊑_{C} γ (b) \Leftrightarrow α (a) ⊑_{A} b

(A Galois Connection is a connection between two ordered sets, with a concretion $γ$ and an abstraction $α$ function.)

What are they good for?

A mathematical definition of one-sided information loss. If my abstraction finds a bug, is there a bug in the original domain?
A weak equality.

Laws For Free

\begin{matrix} c ⊑_{C} γ (α (c)) & – if we abstract we only increase in size \\ α (γ (a)) ⊑_{A} a & – if we concretize we only decrease in size \\ α (γ (α (c))) = α (c) & – we don’t keep losing information \\ γ (α (γ (a))) = γ (a) & – in both directions \\ γ (a_{1} ⊔_{A} a_{2}) = γ (a_{1}) ⊔_{C} γ (a_{2}) & – γ preserves joins. \\ α (c_{1} ⊓_{C} c_{2}) = α (c_{1}) ⊓_{A} α (c_{2}) & – α preserves meets. \end{matrix}

Adjunctions and Testing

# Most of the time
parse(pretty(a)) == a 

# Always
pretty(parse(pretty(a))) == pretty(a)

# Bonus for all strings s:
parse(pretty(parse(s))) == parse(s)

Back to the Sign Analysis (§2.4.1)

\begin{matrix} α (N) & = {+ | n \in N, n < 0} \\ \cup {- | n \in N, n > 0} \\ \cup {0 | n \in N, n = 0} \\ γ (S) & = {n | n \in ℤ, n < 0, + \in S} \\ \cup {n | n \in ℤ, n > 0, - \in S} \\ \cup {0 | 0 \in S} \end{matrix}

Build the Sign Abstraction

def to_sign(value: jvms.StackValue) -> Sign:
    match value:
        case jvms.StackInt(v):
            return (v > 0) - (v < 0)
        case a:
            raise NotImplementedError(f"Unsupported value {value!r}")

class SignSet:
  ...
  @classmethod
  def abstract(cls, items : Iterable[jvms.StackValue]): 
    signs = set()
    for value in values:
        signs.add(to_sign(value))
    return cls(frozenset(signs))

def __contains__(self, value : jvms.StackValue): 
    return to_sign(value) in self.signs

Test your abstaction

\forall X \subset 2^{ℤ} : X \subseteq γ (α (X))

see solutions/static/tests/test_abstractions.py

Abstract Operations (§2.5)

$A +_{2^{32}} B \subseteq γ (α (A) +_{𝐒 𝐢 𝐠 𝐧} α (B))$

$α (A +_{2^{32}} B) \subseteq α (A) +_{𝐒 𝐢 𝐠 𝐧} α (B)$

Define the operation

\begin{matrix} {+} +_{𝐒 𝐢 𝐠 𝐧} {+} = & {+} & {+} +_{𝐒 𝐢 𝐠 𝐧} {-} = {-, +, 0} \\ {+} +_{𝐒 𝐢 𝐠 𝐧} {0} = & {+} & {0} +_{𝐒 𝐢 𝐠 𝐧} {+} = {+} \\ {0} +_{𝐒 𝐢 𝐠 𝐧} {-} = & {-} & {0} +_{𝐒 𝐢 𝐠 𝐧} {0} = {0} \\ {-} +_{𝐒 𝐢 𝐠 𝐧} {+} = & {-, +, 0} & {-} +_{𝐒 𝐢 𝐠 𝐧} {-} = {-} \\ {-} +_{𝐒 𝐢 𝐠 𝐧} {0} = & {-} & \dots \end{matrix}

match opr:
    case jvm.BinaryOpr.Add:
        output = set()
        if 1 in self.signs:
            output.add(1)
            if -1 in other.signs:
                output.update([0, -1])

        if -1 in self.signs:
            output.add(-1)
            if 1 in other.signs:
                output.update([0, 1])

        if 0 in self.signs:
            output.update(other.signs)

        return (SignSet(output), set())

Bounded Abstract Interpretation (§3)

$(2^{𝐓 𝐫 𝐚 𝐜 𝐞}, \subseteq) \leftrightarrow_{γ}^{α} (A, ⊑_{A})$

\begin{matrix} Δ_{A}^{0} & = α (I_{P}) \\ Δ_{A}^{n} & = Δ_{A} (Δ_{A}^{n - 1}) ⊔_{A} Δ_{A}^{n - 1} \end{matrix}

To show $Δ^{n} \subseteq γ (Δ_{A}^{n})$ , we need to prove:

Δ (T) \cup T \subseteq γ (Δ_{A} (α (T)) ⊔_{A} α (T)) .

But we can get away with

α (Δ (T)) ⊑_{A} Δ_{A} (α (T))

The State Abstraction (§3.1)

(2^{𝐓 𝐫 𝐚 𝐜 𝐞}, \subseteq) \leftrightarrow_{γ}^{α} (2^{𝐒 𝐭 𝐚 𝐭 𝐞}, \subseteq)

\begin{matrix} α (T) = {τ_{| τ | - 1} | τ \in T} \\ γ (S) = {τ | s \in S, τ \in 𝐓 𝐫 𝐚 𝐜 𝐞, τ_{| τ | - 1} = s} \end{matrix}

Δ_{𝐒 𝐭 𝐚 𝐭 𝐞} (S) = {s^{'} | s \in S, δ (s, s^{'})}

This is nice because

if $err (‘𝚊𝚜𝚜𝚎𝚛𝚝𝚒𝚘𝚗 𝚎𝚛𝚛𝚘𝚛’) \notin Δ_{𝐒 𝐭 𝐚 𝐭 𝐞}^{n}$ , then
$\neg \exists τ . (τ err (‘𝚊𝚜𝚜𝚎𝚛𝚝𝚒𝚘𝚗 𝚎𝚛𝚛𝚘𝚛’)) \in Δ^{n}$

The Per-Instruction Abstraction (§3.2)

𝐏 𝐜 = ι \to 2^{𝐒 𝐭 𝐚 𝐭 𝐞}

(2^{𝐒 𝐭 𝐚 𝐭 𝐞}, \subseteq) \leftrightarrow_{γ}^{α} (𝐏 𝐜, ⊑_{𝐏 𝐜})

Δ_{𝐏 𝐜} (C) = ⨆_{𝐏 𝐜} {ι^{'} \mapsto {⟨ σ^{'}, λ^{'}, ι^{'} ⟩} | \begin{matrix} (ι \mapsto S) \in C, S^{'} = Δ_{ι} (S), \\ ⟨ σ^{'}, λ^{'}, ι^{'} ⟩ \in S^{'} \end{matrix}}

The Per-Variable Abstraction (§3.3)

𝐏 𝐯 = ι \to (ℕ \mapsto (2^{𝐕_{σ}})) \times (2^{𝐕_{σ}}) *

(𝐏 𝐜, ⊑_{𝐏 𝐜}) \leftrightarrow_{γ}^{α} (𝐏 𝐯, ⊑_{𝐏 𝐯})

Variable Abstractions (§3.4)

𝐏 𝐯 [A] = ι \to (ℕ \mapsto A) \times A *

(2^{𝐕_{σ}}, \subseteq) \leftrightarrow_{γ}^{α} (A, ⊑_{A}) ⟹ (𝐏 𝐯, ⊑_{𝐏 𝐯}) \leftrightarrow_{γ}^{α} (𝐏 𝐯 [A], ⊑_{𝐏 𝐯 [A]})

(𝐏 𝐯, ⊑_{𝐏 𝐯}) \leftrightarrow_{γ}^{α} (𝐏 𝐯 [𝐒 𝐢 𝐠 𝐧], ⊑_{𝐏 𝐯 [𝐒 𝐢 𝐠 𝐧]})

Abstractions All The Way Down. (§3.5)

\begin{matrix} (2^{𝐓 𝐫 𝐚 𝐜 𝐞}, \subseteq) & \leftrightarrow_{γ}^{α} (2^{𝐒 𝐭 𝐚 𝐭 𝐞}, \subseteq) \\ \leftrightarrow_{γ}^{α} (𝐏 𝐜, ⊑_{𝐏 𝐜}) \\ \leftrightarrow_{γ}^{α} (𝐏 𝐯, ⊑_{𝐏 𝐯}) \\ \leftrightarrow_{γ}^{α} (𝐏 𝐯 [𝐒 𝐢 𝐠 𝐧], ⊑_{𝐏 𝐯 [𝐒 𝐢 𝐠 𝐧]}) \end{matrix}

Getting Started

Abstract Your Interpreter
Emit multiple states.
Start Small, Just One frame.

Questions

Why should we use abstractions when analyzing code?
What is the advantage of Galois connections?
Which cases can the Sign abstraction not catch?

Bounded Static Analysis

Table of Contents

Questions

What is Bounded Static Analysis? (§1)

Goal and Notation (§1.1)

The Many Step Function (§1.2)

Abstractions (§2)

The Sign Analysis (§2.1)

Partially Ordered Sets (Posets) (§2.2)

Examples

Why Not Total Orders?

Lattices (§2.3)

Hasse diagrams. (§2.3.1)

Back to the Sign Abstraction (§2.3.2)

Galois Connection (§2.4)

What are they good for?

Laws For Free

Adjunctions and Testing

Back to the Sign Analysis (§2.4.1)

Build the Sign Abstraction

Test your abstaction

Abstract Operations (§2.5)

Define the operation

Bounded Abstract Interpretation (§3)

To show Δn⊆γ(ΔAn), we need to prove:

But we can get away with

The State Abstraction (§3.1)

This is nice because

The Per-Instruction Abstraction (§3.2)

The Per-Variable Abstraction (§3.3)

Variable Abstractions (§3.4)

Abstractions All The Way Down. (§3.5)

Getting Started

Questions

To show $Δ^{n} \subseteq γ (Δ_{A}^{n})$ , we need to prove: