Z3 — Motorul de deducție matematică și verificare formală

Ce este Z3?

Z3 este un SMT Solver (Satisfiability Modulo Theories) dezvoltat de Microsoft Research, lansat inițial în 2007. În termeni simpli, Z3 este un motor care decide automat dacă o mulțime de constrângeri logice poate fi satisfăcută și, în caz afirmativ, găsește o soluție.

Ce îl face special:

Automat — nu trebuie să scrii demonstrația, doar specifici problema
Rapid — poate verifica milioane de constrângeri pe secundă
General — acoperă aritmetică, vectori, șiruri, biti, funcții, cuantificatori
Folosit în producție — AWS, Azure, securitate, criptografie, optimizare

1. Ce înseamnă SMT?

SAT (Boolean Satisfiability)

Problema SAT: există o asignare de valori true/false pentru variabilele booleene astfel încât o formulă să fie adevărată?

$$(x \lor y) \land (\lnot x \lor z) \land (\lnot y \lor \lnot z)$$

Un SAT solver găsește automat: $x = true, y = false, z = false$ (sau alte combinații).

SMT (Satisfiability Modulo Theories)

SMT extinde SAT cu teorii de fond — nu doar true/false, ci și:

Aritmetică — $x + y > 10$
Șiruri — $s_1 \cdot s_2 = "hello"$
Vectori / array-uri — $a[i] = 5$
Bitvectori — operații pe biți
Tipuri de date — liste, arbori, opționale

Exemplu: În SAT nu poți exprima $x + y > 10$. În SMT (cu Z3), da.

2. Cum funcționează Z3 pe dinăuntru

Arhitectura pe stratificare

Problema (Python/SMT-LIB)
        ↓
   Parser & Type Checker
        ↓
   Simplifier (algebraic rewrite)
        ↓
   SAT Solver (CDCL) ←→ Theory Solvers (EUF, LRA, LIA, BV, Arrays...)
        ↓
   Model / unsat / unknown

CDCL — Conflict-Driven Clause Learning

Inima lui Z3 e un algoritm CDCL (Conflict-Driven Clause Learning), o extensie modernă a algoritmului DPLL:

Alege o variabilă și îi atribuie o valoare
Propagă — deduce consecințe (unit propagation)
Dacă apare un conflict — învață o nouă clauză care previne același conflict
Backtrack și reia

Theory Solvers

Când SAT solver-ul întâlnește o constrângere teoretică (ex: $x + y = 5$), o trimite la theory solver-ul specializat:

Arithmetic solver — eliminare Gaussiană, simplex
Bitvector solver — saturare pe biți, BDD-uri
Array solver — teoria array-urilor (read-over-write)
String solver — automat finit, length constraints

Cheia eficienței: Theory solver-ul comunică înapoi noi clauze (theory lemmas) care ajută SAT solver-ul să nu exploreze ramuri imposibile.

3. Programare cu Z3 (Python)

3.1 Instalare

pip install z3-solver

3.2 Exemplu de bază

from z3 import *

x = Int('x')
y = Int('y')

solve(x > 5, y < 10, x + y == 20)
# [y = 6, x = 14]

3.3 Tipuri de variabile

# Booleene
p = Bool('p')
q = Bool('q')

# Întregi
a = Int('a')
b = Int('b')

# Reale
r = Real('r')

# Bitvectori (ex: pe 8 biți)
bv = BitVec('bv', 8)

# Șiruri
s = String('s')
t = String('t')

3.4 Constrângeri combinate

x = Int('x')
y = Int('y')

solver = Solver()
solver.add(x > 0)
solver.add(y > 0)
solver.add(x * y == 12)
solver.add(x + y == 8)

if solver.check() == sat:
    print(solver.model())  # [x = 6, y = 2] sau [x = 2, y = 6]
else:
    print("unsat")

3.5 Cuantificatori

x = Int('x')
y = Int('y')

# Pentru toți x, există y astfel încât y > x
solver.add(ForAll([x], Exists([y], y > x)))

print(solver.check())  # sat (evident, întregii sunt infiniti)

3.6 Optimizare (MaxSMT)

opt = Optimize()
x = Int('x')
y = Int('y')

opt.add(x > 0)
opt.add(y > 0)
opt.add(x + y <= 10)

opt.maximize(x * y)  # găsește maximul produsului

if opt.check() == sat:
    print(opt.model())  # [x = 5, y = 5], produs = 25

4. Aplicații practice reale

4.1 AWS Zelkova (Cloud Security)

Amazon folosește Z3 pentru a verifica politicile de securitate IAM. Exemplu:

