Praktik AWS dalam Menjaga Ketepatan Sistem
(cacm.acm.org)- Amazon Web Services (AWS) menempatkan ketepatan layanan sebagai nilai inti dan mengintegrasikan berbagai bentuk metodologi formal ke dalam proses pengembangan
- Melalui alat spesifikasi formal seperti TLA+ dan bahasa P, bug yang halus dapat ditemukan lebih dini, dan keandalan tetap terjaga bahkan saat melakukan optimasi yang berani
- AWS juga mengoperasikan metodologi formal ringan secara luas seperti pengujian berbasis properti, simulasi deterministik, dan fuzzing berkelanjutan
- Melalui alat injeksi kegagalan seperti Fault Injection Service, otomatisasi verifikasi keandalan mencakup bahkan situasi saat gangguan benar-benar terjadi
- Meski hambatan pembelajaran dan kompleksitas alat masih ada, penyebaran AI dan alat otomatisasi diperkirakan akan membantu adopsi yang lebih luas
Strategi AWS untuk Menjamin Ketepatan Sistem
Amazon Web Services (AWS) bertujuan menyediakan layanan yang sangat andal yang dapat dipercaya sepenuhnya oleh pelanggan.
Untuk itu, AWS berupaya mempertahankan standar keamanan, daya tahan, integritas, dan ketersediaan, dengan konsep ketepatan sistem ditempatkan di pusatnya.
Sejak contoh penerapan metodologi formal AWS diperkenalkan di Communications of the ACM pada 2015, pendekatan tersebut telah memainkan peran penting dalam pengoperasian sukses layanan-layanan inti.
Di pusat pendekatan ini ada TLA+, sebuah bahasa spesifikasi formal yang dikembangkan oleh Leslie Lamport.
Pengalaman AWS mengadopsi TLA+ memungkinkan mereka mengidentifikasi bug halus yang tidak tertangkap oleh pengujian konvensional pada tahap awal pengembangan.
Selain itu, bahkan saat melakukan optimasi performa yang agresif, verifikasi formal memungkinkan stabilitas dan keandalan tetap terjaga.
Lima belas tahun lalu, AWS masih berada pada tingkat dasar seperti unit test saat build dan integration test yang terbatas, tetapi kemudian mereka mengadopsi pendekatan formal dan metode semi-formal secara menyeluruh.
Perubahan ini berkontribusi bukan hanya pada ketepatan, tetapi juga pada verifikasi optimasi tingkat tinggi dan rendah, peningkatan kecepatan pengembangan, serta pengurangan biaya.
Di AWS, selain pembuktian formal dan model checking yang konvensional, hal-hal seperti pengujian berbasis properti, fuzzing, dan pemantauan runtime juga diterima sebagai bagian dari metodologi formal.
Munculnya Bahasa Pemrograman P
Pada awalnya, TLA+ memiliki keunggulan sebagai deskripsi abstrak yang kuat, tetapi bagi banyak pengembang, hambatan masuk karena penggunaan notasi matematis cukup besar.
Karena itu, AWS memperkenalkan bahasa P, yang menyediakan pendekatan berbasis state machine yang lebih akrab bagi pengembang.
Bahasa P menyediakan pendekatan pemodelan state machine untuk desain dan analisis sistem terdistribusi.
Ini merupakan konsep yang familier bagi pengembang Amazon yang menggunakan arsitektur SOA berbasis microservices.
Sejak 2019, bahasa ini dikembangkan di AWS dan dikelola sebagai proyek open source strategis.
Tim layanan utama seperti Amazon S3, EBS, DynamoDB, Aurora, EC2, dan IoT menggunakan P untuk memverifikasi ketepatan desain sistem.
Saat mengubah S3 ke konsistensi read-after-write yang kuat, AWS memodelkan dan memverifikasi protokolnya dengan P, sehingga bug dapat dihilangkan pada tahap awal desain dan optimasi juga dapat diterapkan secara aman.
Pada 2023, tim AWS P mengembangkan alat PObserve, yang memungkinkan verifikasi ketepatan sistem terdistribusi baik di lingkungan pengujian maupun operasi nyata.
PObserve mengekstrak log eksekusi sehingga validasi pasca-eksekusi dapat dilakukan untuk memastikan apakah perilaku berjalan sesuai spesifikasi, sekaligus menghubungkan spesifikasi tahap desain dengan implementasi kode nyata secara efektif.
Perluasan Metodologi Formal Ringan
Pengujian Berbasis Properti
Teknik formal ringan yang paling representatif adalah pengujian berbasis properti.
Sebagai contoh, tim pengembang ShardStore di S3 menggabungkan pengujian berbasis properti, fuzzing berbasis code coverage, injeksi kegagalan, dan minimalisasi counterexample di seluruh siklus pengembangan.
Pendekatan ini terhubung dengan spesifikasi ketepatan yang ditulis langsung oleh pengembang, dan juga sangat meningkatkan efisiensi debugging masalah.
Simulasi Deterministik
Pengujian simulasi deterministik menjalankan sistem terdistribusi di simulator single-thread, sehingga semua elemen acak seperti scheduling, timing, dan urutan pesan dapat dikendalikan.
Teknik ini diterapkan dalam berbagai cara, termasuk pengujian skenario kegagalan dan keberhasilan tertentu, pengaturan urutan pemicu bug, serta perluasan fuzzing.
Dengan demikian, verifikasi perilaku seperti latensi dan kegagalan sistem dapat dilakukan lebih awal pada tahap build, dan cakupan pengujian pun meluas.
AWS membuka kode pengujian build-time ini melalui proyek open source shuttle dan turmoil.
Fuzzing Berkelanjutan
Fuzzing berkelanjutan, khususnya pembuatan input skala besar berbasis code coverage, efektif untuk memverifikasi ketepatan sistem pada tahap integration test.
Sebagai contoh, saat mengembangkan Aurora Limitless Database, AWS melakukan fuzzing terhadap query SQL dan transaksi untuk memverifikasi ketepatan logika partisi dengan menghasilkan skema, dataset, dan query acak dalam jumlah besar.
Hasilnya dibandingkan dengan perilaku engine non-sharded atau pendekatan seperti SQLancer.
Dengan menggabungkan fuzzing dan injeksi kegagalan, properti inti basis data seperti atomisitas, konsistensi, dan isolasi dapat diverifikasi.
Beberapa properti seperti transaksi yang dibuat otomatis dan isolasi dijamin melalui validasi pasca-eksekusi berbasis riwayat eksekusi.
Injeksi Gangguan melalui Fault Injection Service
Pada 2021, AWS meluncurkan Fault Injection Service (FIS), yang memungkinkan pelanggan dengan cepat menguji berbagai skenario cacat seperti error API, gangguan I/O, dan kegagalan instance di lingkungan nyata maupun pengujian.
Melalui ini, mereka dapat membantu menjamin ketersediaan arsitektur, memeriksa ketahanan pemulihan dari gangguan, mengatasi perbedaan tingginya kepadatan bug dalam kasus error, dan menemukan lebih awal masalah serius yang berpotensi terjadi.
FIS digunakan secara luas tidak hanya oleh pelanggan AWS tetapi juga di internal Amazon; misalnya, sebanyak 733 eksperimen dilakukan hanya dalam proses persiapan Prime Day.
Injeksi error menjadi lebih efektif bila digabungkan dengan spesifikasi formal.
Setelah perilaku yang diharapkan ditulis sebagai spesifikasi formal, hasil dari cacat yang benar-benar dipicu dapat dibandingkan dengannya, sehingga lebih banyak error dapat ditemukan dibanding sekadar memeriksa log atau metrik sederhana.
Metastabilitas dan Perilaku Emergen Sistem
Dalam sistem terdistribusi, semakin banyak kasus di mana beban berlebih atau habisnya cache memicu kondisi abnormal (metastabil) yang tidak dapat pulih sendiri.
Dalam keadaan ini, sistem tidak kembali normal hanya dengan mengurangi beban, sehingga penanganannya lebih sulit daripada kasus error biasa.
Sebagian besar logika retry-timeout juga menjadi penyebab fenomena semacam ini.
Spesifikasi formal yang ada biasanya berfokus pada safety dan liveness, tetapi metastabilitas mengharuskan perhatian juga pada berbagai perilaku emergen lainnya.
Berdasarkan model spesifikasi seperti TLA+ dan P, AWS menjalankan simulasi kejadian diskret untuk menganalisis secara sistematis bahkan karakteristik probabilistik seperti kemungkinan tercapainya SLA performa dan distribusi latensi.
Kebutuhan akan Pembuktian Formal
Pada beberapa batas keamanan (otorisasi, virtualisasi, dan sebagainya), pembuktian pada tingkat matematis menjadi penting, melampaui pengujian biasa.
Sebagai contoh, bahasa kebijakan otorisasi Cedar yang diperkenalkan AWS pada 2023 dioptimalkan untuk pembuktian otomatis dan verifikasi formal berbasis Dafny, dan melalui kode terbuka serta prosedur koreksi, seluruh pengguna juga dapat memverifikasinya secara langsung.
Selain itu, key property dari batas keamanan Firecracker VMM dibuktikan menggunakan alat analisis kode Rust seperti Kani.
Dengan memanfaatkan model dan spesifikasi formal secara luas pada berbagai tahap—desain, implementasi, eksekusi, dan pembuktian—AWS menggunakannya untuk memastikan ketepatan perangkat lunak sekaligus memperluas nilai bagi perusahaan dan pelanggan.
Dampak Tambahan di Luar Ketepatan
Metodologi formal memainkan peran penting baik dalam keandalan maupun peningkatan performa.
Sebagai contoh, protokol commit Aurora diverifikasi dengan P dan TLA+, sehingga round-trip jaringan dapat dikurangi sekaligus tetap menjamin safety.
Saat mengoptimalkan algoritme enkripsi RSA untuk ARM Graviton 2, AWS membuktikan ketepatan matematis transformasinya di HOL Light, dan memperoleh manfaat nyata berupa peningkatan performa sekaligus penurunan biaya infrastruktur.
Tantangan dan Peluang di Masa Depan
Selama 15 tahun, AWS telah sangat memperluas penerapan industri metodologi formal dan semi-formal, tetapi masalah hambatan adopsi yang nyata seperti learning curve, kebutuhan akan pakar, dan sifat alat yang akademis masih tetap ada.
Pengujian berbasis properti dan simulasi deterministik pun masih terasa asing bagi banyak pengembang.
Karena hambatan pendidikan sudah ada sejak tingkat sarjana, penyebaran alat dan metodologi serta penerapan praktisnya berjalan lambat.
Karakteristik emergen sistem skala besar seperti metastabilitas juga masih berada pada tahap awal penelitian.
Ke depannya, AI/model bahasa besar diharapkan dapat membantu penulisan model dan spesifikasi formal, sehingga aksesibilitas bagi praktisi dapat meningkat secara drastis dalam waktu singkat.
Kesimpulan
Untuk membangun perangkat lunak yang kokoh dan aman, diperlukan beragam cara untuk menjamin ketepatan sistem.
AWS mengadopsi secara komprehensif bukan hanya teknik pengujian standar, tetapi juga model checking, fuzzing, pengujian berbasis properti, pengujian injeksi gangguan, simulasi deterministik/berbasis kejadian, dan verifikasi riwayat eksekusi.
Spesifikasi dan metodologi formal berperan sebagai test oracle penting dalam proses pengembangan AWS, dan melalui pembuktian efek praktis serta ekonominya, kini telah menjadi salah satu area investasi penting.
1 komentar
Opini Hacker News
Ingin membahas pendekatan pengujian simulasi deterministik. Di AWS, sistem terdistribusi dijalankan di simulator single-thread sambil mengendalikan semua elemen non-deterministik seperti penjadwalan thread, timing, dan urutan pengiriman pesan. Lalu mereka menulis pengujian yang disesuaikan untuk skenario kegagalan atau keberhasilan tertentu, dan non-determinisme dalam sistem dikendalikan oleh framework pengujian. Developer bisa menentukan urutan spesifik yang dulu pernah memicu bug. Scheduler juga bisa diperluas ke fuzzing urutan atau bahkan menelusuri semua urutan yang mungkin. Saya penasaran apakah ada library open source yang mengimplementasikan hal seperti ini secara agnostik terhadap bahasa. Idenya adalah perlu ada alat middleware yang bisa membuat hal-hal seperti networking dan storage di dalam container juga menjadi "deterministik" saat pengujian. antithesis hampir melakukan hal ini, tapi saya belum melihat versi open source-nya. Jika pengujian ditulis dengan baik, sebagian ini bisa diatasi dengan men-stub hal seperti I/O, tetapi tidak ada jaminan semua orang menulis pengujian dengan baik. Menurut saya akan bagus jika determinisme disediakan pada lapisan yang lebih tinggi di atas aplikasi. Di sisi lain, saya berharap AI bisa benar-benar bersinar dalam pengujian. Prompt (requirements)-implementasi pengujian-AI-kode eksekusi, ketiga sumbu ini bisa saling terkait dengan ideal. Ada harapan AI bisa mempermudah verifikasi formal sehingga dunia perangkat lunak menjadi lebih ketat dan rigor
Ada dua kesulitan dalam penyebaran teknik deterministic simulation testing (DST). Pertama, selama ini seluruh sistem harus langsung dibangun di atas framework simulasi tertentu tanpa dependensi lain. Kedua, jika pembuatan dan eksplorasi input lemah, semua pengujian bisa tampak sukses padahal verifikasi nyatanya tidak berarti. antithesis berusaha menyelesaikan keduanya, tetapi masih banyak tantangannya. Hampir tidak ada yang punya cara pasti untuk menerapkan determinisme ke sembarang software. Proyek Hermit milik Facebook juga pernah mencoba lewat deterministic Linux userspace, tetapi akhirnya dihentikan. Komputer deterministik adalah fondasi teknis yang sangat berguna bukan hanya untuk pengujian, dan saya pikir suatu hari seseorang akan merilisnya sebagai open source
Menurut saya, mendapatkan mesin deterministik dengan menjalankan QEMU dalam mode emulasi 100% secara single-thread relatif mudah. Tetapi yang benar-benar diinginkan adalah eksekusi deterministik yang 'terkendali', dan ini jauh lebih sulit. Jika ingin membuat banyak proses berjalan sesuai skenario yang ditentukan, tingkat kesulitannya sangat tinggi terutama di level CPU dan scheduler OS. Sulit juga membangun lingkungan yang benar-benar agnostik terhadap bahasa, dan mudah terseret detail-detail kecil. Saya sendiri pernah membuat sistem sederhana yang menjalankan beberapa thread JVM dalam lockstep pada titik perilaku tertentu, sambil menangani I/O dan system time dengan stub dan kontrol. Dengan begitu saya bisa menguji berbagai interaksi antar komponen asinkron, gangguan I/O, retry, dan menangkap bug menyebalkan sebelum masuk produksi. Namun ini dimungkinkan dengan menyederhanakan hanya titik sinkronisasi tertentu, bukan dengan mengendalikan seluruh sistem. Data race umum akibat kesalahan sinkronisasi sulit ditangkap dengan pendekatan ini
Berbagi dokumen resmi metode pengujian FoundationDB dan video presentasi YouTube
Jika bahasanya bisa di-debug dengan gdb, saya merekomendasikan proyek https://rr-project.org/
Saya ingat pernah melihat presentasi Joe Armstrong tentang menguji Dropbox dengan property testing
Menurut saya S3 adalah salah satu software paling keren yang pernah saya lihat. Beberapa tahun lalu mereka juga menambahkan strong read-after-write consistency ke seluruh sistem S3, dan itu benar-benar puncak software engineering tautan blog post
Saya pernah bekerja langsung menangani lifecycle S3, dan saat itu bertepatan dengan masa tim indeks sedang merancang ulang struktur untuk menyediakan konsistensi tersebut. Dari luar saja S3 sudah luar biasa, tetapi secara internal baik implementasi maupun struktur organisasinya jauh melampaui apa yang bisa dibayangkan
Google Cloud Storage justru sudah punya fitur ini (strong consistency) jauh lebih lama daripada S3. Secara keseluruhan, kesannya GCS adalah produk yang lebih sistematis dan lebih rapi dibangun
Saya setuju dengan angka 92% (sebagian besar kegagalan cluster dimulai dari kegagalan kecil). Bukan insiden besar yang dramatis, melainkan retry "sepele" yang menumpuk sebagai state hingga akhirnya meledak jadi outage besar pukul 2 pagi. Penting untuk mengalokasikan lebih banyak waktu engineering ke kegagalan yang tidak mencolok
Menurut saya ini artikel yang sangat menarik. Penggunaan state machine dalam membangun control plane infrastruktur itu wajib. Saya tidak yakin apakah P memang diperlukan. Kami juga membangun control plane infrastruktur dengan Ruby selama lebih dari 13 tahun, dan hasilnya bekerja sangat baik blog berbagi pengalaman terkait
Saya sempat penasaran soal bahasa P. Dulu sepertinya di Microsoft mereka menghasilkan kode C dari P untuk runtime stack USB Windows dan benar-benar memakainya, tetapi sekarang tampaknya tidak lagi digunakan untuk menghasilkan kode operasional. Saya juga pernah meninggalkan pertanyaan terkait ini di Hacker News tautan pertanyaan. Jika kode hasil generate bisa masuk sampai ke kernel, seharusnya ia juga bisa dipakai di lingkungan cloud yang kondisinya jauh lebih longgar
Dari sudut pandang orang yang bukan alumni AWS dan tidak akrab dengan TLA+ atau P, sepertinya akan jauh lebih mudah dipahami kalau ada contoh setingkat "hello world". Dari tulisannya saja, prosesnya malah terasa menyakitkan, dan timbul kesan apakah ini bukan masalah yang cukup bisa ditangkap hanya dengan desain dan pengujian yang baik. Kalau ada contoh sederhana, akan lebih membantu menilai apa yang sebenarnya dilakukan
Ada contoh demo cepat TLA+ yang saya suka tautan gist. Ini memodelkan beberapa thread yang menaikkan counter bersama secara tidak atomik, dan saat properti diverifikasi, race condition-nya tertangkap. Dalam praktiknya, sangat sulit menemukan bug seperti ini hanya dengan pengujian. Sebagian besar spesifikasi TLA+ jauh lebih kompleks, tetapi contoh ini bagus untuk menangkap kesalahan sederhana
Saya pernah mencoba memakai TLA sendiri, tetapi kecewa karena alat grafisnya tidak cocok dengan tutorial. Sebenarnya saya ingin memakai TLA, dan sejak lama saya menyukai karya Lamport (bahkan sampai paper LaTeX)
Premis penggunaan formal methods pada akhirnya adalah bahwa pengujian saja tidak akan pernah bisa menangkap semua masalah
Merekomendasikan repositori GitHub resmi TLA+ Examples. Disarankan mulai dari hal sederhana seperti masalah DieHard
Pengujian membuktikan kebenaran implementasi terhadap instans tertentu dari suatu masalah, sedangkan verifikasi formal membuktikannya untuk seluruh kelas kasus. Misalnya untuk fungsi yang mengembalikan anagram, pengujian hanya memeriksa beberapa pasangan kata, tetapi untuk membuktikan kebenarannya terhadap semua pasangan kata diperlukan formal verification. Kasus seperti undefined behavior atau bug library juga sering kali hanya tertangkap lewat proses formal verification
Soal penyebutan "teknik ringan semi-formal seperti property-based testing, fuzzing, dan runtime monitoring", saya merasa property-based testing dan fuzzing memang merupakan subset dari formal methods, tetapi memasukkan runtime monitoring sebagai teknik semi-formal agak berlebihan
Dulu saya pernah berinteraksi dengan Leslie Lamport, termasuk lewat paper tentang Buridan's Principle. Hari ini saya jadi banyak belajar soal TLA+ dan PlusCal dari homepage-nya halaman contoh Peterson. Sangat masuk akal bahwa orang yang membawa matematika ke pemrograman, menjadi salah satu pelopor bidang sistem konkuren, lalu membuat bahasa desain sistem (TLA+), juga dipakai di AWS dan tempat lain. Saya berharap lebih banyak orang yang membangun sistem terdistribusi memakai hasil karya Lamport. Pada sistem skala besar, pembuktian kebenaran sangat penting
Untuk mengubah kode yang sudah ada menjadi spesifikasi TLA+, Claude Opus (Extended Thinking) sangat berguna. Saya pernah menemukan beberapa bug saat memverifikasi proyek Rust maupun komponen inti C++ dengannya. Model lain sering tersendat di sintaks dan logika spesifikasi, sementara Opus bekerja jauh lebih mulus
Bukan hanya sistem skala besar, utilitas kecil tetapi penting seperti SSH dan terminal juga sangat diuntungkan oleh pembuktian kebenaran
Menanggapi pernyataan "membuktikan kebenaran sistem", pada praktiknya mustahil membuktikan semuanya. Model checker hanya bisa memberi tahu bahwa spesifikasi yang ditulis memenuhi properti dalam ruang keadaan yang terbatas
Secara pribadi saya penasaran apakah ada yang pernah memakai FIS untuk eksperimen layanan terdistribusi. Saya sedang mempertimbangkan adopsinya, tetapi belum punya pengalaman langsung menjalankan eksperimen skala besar
Saya penasaran apakah Promela dan SPIN adalah bahasa tingkat lebih tinggi daripada yang dibahas dalam artikel