Azhar's Notes

Formal Verification Deep Dive — TLA+, Proof Assistants, and Rust Verification

4 menit baca

Ringkasan & Hubungan ke Vault

Metode testing tradisional (unit, integration, fuzzing) hanya membuktikan adanya bug, bukan meniadakan bug. Untuk sistem kritis berskala enterprise seperti engine proxy jarsWAF, verifikasi formal (formal verification) membuktikan kebenaran spesifikasi dan kode secara matematis. Catatan ini melengkapi software-quality-untung-yuhana dengan aspek pembuktian program secara rigit.

Daftar Isi

  1. Spesifikasi Formal dengan TLA+
  2. Model Checking (SPIN, Alloy, NuSMV)
  3. Proof Assistants (Coq, Lean, Isabelle)
  4. Verifikasi Kode Rust dengan Kani & Verus
  5. Koneksi ke Vault

1. Spesifikasi Formal dengan TLA+

TLA+ (Temporal Logic of Actions) adalah bahasa spesifikasi formal yang dirancang oleh Leslie Lamport untuk mendesain dan memverifikasi sistem konkuren dan terdistribusi. TLA+ berfokus pada pembuktian logika sebelum kode ditulis.

1.1 Contoh Spesifikasi TLA+ Sederhana (Mutual Exclusion Lock)

Spesifikasi berikut mendefinisikan sistem penguncian (locking) konkuren sederhana dengan dua proses untuk membuktikan properti safety (tidak terjadi kebuntuan/deadlock):

---------------------- MODULE SimpleLock ----------------------
EXTENDS Naturals, TLC
 
VARIABLES lock_state, process_owner
 
Vars == <<lock_state, process_owner>>
 
Init ==
    /\ lock_state = "Unlocked"
    /\ process_owner = 0
 
(* Proses p mencoba mengakuisisi lock *)
Acquire(p) ==
    /\ lock_state = "Unlocked"
    /\ lock_state' = "Locked"
    /\ process_owner' = p
 
(* Proses p melepaskan lock *)
Release(p) ==
    /\ lock_state = "Locked"
    /\ process_owner = p
    /\ lock_state' = "Unlocked"
    /\ process_owner' = 0
 
Next ==
    \exists p \in {1, 2} : Acquire(p) \/ Release(p)
 
Spec == Init /\ [][Next]_Vars
 
(* Properti Keamanan (Mutual Exclusion) *)
MutualExclusion ==
    (lock_state = "Unlocked") \/ (process_owner \in {1, 2})
==============================================================

TLC Model Checker akan mengeksplorasi seluruh state space yang mungkin dari spesifikasi di atas untuk memastikan invariant MutualExclusion tidak pernah terlanggar (safety) dan tidak terjadi kondisi di mana sistem terhenti tanpa transisi berikutnya (liveness).

2. Model Checking (SPIN, Alloy, NuSMV)

Model Checking adalah metode otomatis untuk membuktikan apakah model sistem memenuhi properti spesifikasi temporal tertentu secara tuntas (exhaustive state space exploration).

  • SPIN: Menggunakan bahasa Promela (Process Meta Language). Sangat kuat untuk memverifikasi protokol komunikasi konkuren berbasis pertukaran pesan (message passing).
  • Alloy: Menggunakan logika orde-pertama untuk memodelkan struktur data relasional. Baik untuk menganalisis kelemahan desain arsitektur database.
  • NuSMV: Model checker simbolik untuk memverifikasi logika CTL/LTL pada desain sirkuit perangkat keras digital atau sistem otomasi.

3. Proof Assistants (Coq, Lean, Isabelle)

Berbeda dengan model checker yang memeriksa state space secara otomatis (tapi terbatas pada ukuran memori), Proof Assistants adalah perangkat lunak interaktif (interactive theorem provers) yang membantu manusia menyusun bukti matematika formal tanpa batasan ukuran state space.

  • Coq: Berbasis Calculus of Inductive Constructions. Digunakan untuk memverifikasi compiler kritis seperti CompCert (compiler C tersertifikasi bebas bug optimasi).
  • Lean: Sangat populer di kalangan matematikawan modern. Lean digunakan untuk merumuskan dan membuktikan teorema-teoreorema matematika tingkat lanjut secara formal.
  • Isabelle/HOL: Proof assistant interaktif berbasis Higher-Order Logic. Digunakan untuk membuktikan kernel sistem operasi seperti seL4 (microkernel komersial pertama yang terverifikasi aman secara formal).

4. Verifikasi Kode Rust dengan Kani & Verus

Untuk menjembatani teori verifikasi formal dengan kode nyata, komunitas Rust mengembangkan perkakas khusus yang menganalisis kode Rust secara matematis.

4.1 Kani Rust Verifier (Model Checking berbasis CBMC)

Kani membuktikan kode Rust menggunakan Bounded Model Checking (BMC) di tingkat representasi compiler (MIR). Kani dapat membuktikan properti keamanan memori (tidak ada panic, out-of-bounds, overflow) untuk semua nilai input yang mungkin.

// Contoh kode Rust yang akan diverifikasi oleh Kani
pub fn safe_division(numerator: i32, denominator: i32) -> Option<i32> {
    if denominator == 0 {
        None
    } else {
        Some(numerator / denominator) // Aman dari pembagian nol
    }
}
 
#[cfg(kani)]
#[kani::proof]
fn verify_safe_division() {
    // Membuat input simbolis yang mewakili SEMUA nilai i32 yang mungkin
    let num: i32 = kani::any();
    let den: i32 = kani::any();
 
    let result = safe_division(num, den);
 
    if den == 0 {
        assert!(result.is_none());
    } else {
        assert!(result.is_some());
    }
}

Jalankan verifikasi menggunakan Kani CLI:

cargo kani
# Output: VERIFICATION SUCCESSFUL (membuktikan matematis tidak akan pernah crash)

4.2 Verus

Verus adalah perkakas verifikasi formal untuk Rust yang memungkinkan penulisan spesifikasi fungsional (pre-conditions, post-conditions, invariants) langsung di dalam kode Rust menggunakan penanda khusus. Kompiler Verus membuktikan bahwa implementasi kode Rust dijamin 100% memenuhi spesifikasi tersebut sebelum dijalankan.

5. Koneksi ke Vault

CatatanHubungan
software-quality-untung-yuhanaKonsep dasar SQAP dan metodologi jaminan kualitas perangkat lunak konvensional.
threat-modeling-deepdiveIdentifikasi model ancaman yang logikanya dibuktikan menggunakan spesifikasi formal.
jarswaf-planRencana penerapan verifikasi formal pada core engine jarsWAF sebagai prioritas #2.

Tampilan Grafik

Tautan Balik