Ide & Wawasan

Mengeksplorasi pengembangan AI-first, coding guardrail, dan arsitektur untuk dibuang.

abstract-interpretationstatic-analysismetainfer

Meta Menemukan 100.000 Bug di Kode Produksi dengan Static Analyzer yang Tidak Pernah Menjalankan Program

Infer dari Meta menggunakan abstract interpretation dan bi-abduction untuk menemukan null dereference, memory leak, dan race condition dengan menalar struktur kode, bukan eksekusinya. Berikut cara kerjanya dan cara menggunakannya di codebase Anda sendiri.

Meta telah mengirimkan lebih dari 100.000 perbaikan bug yang tertangkap oleh static analyzer sebelum kode tersebut sampai ke pengguna. Tool tersebut bernama…
abstract-interpretationstatic-analysissafety-criticalaviation

Analisis Statis Tidak Bisa Membuktikan Pesawat Anda Tidak Akan Jatuh. Ia Bisa Membuktikan Sesuatu yang Lebih Berguna.

Interpretasi abstrak melebihi-aproksimasi setiap kemungkinan keadaan program. Jika pembagian dengan nol tidak terjangkau dalam abstraksi, maka ia tidak terjangkau dalam kode nyata. Berikut cara kerjanya dan di mana ia mengalami kegagalan.

Analisis statis tidak dapat membuktikan bahwa sebuah pesawat tidak akan jatuh. Ia dapat membuktikan bahwa loop kontrol altimeter Anda tidak akan pernah membagi…
abstract-interpretationstatic-analysisruntime-errorsverification

Cara membuktikan kode Anda bebas dari kesalahan runtime (dan mengapa Anda mungkin akan menyerah mencoba)

Interpretasi abstrak memungkinkan Anda membuktikan kesalahan runtime mustahil terjadi sebelum eksekusi. Berikut cara kerjanya secara nyata, mengapa hal itu sulit, dan di mana ia cocok dalam rantau alat Anda.

Test suite Anda lolos. Pemeriksa tipe Anda hijau. Anda rilis. Dua jam kemudian, produksi melemparkan pada kasus tepi yang tidak terpikirkan untuk diuji.…
hardware-assisted-safetycapability-hardwarecherisoftware-history

Hardware capability tidak gagal. Ia datang 40 tahun terlalu awal.

Keamanan memori di tingkat hardware telah mungkin sejak tahun 1970-an. Berikut mengapa arsitektur capability terus kalah dari model memori datar, dan mengapa CHERI akhirnya mengubah persamaan tersebut.

Tujuh puluh persen CVE adalah bug memory safety. Buffer overflow, use-after-free, double free. Jenis kerentanan yang memungkinkan penyerang berpindah dari JPEG…
hardware-assisted-safetysandboxingcwebassembly

Dependensi C Anda Bisa Membuat Seluruh Proses Crash. WebAssembly Bisa Mencegahnya.

Container terlalu berlebihan untuk mengisolasi satu library C. Kompilasi ke WebAssembly dan jalankan di dalam sandbox WASI untuk memory safety, akses filesystem berbasis capability, dan containment crash tanpa Docker.

Satu null pointer dereference di dalam library C bisa membuat seluruh aplikasi Anda crash. Jika library tersebut mem-parse input pengguna, melakukan dekompresi…
cleanroom-correctnessllmformal-proofsautomation

LLM Tidak Bisa Membuktikan Kode Anda Benar, Tapi Mereka Bisa Menulis Boilerplate yang Melakukannya

Verifikasi Cleanroom memerlukan pembuatan dan pelunasan kewajiban pembuktian. Berikut cara LLM mengotomatisasi anotasi dan pembuatan VC sehingga Anda bisa fokus pada pembuktian yang sebenarnya sulit.

Cleanroom software engineering menuntut agar Anda membuktikan kode Anda benar sebelum Anda mengompilasinya. Kedengarannya mulia sampai Anda menghabiskan tiga…
cleanroom-correctnessprocessefficiencypragmatism

Cleanroom Menghasilkan 0,1 Defect per KLOC. Anda Tidak Perlu Proses Lengkap untuk Sampai ke Sana.

Cleanroom software engineering memangkas defect rate 100×, tapi adopsi penuh memerlukan tim test terpisah dan proof formal. Berikut subset pragmatis yang menangkap sebagian besar manfaat tanpa overhead-nya.

Cleanroom software engineering menghasilkan 0,1 defect per seribu baris kode. Rata-rata industri adalah 10 sampai 50. Masalahnya, Cleanroom penuh mengharuskan…