Test suite Anda memiliki cakupan 94% dan nol kegagalan. Sebuah symbolic execution engine menemukan crash di kode Anda dalam waktu kurang dari tiga detik.

Testnya tidak rusak. Metric cakupan tidak berbohong. Masalahnya adalah testing memverifikasi perilaku di titik-titik spesifik. Symbolic execution memverifikasi perilaku di seluruh region ruang input. Tidak peduli berapa banyak contoh yang Anda tulis jika bug tinggal di celah di antara dua contoh tersebut.

Apa yang Sebenarnya Dilakukan Symbolic Execution

Symbolic execution adalah teknik analisis program yang menjalankan kode Anda pada variabel simbolik alih-alih nilai konkret. Test normal melewatkan x = 5 ke fungsi. Sebuah symbolic execution engine melewatkan x = α, di mana α merepresentasikan setiap integer yang mungkin.

Saat kode berjalan, engine melacak constraints. Saat menemukan branch seperti if (x > 0), engine tidak memilih arah. Ia mem-fork execution. Satu jalur membawa constraint α > 0. Jalur lainnya membawa α ≤ 0. Kedua jalur berlanjut secara independen.

Ketika sebuah jalur mencapai assertion, akses memori, atau potensi crash site, engine bertanya pada SMT solver sebuah pertanyaan sederhana: “Apakah ada nilai α yang memenuhi semua constraint di jalur ini dan juga melanggar safety property ini?” Jika solver menjawab ya, ia memberikan counterexample konkret. Anda sekarang memiliki input spesifik yang memicu bug yang tidak pernah Anda tulis test untuknya.

Bug yang Unit Test Anda Tidak Akan Tangkap

Pertimbangkan fungsi yang memvalidasi batas array sebelum menyalin:

int copy_slice(const char *src, size_t src_len,
               size_t offset, size_t count) {
    if (offset > src_len) return -1;
    if (count > 1024) return -1;

    size_t end = offset + count;
    if (end > src_len) return -1;

    char dst[1024];
    memcpy(dst, src + offset, count);
    return 0;
}

Test suite Anda terlihat masuk akal:

void test_copy_slice_normal() {
    assert(copy_slice("hello", 5, 1, 3) == 0);
}

void test_copy_slice_too_long() {
    assert(copy_slice("hi", 2, 0, 1025) == -1);
}

void test_copy_slice_bad_offset() {
    assert(copy_slice("hi", 2, 5, 1) == -1);
}

Semua hijau. Tapi offset dan count adalah size_t, integer unsigned. Di sistem 64-bit, offset + count bisa melipat kembali ke angka kecil jika keduanya besar. Jika offset = 0xFFFFFFFFFFFFFFFF dan count = 1, maka end = 0, yang tidak lebih besar dari src_len. Pengecekan batas lolos. memcpy membaca dari alamat yang tidak valid.

Tidak ada pengembang yang masuk akal menulis test case dengan offset = 2^64 - 1. Ruang input sangat besar. Symbolic execution tidak memerlukan Anda untuk menebak input yang buruk. Ia mengeksplorasi jalur di mana wraparound terjadi dan meminta solver untuk menemukan nilai yang memenuhi constraint end ≤ src_len sementara offset + count overflow. Solver mengembalikan counterexample dalam milidetik.

Bagaimana Engine Mengeksplorasi Jalur

Mekanisme inti adalah pengumpulan constraint dan path forking. Setiap pernyataan kondisional di kode Anda menjadi titik branch. Engine mempertahankan path constraint, formula boolean yang merepresentasikan semua kondisi yang harus benar agar execution mencapai titik saat ini.

Di setiap branch, engine meng-query solver:

  1. Apakah path constraint saat ini ditambah kondisi true-branch satisfiable?
  2. Apakah path constraint saat ini ditambah kondisi false-branch satisfiable?

