Jawabannya Tidak. Pertanyaan Sebenarnya adalah Apa yang Bisa Ia Buktikan Sebagai Gantinya.
Analisis statis tidak dapat membuktikan bahwa sebuah pesawat tidak akan jatuh. Ia dapat membuktikan bahwa loop kontrol altimeter Anda tidak akan pernah membagi dengan nol, tidak akan pernah mengindeks di luar batas, dan tidak akan pernah meluapkan akumulator titik tetap. Perbedaannya penting karena yang satu adalah klaim tentang fisika, aerodinamika, dan aluminium di bawah tekanan, sedangkan yang lain adalah klaim tentang kode yang dapat Anda verifikasi sebelum pesawat meninggalkan tanah.
Inilah janji interpretasi abstrak. Bukan omnisiensi. Hanya bukti ketat bahwa kategori kegagalan perangkat lunak yang kataklysmik tertentu tidak mungkin terjadi dalam setiap eksekusi yang mungkin.
Mengapa Menguji Sejuta Skenario Masih Membuat Anda Menebak-nebak
Sebuah sistem kontrol penerbangan tipikal berisi ratusan ribu baris kode C. Ruang input adalah produk silang dari pembacaan sensor, perintah pilot, kondisi lingkungan, dan variabel keadaan internal. Anda bisa menjalankan sistem dalam simulator sampai kematian panas alam semesta dan masih belum menutupi setiap jalur.
Pengujian menemukan bug. Ia tidak membuktikan ketiadaannya. Setiap tes yang lulus adalah sebuah titik data. Ia bukan jaminan.
Interpretasi abstrak membalikkan pendekatan tersebut. Alih-alih mengeksekusi program dengan input spesifik, ia mengeksekusi program pada domain abstrak yang mewakili himpunan nilai yang mungkin. Jika analisis abstrak mengatakan bahwa keadaan kesalahan tertentu tidak terjangkau, maka kesalahan tersebut tidak terjangkau untuk setiap input konkret. Buktinya bersifat ekshaustif karena ia mencakup seluruh ruang input dalam satu lintasan.
Nilai Konkret Terlalu Mahal. Gunakan Bentuk Sebagai Gantinya.
Pertimbangkan sebuah variabel sederhana x. Dalam eksekusi konkret, x mungkin bernilai 42. Dalam interpretasi abstrak, x mungkin “sebarang bilangan bulat antara 0 dan 255.” Ini disebut abstraksi interval.
Analyzer melacak interval-interval ini melalui setiap operasi. Jika x adalah [0, 100] dan y adalah [1, 10], maka x / y adalah [0, 100]. Analyzer tahu bahwa pembagian aman karena interval pembagi tidak mencakup nol.
Tetapi jika y adalah [-5, 5], analyzer akan menandai potensi pembagian dengan nol. Ia tidak tahu apakah eksekusi konkret mengenai nol. Ia tahu bahwa nol berada di dalam rentang yang mungkin. Itu sudah cukup untuk mengangkat alarm.
Wawasan kunci, berkat Patrick dan Radhia Cousot pada tahun 1976, adalah bahwa domain abstrak harus merupakan aproksimasi-berlebih yang sahih dari semantik konkret. Setiap perilaku konkret harus dapat direpresentasikan dalam abstraksi. Jika abstraksi aman, program konkret aman. Jika abstraksi memperingatkan, program konkret mungkin baik-baik saja. Tetapi mungkin juga tidak.
Membangun Analisis Interval Mainan dalam Python
Berikut adalah domain abstrak interval yang berfungsi. Ia naif, tetapi mendemonstrasikan mekanismenya.
from dataclasses import dataclass
from typing import Optional
@dataclass(frozen=True)
class Interval:
lo: int
hi: int
def __post_init__(self):
if self.lo > self.hi:
raise ValueError("Empty interval")
def add(self, other: "Interval") -> "Interval":
return Interval(self.lo + other.lo, self.hi + other.hi)
def div(self, other: "Interval") -> Optional["Interval"]:
if other.lo <= 0 <= other.hi:
return None # Potential division by zero
# Simplified: assumes positive divisor for demo
return Interval(self.lo // other.hi, self.hi // other.lo)
def intersect(self, other: "Interval") -> Optional["Interval"]:
lo = max(self.lo, other.lo)
hi = min(self.hi, other.hi)
if lo > hi:
return None
return Interval(lo, hi)
def __repr__(self):
return f"[{self.lo}, {self.hi}]"
def analyze_division(a: Interval, b: Interval) -> None:
result = a.div(b)
if result is None:
print(f"ALERT: {a} / {b} may divide by zero")
else:
print(f"SAFE: {a} / {b} = {result}")Jalankan beberapa kasus:
analyze_division(Interval(10, 20), Interval(2, 5)) # SAFE
analyze_division(Interval(10, 20), Interval(-1, 1)) # ALERT
analyze_division(Interval(10, 20), Interval(0, 5)) # ALERTKasus pertama aman karena setiap pembagi positif. Kasus kedua ditandai karena nol berada di dalam [-1, 1]. Kasus ketiga ditandai karena nol berada di dalam [0, 5].
Perhatikan apa yang terjadi pada kasus ketiga. Program konkret mungkin tidak pernah benar-benar mengeksekusi dengan b = 0. Analyzer tidak mengetahui hal itu. Ia bersifat konservatif secara desain. Inilah pertukaran fundamental.
Pajak Positif Palsu
Sebuah analisis statis yang sahih tidak akan pernah melewatkan bug. Jika crash mungkin terjadi, ia akan melaporkannya. Tetapi ia juga akan melaporkan crash yang mustahil. Positif palsu inilah biaya dari kesahihan.
Dalam praktiknya, biaya ini tinggi. Analisis interval naif dari sebuah loop seperti for (i = 0; i < n; i++) akan sering menyimpulkan bahwa i adalah [0, +∞], bahkan jika n dibatasi. Analyzer kehilangan presisi pada titik-titik penggabungan, di mana dua jalur aliran kontrol bergabung dan keadaan abstrak mereka harus digabungkan.
Alat-alat nyata menggunakan domain yang lebih canggih. Polihedra, oktagon, dan abstraksi predikat melacak hubungan antar variabel. x < y tidak terlihat oleh interval, tetapi domain polihedral mengingatnya. Domain-domain ini lebih presisi. Mereka juga lebih mahal. Domain polihedral memiliki kompleksitas kasus terburuk eksponensial. Untuk sistem kontrol penerbangan dengan 300.000 baris kode C, implementasi naif tidak akan berhenti sebelum pesawat tersebut pensiun.
Apa yang Sebenarnya Dibuktikan Astrée pada A380
Astrée adalah alat analisis statis yang membuat interpretasi abstrak terkenal dalam dunia penerbangan. Pada tahun 2003, Astrée dijalankan terhadap perangkat lunak kontrol penerbangan utama Airbus A380. Ia membuktikan ketiadaan setiap kesalahan waktu eksekusi. Tidak ada pembagian dengan nol. Tidak ada akses array di luar batas. Tidak ada aritmetika overflow. Tidak ada kode yang tidak terjangkau di jalur kritis.
Ia tidak membuktikan bahwa pesawat tidak akan jatuh. Ia tidak membuktikan bahwa hukum kontrol benar. Ia tidak membuktikan bahwa perhitungan angle-of-attack cocok dengan fisika pesawat. Itu adalah masalah yang berbeda, diselesaikan dengan alat yang berbeda.
Astrée membuktikan bahwa perangkat lunak tidak akan menghancurkan dirinya sendiri. Itu adalah klaim yang lebih sempit dari yang terdengar, dan lebih berharga daripada yang disadari kebanyakan orang. Penghancuran diri perangkat lunak adalah penyebab umum kecelakaan penerbangan. Membuktikan bahwa hal itu tidak mungkin terjadi sepadan dengan usaha.
Alat ini mencapai hal ini dengan menggabungkan beberapa trik khusus domain. Ia menggunakan domain non-relasional untuk kecepatan dan domain relasional untuk presisi. Ia menangani aritmetika floating-point dengan model yang memperhitungkan kesalahan pembulatan. Ia memahami subset C spesifik yang digunakan dalam avionik dan memperlakukan perilaku tak terdefinisi sebagai kesalahan. Butuh bertahun-tahun penyetelan untuk mendapatkan tingkat positif palsu yang cukup rendah sehingga para insinyur mempercayai outputnya.
Kesahihan Adalah Pilihan, Bukan Default
Tidak setiap analisis statis menargetkan kesahihan. Alat-alat seperti Coverity, CodeQL, dan Infer memprioritaskan menemukan bug nyata daripada membuktikan ketiadaannya. Mereka mengkurangi-aproksimasi ruang keadaan. Mereka mungkin melewatkan pembagian dengan nol, tetapi yang mereka temukan biasanya nyata.
Ini adalah pilihan rekayasa yang sah. Untuk aplikasi web, penemuan bug 90% akurat yang berjalan dalam hitungan menit mengalahkan analisis statis yang sahih yang menenggelamkan Anda dalam positif palsu. Untuk sistem kontrol penerbangan, sebaliknya yang benar. Anda ingin buktinya, meskipun Anda harus menyaring kebisingan.
Interpretasi abstrak adalah teknologi yang memungkinkan bukti tersebut. Ia bukan satu-satunya metode formal. Model checker seperti SPIN dan TLA+ memverifikasi mesin keadaan. Theorem prover seperti Coq dan Isabelle memverifikasi kebenaran fungsional. Interpretasi abstrak menempati titik manis: ia sepenuhnya otomatis, ia menskalakan ke codebases besar, dan memberikan jaminan matematis tentang perilaku waktu eksekusi.
Di Mana Interpretasi Abstrak Gagal
Metode ini memiliki batas keras. Ia tidak dapat bernalar tentang memori yang dialokasikan melalui aritmetika pointer yang kompleks. Ia tidak dapat memverifikasi bahwa algoritma Anda menghitung nilai yang benar, hanya bahwa ia tidak crash saat menghitungnya. Ia kesulitan dengan konkurensi, penyebaran dinamis, dan kode yang bergantung pada perilaku tak terdefinisi secara desain.
Ia juga mengharuskan kode ditulis dalam gaya yang dapat diverifikasi. Perangkat lunak penerbangan A380 menghindari rekursi, membatasi alokasi memori dinamis, dan menjaga aliran kontrol tetap sederhana. Pembatasan-pembatasan ini bukan keterbatasan analyzer. Mereka adalah prasyarat untuk bukti. Anda tidak dapat membuktikan properti dari kode yang terlalu kacau untuk dimodelkan.
Mulai dengan Interval pada Fungsi Nyata
Anda tidak memerlukan Astrée untuk menerapkan ide-ide ini. Pilih satu fungsi murni dalam codebase Anda. Identifikasi satu variabel yang harus tetap dalam batas. Tulis skrip propagasi interval sederhana. Lacak variabel tersebut melalui setiap cabang dan operasi.
Jika interval pada titik penggunaan berada di dalam rentang aman, Anda memiliki bukti manual keamanan untuk variabel tersebut. Jika tidak, Anda telah mengidentifikasi baik bug atau tempat di mana penalaran Anda tidak lengkap. Bagaimanapun, Anda mempelajari sesuatu yang mungkin tidak tertangkap oleh unit test.
Interpretasi abstrak tidak akan membuktikan bahwa pesawat Anda tidak akan jatuh. Tidak ada yang bisa. Tetapi ia dapat membuktikan bahwa perangkat lunak Anda tidak akan menjadi alasannya.
FAQ
Apa itu interpretasi abstrak?
Interpretasi abstrak adalah metode formal untuk analisis program statis di mana nilai program konkret digantikan oleh representasi abstrak, seperti interval atau bentuk. Analyzer mensimulasikan eksekusi program pada nilai-nilai abstrak ini. Jika kesalahan tidak terjangkau dalam domain abstrak, maka ia tidak terjangkau dalam program konkret untuk semua input yang mungkin.
Dapatkah interpretasi abstrak menemukan semua bug?
Tidak. Interpretasi abstrak membuktikan ketiadaan kesalahan waktu eksekusi spesifik, seperti pembagian dengan nol, buffer overflow, dan arithmetic overflow. Ia tidak dapat memverifikasi bahwa algoritma menghasilkan hasil yang benar, hanya bahwa ia tidak crash. Ia juga tidak dapat bernalar tentang properti di luar kode, seperti kegagalan perangkat keras atau perilaku sistem fisik.
Apa perbedaan antara analisis statis yang sahih dan tidak sahih?
Sebuah analisis statis yang sahih melebihi-aproksimasi himpunan perilaku program yang mungkin. Ia tidak akan pernah melewatkan bug dari jenis yang dirancang untuk dideteksi, tetapi ia mungkin melaporkan positif palsu. Sebuah analisis statis yang tidak sahih mengkurangi-aproksimasi. Ia mungkin melewatkan bug, tetapi yang dilaporkannya lebih mungkin nyata. Kesahihan sangat penting untuk sistem kritis untuk keselamatan. Analisis yang tidak sahih sering lebih disukai untuk umpan balik yang lebih cepat dalam pengembangan perangkat lunak umum.
Apakah interpretasi abstrak hanya untuk perangkat lunak kritis untuk keselamatan?
Tidak, meskipun di situlah ia paling banyak digunakan. Ide-ide di balik interpretasi abstrak muncul dalam banyak compiler dan optimizer. Analisis rentang LLVM, misalnya, menggunakan abstraksi interval untuk menghilangkan bounds check yang redundan. Anda dapat menerapkan penalaran interval yang sama ke kode apa pun di mana membuktikan batas penting, dari firmware embedded hingga kernel numerik berkinerja tinggi.