Permiți accesul la resursa S3:users/boss?
Politica: Allow dacă user = "admin" SAU IP-range = 10.0.0.0/8
User: "guest", IP: 10.0.1.5

Z3 verifică automat: există o cale prin care un utilizator neautorizat poate accesa o resursă? Dacă Z3 zice unsat, configurația e sigură.

4.2 Azure Resource Manager

Azure folosește Z3 pentru a verifica constrângeri de rețea, dependențe între resurse și politici de securitate înainte de deploy.

4.3 Criptografie și securitate

Z3 e folosit pentru:

Cryptanalysis — găsirea de atacuri asupra cifrurilor
Reverse engineering — deducerea constrângerilor dintr-un binar
Fuzzing ghidat — generarea de intrări care explorează căi noi (ex: AFL + Z3)

4.4 Sisteme embedded

Arm Holdings folosește Z3 pentru verificarea modelelor de memorie și a protocoalelor de coerență (cache coherence).

4.5 Planificare și optimizare

De la orarul școlar la rutarea în rețele — Z3 poate găsi soluții la probleme combinatoriale cu mii de variabile.

5. Z3 în contextul verificării formale

Comparație cu alte instrumente

Instrument	Tip	Automat?	Expresivitate	Utilizare
Z3	SMT solver	Da	Medie	AWS, Azure, securitate
Isabelle/HOL	Theorem prover	Semi-automat	Foarte înaltă	seL4, CakeML
Coq	Theorem prover	Manual	Foarte înaltă	CompCert
CBMC	Bounded model checker	Da	Scăzută	Verificare C
Dafny	Verifier înglobat	Semi-automat	Medie	Programare generală

Z3 e cel mai automat — nu trebuie să scrii demonstrația, doar problema. Dar e și mai puțin expresiv — nu poate demonstra orice proprietate.

Cum se integrează Z3 cu alte limbaje

Limbaj	Bibliotecă
Python	`z3-solver`
C++	`#include <z3++.h>`
Java	`com.microsoft.z3`
Rust	`z3` (wrapper)
Go	`go-z3`
JavaScript	`z3-solver` (WebAssembly)

6. Limitări

Indecidabilitate — Pentru teorii cu cuantificatori peste întregi, problema e indecidabilă (Teorema lui Gödel). Z3 poate răspunde unknown.
Explozia exponențială — Probleme cu mii de variabile booleene pot fi rezolvate rapid; milioane — deja greu.
Non-linear arithmetic — $x \cdot y \cdot z = 1000$ cu variabile nelineare e dificil.
Sisteme hibride — Z3 nu poate verifica direct sisteme cu timp continuu (ecuații diferențiale).
Necesită formalizare — Trebuie să traduci problema în constrângeri logice, ceea ce poate fi dificil.

7. Exercițiu practic: Verifică un program

Să zicem că ai funcția:

def binary_search(arr, target):
    low, high = 0, len(arr) - 1
    while low <= high:
        mid = (low + high) // 2
        if arr[mid] == target:
            return mid
        elif arr[mid] < target:
            low = mid + 1
        else:
            high = mid - 1
    return -1

Vrei să verifici că nu accesezi niciodată indexul în afara limitelor. Cu Z3:

from z3 import *

arr_len = Int('arr_len')
low = Int('low')
high = Int('high')
mid = Int('mid')

s = Solver()
s.add(arr_len > 0)
s.add(low >= 0)
s.add(high < arr_len)
s.add(low <= high)
s.add(mid == (low + high) // 2)

# Verific: mid e întotdeauna între 0 și arr_len-1?
s.add(Not(And(mid >= 0, mid < arr_len)))

result = s.check()
if result == unsat:
    print("✅ Accesul la mid e întotdeauna safe!")
else:
    print(f"❌ Contraspemplu: {s.model()}")

Concluzie

Z3 e unul dintre cele mai practice instrumente de verificare formală — rapid, automat, bine documentat și folosit în producție la scară largă. Nu trebuie să fii logician ca să-l folosești: instalezi pip install z3-solver și începi să rezolvi probleme.

Pentru aprofundare, vezi articolul despre Verificarea Matematică a Software-ului, care plasează Z3 în contextul mai larg al verificării formale.

Referințe

De Moura, L. & Bjørner, N. Z3: An Efficient SMT Solver (TACAS 2008)
Microsoft Research. Z3 Documentation. https://github.com/Z3Prover/z3
Barrett, C. et al. The SMT-LIB Standard (2024)
AWS. Zelkova: Using Z3 for Cloud Security. https://aws.amazon.com/blogs/security/
Bjørner, N. SMT Solving: A Tutorial