Jika keduanya satisfiable, engine melakukan fork. Ia mengantrekan kedua jalur untuk eksplorasi. Inilah cara symbolic execution mencapai exhaustive path coverage untuk program yang terbatas.

Ketika sebuah jalur mencapai crash, akses di luar batas, atau assertion yang gagal, engine meminta solver untuk satisfying assignment ke input simbolik di bawah path constraint saat ini. Assignment tersebut adalah input trigger bug Anda.

Anda bisa melihat langkah constraint-solving secara langsung dengan Z3, SMT solver yang menggerakkan banyak symbolic execution engine:

from z3 import Solver, BitVec, UGT, ULT, ULE, simplify

solver = Solver()

# Model 32-bit unsigned size_t values
offset = BitVec('offset', 32)
count = BitVec('count', 32)
src_len = BitVec('src_len', 32)

# Path constraints: offset <= src_len, count <= 1024
solver.add(ULE(offset, src_len))
solver.add(ULE(count, 1024))

# We want to find a case where offset + count wraps around
# and the end check passes incorrectly
end = offset + count
solver.add(UGT(end, src_len))  # This should trigger the return -1

# But what if we look for the overflow case where end wraps?
solver2 = Solver()
solver2.add(ULE(offset, src_len))
solver2.add(ULE(count, 1024))
solver2.add(ULT(offset + count, offset))  # unsigned overflow
solver2.add(ULE(offset + count, src_len))  # bogus check passes

if solver2.check() == solver2.sat:
    model = solver2.model()
    print(f"offset={model[offset]}, count={model[count]}")
    # offset=4294967295, count=1 on a 32-bit model

Solver mengembalikan nilai konkret yang memenuhi constraint overflow. Ini adalah inti matematika dari symbolic execution. Engine melakukan ini secara otomatis di setiap branch di program Anda.

Trade-off yang Mencegahnya Menggantikan Test Suite Anda

Symbolic execution tidak gratis. Ada tiga biaya yang membatasi di mana ia praktis.

Path explosion. Setiap pernyataan if menggandakan jumlah jalur. Fungsi dengan 20 branch independen memiliki lebih dari satu juta jalur. Kebanyakan engine menyerah setelah timeout atau path budget. Loop memperburuk ini. Loop yang secara simbolis mengiterasi rentang yang tidak terbatas menciptakan jalur yang tak terhingga banyaknya. Engine biasanya meng-unroll loop sejumlah tetap kali dan melanjutkan.

External state dan system calls. Symbolic execution bekerja paling baik pada pure function. Ketika kode Anda membaca dari file, membuat network request, atau meng-query database, engine tidak tahu nilai apa yang akan kembali. Beberapa tool memodelkan pemanggilan library umum secara heuristik. Yang lain mengharuskan Anda menulis mock models. Ini membosankan dan rawan error.

Solver timeouts. Formula constraint untuk kode nyata kompleks. Array, bitvector, floating-point arithmetic, dan matematika non-linear bisa mendorong SMT solver ke waktu eksponensial. Jalur yang membutuhkan mikrodetik untuk dieksekusi secara konkret mungkin membutuhkan menit untuk diselesaikan secara simbolis. Engine menjatuhkan jalur-jalur ini dan melaporkannya sebagai unresolved.

Karena batasan ini, symbolic execution adalah pelengkap testing, bukan pengganti. Ia menemukan kasus sudut yang dalam. Test Anda memverifikasi kasus umum dan perilaku integration.

Tiga Cara Mencobanya pada Kode Nyata

Anda tidak memerlukan PhD untuk menjalankan symbolic execution. Tool modern menyembunyikan sebagian besar kompleksitas.

Untuk C/C++: KLEE. KLEE adalah symbolic execution engine open-source klasik yang dibangun di atas LLVM. Anda mengompilasi kode Anda ke LLVM bitcode dengan clang -emit-llvm, lalu menjalankan klee pada hasilnya. KLEE telah menemukan bug serius di GNU coreutils, SQLite, dan codebase C lain yang banyak digunakan.

