- Bug pelepasan kunci sumber daya yang terlewat ditemukan dalam kode Apollo Guidance Computer(AGC) yang selama 57 tahun dianggap nyaris sempurna
- Tim JUXT menganalisis 130 ribu baris assembly menggunakan bahasa spesifikasi AI Allium dan Claude, lalu mengidentifikasi cacat yang tidak terlihat lewat metode verifikasi sebelumnya
- Pada jalur terminasi abnormal (BADEND) di rutinitas kontrol gyro, kunci
LGYRO tidak dilepas, sehingga seluruh fungsi terkait gyro setelahnya bisa berhenti
- Jika sakelar Cage sempat tertekan secara keliru saat misi nyata di orbit bulan, pekerjaan penyelarasan Program 52 bisa terhenti dan Collins mungkin mengiranya sebagai kerusakan perangkat keras
- Kasus ini menunjukkan bahwa analisis berbasis spesifikasi perilaku adalah metode yang ampuh untuk menemukan cacat baru bahkan pada kode lama
Cacat Potensial yang Ditemukan di Komputer Pemandu Apollo 11
- Apollo Guidance Computer(AGC) adalah salah satu codebase yang paling teliti ditinjau dalam sejarah, dan telah dianalisis oleh banyak pengembang serta peneliti
- Namun, bug kunci sumber daya yang tidak dilepas yang tak terdeteksi selama 57 tahun kini ditemukan di kode kontrol gyro
- Masalahnya adalah pada jalur error, kunci tidak dilepas sehingga fungsi penyelarasan ulang platform pemandu menjadi nonaktif
- Tim JUXT menggunakan bahasa spesifikasi berbasis AI Allium dan Claude untuk mengubah 130 ribu baris assembly AGC menjadi 12.500 baris spesifikasi perilaku
- Mereka mengekstrak spesifikasi langsung dari kode untuk memodelkan semua jalur akuisisi dan pelepasan sumber daya
- Dalam proses ini, muncullah cacat yang tidak terlihat lewat pembacaan kode atau emulasi biasa
Struktur Kode dan Pendekatan Analisis
- Kode sumber AGC dipublikasikan pada 2003 setelah Ron Burkey dan para relawan menyalin secara manual versi cetak dari MIT Instrumentation Laboratory
- Pada 2016, repositori GitHub milik Chris Garry dipublikasikan sehingga para pengembang di seluruh dunia dapat menelaah kode assembly dengan RAM 2KB dan CPU 1MHz
- Program disimpan dalam core rope memory berukuran 74KB, yang merepresentasikan 1 dan 0 dengan menenun kawat tembaga secara manual ke inti magnetik
- Para teknisi perempuan yang melakukan pekerjaan ini dijuluki “Little Old Ladies”, dan memorinya dinamai LOL memory
- Hingga kini, tidak ada catatan bahwa verifikasi formal, model checking, atau analisis statis pernah dilakukan terhadap AGC
- Sebagian besar verifikasi berfokus pada pembacaan kode, emulasi, dan pengecekan akurasi transkripsi
- JUXT menulis spesifikasi perilaku subsistem IMU(Inertial Measurement Unit) dalam Allium
- Dengan memodelkan waktu akuisisi dan pelepasan tiap sumber daya bersama, mereka berhasil mengidentifikasi cacat
Kunci yang Tidak Dilepas di Rutinitas Kontrol Gyro
- AGC mengelola IMU dengan kunci bersama bernama
LGYRO
- Saat memberi torsi pada gyroscope, sistem mengambil kunci tersebut dan melepaskannya setelah ketiga sumbu selesai
- Ini melindungi agar dua rutinitas tidak memanipulasi perangkat keras secara bersamaan
- Namun, pada jalur terminasi abnormal, kunci itu tidak dilepas
- Dalam terminasi normal, rutinitas
STRTGYR2 melepaskan LGYRO, tetapi ketika terjadi ‘Caging’ (kunci fisik untuk melindungi gyro), alur berpindah ke rutinitas BADEND
- Di
BADEND, dua instruksi CAF ZERO dan TS LGYRO (total 4 byte) tidak ada, sehingga kunci tetap tertahan
- Jika
LGYRO tidak dilepas, semua rutinitas torsi gyro berikutnya akan berhenti sambil menunggu kunci
- Penyelarasan halus, koreksi drift, torsi manual, dan seluruh fungsi terkait gyro akan terhenti
Dampak Potensial di Sisi Gelap Bulan
- Pada 21 Juli 1969, Michael Collins secara berkala menjalankan Program 52 (program penyelarasan pengamatan bintang) saat berada di orbit bulan
- Jika platform mengalami drift, ada risiko arah mesin pulang menjadi salah
- Jika sakelar Cage tanpa sengaja tertekan saat proses torsi berlangsung dan alur masuk ke
BADEND, LGYRO mungkin tidak akan dilepas sehingga semua P52 berikutnya bisa macet
- DSKY (display-keyboard) tetap menerima input tetapi tidak memberi respons
- Karena fungsi lain tetap berjalan normal, Collins bisa saja mengiranya sebagai kerusakan perangkat keras
- Jika restart (hard reset) dilakukan, masalah ini kemungkinan akan teratasi, tetapi pengalaman alarm 1202 saat pendaratan bulan mungkin membuat keputusan untuk segera melakukan reset tidak mudah
Desain Defensif Sistem Lama dan Keterbatasannya
- Tim MIT yang dipimpin Margaret Hamilton memperkenalkan konsep dasar rekayasa perangkat lunak modern seperti penjadwalan prioritas, multitasking asinkron, dan perlindungan restart
- Berkat desain ini, pendaratan tetap bisa dilakukan meski muncul alarm 1202
- Sebagian besar cacat besar merupakan kesalahan spesifikasi, dan seperti kasus yang didokumentasikan Don Eyles, pernah ada peningkatan beban CPU akibat sinkronisasi fase antaperangkat keras yang terlewat
- Cacat kali ini memiliki struktur serupa
BADEND adalah rutinitas terminasi umum untuk perpindahan mode IMU; ia melepaskan sumber daya umum seperti MODECADR, tetapi tidak menangani LGYRO- Karena logika restart menginisialisasi ulang
LGYRO, masalah ini pulih tanpa gejala saat pengujian sehingga cacatnya tetap tersembunyi
- Namun, dalam situasi nyata tanpa restart, gyro bisa tetap berada dalam keadaan terkunci secara permanen
Proses Penemuan Cacat dengan Allium
- Spesifikasi Allium memodelkan siklus hidup (lifecycle) tiap sumber daya
- Field
gyros_busy merepresentasikan LGYRO, aturan GyroTorque mendefinisikan pengambilan kunci, dan aturan GyroTorqueBusy mendefinisikan keadaan menunggu saat kunci sudah diambil
- Spesifikasi tersebut menyatakan kewajiban bahwa “jika kunci menjadi true, maka ia harus kembali menjadi false”
- Setelah Claude melacak semua jalur, ditemukan bahwa pada jalur normal (
STRTGYR2) kunci dilepas, tetapi pada jalur error (BADEND) hal itu terlewat
- Pendekatan berbasis spesifikasi memverifikasi bukan apa yang dilakukan kode, melainkan apa yang seharusnya dilakukan
- Pengujian memeriksa perilaku kode saat ini, sedangkan spesifikasi memverifikasi perilaku yang dimaksudkan
- Spesifikasi Allium dan kode reproduksi bug dipublikasikan di GitHub
Implikasi dan Pelajaran Modern
- Pada masa itu, programmer harus melepaskan kunci secara manual dengan instruksi
CAF ZERO dan TS LGYRO
- Mereka harus mengingat semua jalur dan menyisipkan kode pelepasan secara manual
- Bahasa modern mencegah masalah sumber daya yang terlewat seperti ini secara lebih struktural
defer di Go, try-with-resources di Java, with di Python, dan sistem ownership di Rust menjamin pelepasan otomatis
- Meski begitu, cacat tipe CWE-772 (Missing Release of Resource) masih tetap ada
- Koneksi database, kunci terdistribusi, file handle, dan urutan penghentian infrastruktur masih sering menjadi tanggung jawab programmer
- Semua misi Apollo berhasil kembali dengan selamat, tetapi cacat ini tetap ikut terbawa tanpa diperbaiki ke perangkat lunak COMANCHE(command module) dan LUMINARY(lunar module)
- Cacat yang tersembunyi selama 57 tahun ini menunjukkan pentingnya analisis berbasis spesifikasi perilaku
Belum ada komentar.