clang -emit-llvm -c -g copy_slice.c -o copy_slice.bc
klee --max-time=60 copy_slice.bc

KLEE mengeluarkan file .ktest untuk setiap bug yang ditemukan. Anda bisa memutar ulang dengan runtime kecil untuk melihat input eksaknya.

Untuk Python dan biner: angr. angr adalah framework Python untuk symbolic execution, binary analysis, dan reverse engineering. Ia bekerja pada biner yang dikompilasi, jadi Anda tidak memerlukan source code. Anda menulis skrip Python untuk menyiapkan register dan memori simbolik, lalu membiarkan angr mengeksplorasi.

import angr

proj = angr.Project("./copy_slice")
state = proj.factory.entry_state()
sm = proj.factory.simulation_manager(state)
sm.explore(find=lambda s: b"crash" in s.posix.dumps(1))

angr lebih lambat dari KLEE tapi menangani biner dunia nyata dengan semua konvensi pemanggilan berantakan dan dependency library mereka.

Untuk Rust: Kani. Kani adalah verifier khusus Rust yang dibangun di atas CBMC. Anda memberi anotasi fungsi dengan #[kani::proof] dan menjalankan cargo kani. Ia memeriksa arithmetic overflow, akses di luar batas, dan kegagalan assertion menggunakan symbolic execution di balik layar.

#[kani::proof]
fn check_copy_slice() {
    let src = kani::any_slice::<u8, 1024>();
    let offset: usize = kani::any();
    let count: usize = kani::any();
    kani::assume(count <= 1024);
    let _ = copy_slice(src, src.len(), offset, count);
}

Kani adalah on-ramp termudah jika Anda sudah berada di ekosistem Rust. Ia terintegrasi dengan cargo dan memberikan error trace dalam format yang familier.

Pertanyaan yang Sering Diajukan

Apakah symbolic execution menggantikan fuzzing?

Tidak. Fuzzing menghasilkan input acak dan mengamati crash. Symbolic execution bernalar tentang jalur dan menemukan input yang memenuhi constraint spesifik. Fuzzing diskalakan ke program besar dan proses panjang. Symbolic execution menemukan bug yang lebih dalam di region yang lebih kecil. Kedua teknik bekerja dengan baik bersama-sama. Tool seperti Driller dan QSYM menggabungkannya, menggunakan fuzzing untuk coverage dan symbolic execution untuk branch yang sulit dijangkau.

Bisakah symbolic execution membuktikan kode saya tidak memiliki bug?

Hanya untuk program terbatas tanpa loop tak terbatas dan tanpa dependency eksternal. Untuk kebanyakan kode produksi, symbolic execution bisa membuktikan ketiadaan kelas bug tertentu hingga batas kedalaman jalur. Ia tidak bisa membuktikan total correctness.

Berapa lama waktu yang dibutuhkan untuk dijalankan?

Menit hingga jam untuk fungsi kecil. Symbolic execution bukan kecepatan dewa CI. Jalankan pada fungsi keamanan kritis, parser, dan kode pengecekan batas. Jangan mencoba secara simbolis mengeksekusi seluruh web framework Anda.

Mulai dengan Satu Fungsi

Anda tidak perlu secara simbolis mengeksekusi seluruh codebase. Pilih satu fungsi di mana bug akan menyakitkan. Sebuah parser. Sebuah pengecekan otorisasi. Sebuah buffer copy.

Tulis harness KLEE, skrip angr, atau proof Kani. Jalankan. Saksikan ia menemukan input yang tidak pernah Anda tulis test untuk. Perbaiki bug. Tidur lebih nyenyak.

Tujuannya bukan menggantikan test Anda. Tujuannya adalah berhenti berpura-pura bahwa cakupan 94% berarti keamanan 94%. Symbolic execution menemukan celah-celahnya. Test Anda tidak akan pernah.