Praktik AWS dalam Menjaga Kebenaran Sistem

• AWS menjadikan kebenaran sistem sebagai fondasi utama untuk menjaga keamanan, daya tahan, integritas, dan ketersediaan, serta telah memperluas penerapannya dari TLA+ ke model checking, fuzzing, property-based testing, verifikasi runtime, hingga pembuktian formal
• TLA+ membantu menghilangkan bug sejak awal yang sulit ditangkap dengan pengujian tradisional dan memberi keyakinan pada optimisasi performa, tetapi untuk meningkatkan aksesibilitas bagi pengembang, alat seperti bahasa pemrograman P dan PObserve juga diperkenalkan
• Property-based testing pada S3 ShardStore, simulasi deterministik, dan SQL fuzzing pada Aurora Limitless Database adalah contoh yang membawa teknik formal lebih dekat ke pengembangan sehari-hari dan pengujian integrasi
• Fault Injection Service memverifikasi mekanisme ketahanan dengan menyuntikkan gangguan seperti error API, jeda I/O, dan kegagalan instance; Amazon.com menjalankan 733 eksperimen berbasis FIS dalam persiapan Prime Day 2024
• Di area yang sangat penting bagi batas keamanan dan optimisasi performa seperti Cedar, Firecracker, dan optimisasi RSA Graviton 2, pembuktian formal digunakan, tetapi kurva pembelajaran yang curam dan aksesibilitas alat masih menjadi hambatan adopsi

---

Cara AWS menangani kebenaran sistem

• AWS harus mempertahankan standar tinggi keamanan, daya tahan, integritas, dan ketersediaan agar dapat menyediakan layanan yang dipercaya pelanggan, dan kebenaran sistem menjadi penopangnya
• Artikel CACM tahun 2015, “How Amazon Web Services Uses Formal Methods”, memperkenalkan pendekatan untuk menjamin kebenaran layanan inti AWS, dan sejak itu layanan-layanan tersebut digunakan secara luas oleh pelanggan AWS
• Alat utama pada fase awal adalah bahasa spesifikasi formal TLA+ yang dikembangkan oleh Leslie Lamport
  • Membantu menemukan dan menghilangkan bug halus pada tahap awal pengembangan yang dapat terlewat oleh pengujian tradisional
  • Memberikan keyakinan bahwa optimisasi performa yang agresif dapat diterapkan tanpa mengorbankan kebenaran sistem
• Lima belas tahun lalu, praktik pengujian AWS terutama bergantung pada unit test saat build dan integration test terbatas saat deployment
• Setelah itu, AWS mengintegrasikan teknik formal dan semi-formal ke dalam proses pengembangan
  • Pembuktian teorema, verifikasi deduktif, model checking
  • Property-based testing, fuzzing, runtime monitoring

Bahasa pemrograman P dan PObserve

• Saat AWS memperluas teknik formal ke luar tim awal pada awal 2010-an, mereka menemukan bahwa banyak engineer mengalami kesulitan dalam mempelajari TLA+ dan menjadi produktif dengannya
• TLA+ kuat karena merupakan bahasa abstraksi tingkat tinggi yang dekat dengan matematika, tetapi hal ini juga menjadi hambatan bagi pengembang yang terbiasa dengan bahasa imperatif
• P, bahasa berbasis state machine untuk pemodelan dan analisis sistem terdistribusi, hadir untuk menjembatani kesenjangan ini
  • Pengembang memodelkan desain sistem sebagai state machine yang saling berkomunikasi
  • Model mental ini akrab bagi pengembang Amazon yang banyak bekerja dengan microservices dan service-oriented architecture (SOA)
  • P dikembangkan di AWS sejak 2019 dan dipelihara sebagai proyek open source strategis
• Beberapa tim produk utama AWS menggunakan P untuk meninjau kebenaran desain sistem
  • Storage: Amazon S3, EBS
  • Database: Amazon DynamoDB, MemoryDB, Aurora
  • Compute: EC2, IoT
• S3 menggunakan P dalam proses transisi dari eventual consistency ke strong read-after-write consistency
  • Subsistem indeks S3 adalah penyimpanan metadata objek yang memungkinkan pengambilan data cepat
  • Untuk mencapai konsistensi kuat, diperlukan sejumlah perubahan yang tidak sepele pada stack protokol indeks S3
  • P memungkinkan desain protokol dimodelkan dan diverifikasi secara formal untuk menghilangkan bug tingkat desain sejak awal, serta memeriksa optimisasi berisiko melalui model checking
• Pada 2023, tim P AWS membangun PObserve
  • Menggunakan log terstruktur dari eksekusi sistem terdistribusi
  • Memverifikasi setelah kejadian apakah log tersebut sesuai dengan perilaku yang diizinkan oleh spesifikasi formal P dari sistem
  • Menjembatani kesenjangan antara implementasi produksi yang ditulis dalam bahasa seperti Rust atau Java dan spesifikasi P pada tahap desain
  • Menghubungkan verifikasi saat desain dengan runtime monitoring implementasi, sehingga meningkatkan nilai investasi pada spesifikasi formal

Menempelkan teknik formal ringan ke alur pengembangan

• AWS mengadopsi teknik formal ringan agar teknik formal lebih dekat dengan alur pengembangan dan pengujian tim engineering

• Property-based testing

  • ShardStore di Amazon S3 menggunakan property-based testing sepanjang siklus pengembangan untuk pengujian kebenaran dan peningkatan kecepatan pengembangan
  • Berbagai teknik digunakan bersama agar manusia dapat menspesifikasikan perilaku yang diharapkan, sementara pengujian otomatis menjelajahi lebih banyak input dan kondisi kegagalan
    • Spesifikasi kebenaran yang disediakan pengembang
    • Coverage-guided fuzzing yang mengarahkan distribusi input dengan metrik code coverage
    • Fault injection yang mensimulasikan kegagalan hardware dan sistem lain selama pengujian
    • Minimization yang otomatis menyederhanakan counterexample agar lebih mudah di-debug oleh manusia

• Simulasi deterministik

  • Pengujian simulasi deterministik menjalankan sistem terdistribusi dalam simulator single-thread dan mengendalikan semua sumber keacakan
    • Penjadwalan thread
    • Timing
    • Urutan pengiriman pesan
  • Pengembang dapat menulis skenario kegagalan atau keberhasilan tertentu, misalnya ketika peserta gagal pada tahap tertentu dari protokol terdistribusi
  • Karena framework pengujian mengendalikan nondeterminisme, urutan eksekusi yang menarik—seperti urutan yang pernah memicu bug di masa lalu—dapat ditentukan secara eksplisit
  • Scheduler dapat diperluas menjadi fuzzing urutan atau eksplorasi semua urutan yang mungkin
  • Dengan ini, pengujian properti sistem pada kondisi latensi dan kegagalan dapat dipindahkan lebih dekat ke waktu build daripada integration test, mempercepat pengembangan dan memperluas cakupan perilaku
  • Sebagian pekerjaan AWS untuk pengujian urutan thread dan kegagalan sistem pada waktu build telah di-open-source-kan melalui proyek shuttle dan turmoil

• Fuzzing berkelanjutan dan pembuatan input uji acak

  • Fuzzing berkelanjutan, khususnya pembuatan input uji yang skalabel berbasis panduan coverage, efektif untuk pengujian kebenaran sistem pada tahap integrasi
  • Dalam pengembangan Aurora Limitless Database, fitur data sharding Amazon Aurora, fuzzing digunakan secara luas untuk memverifikasi dua properti utama
  • Query SQL dan seluruh transaksi di-fuzz untuk memverifikasi bahwa pemisahan logika eksekusi SQL lintas shard dilakukan dengan benar
  • Sejumlah besar skema SQL, dataset, dan query acak disintesis lalu dijalankan pada engine yang diuji, dan hasilnya dibandingkan dengan oracle berbasis engine non-sharded
  • Metode verifikasi lain, seperti pendekatan yang dipelopori SQLancer, juga digunakan bersama
  • Kombinasi fuzzing dan fault injection testing juga berguna untuk aspek kebenaran database seperti atomisitas, konsistensi, dan isolasi
    • Menghasilkan transaksi secara otomatis
    • Mendefinisikan perilaku yang benar melalui oracle kebenaran yang dispesifikasikan secara formal
    • Menjalankan kemungkinan interleaving antartransaksi dan pernyataan di dalam transaksi pada sistem yang diuji
    • Memverifikasi setelah kejadian properti seperti isolasi, mengikuti pendekatan seperti Elle

Fault Injection Service dan verifikasi kondisi kegagalan

• AWS merilis Fault Injection Service(FIS) pada awal 2021 agar pengujian berbasis fault injection dapat digunakan oleh berbagai pelanggan AWS
• FIS dapat menyuntikkan gangguan simulasi ke deployment pengujian atau produksi di infrastruktur AWS
  • Error API
  • Jeda I/O
  • Instance gagal
• Fault injection membantu memastikan bahwa mekanisme ketahanan yang dibangun ke dalam arsitektur benar-benar meningkatkan ketersediaan dan tidak menciptakan masalah kebenaran baru
  • Failover
  • Health check
• Pengujian fault injection berbasis FIS digunakan secara luas oleh pelanggan AWS maupun di internal Amazon
• Amazon.com menjalankan 733 eksperimen fault injection berbasis FIS dalam persiapan Prime Day 2024
• Pada 2014, Yuan dkk. menganalisis bahwa 92% kegagalan fatal pada sistem terdistribusi yang mereka uji dipicu oleh penanganan yang salah atas error yang sebenarnya tidak fatal
• Kegagalan fatal pada jalur normal jarang terjadi karena jalur normal lebih sering dieksekusi, lebih banyak diuji, dan jauh lebih sederhana dibanding jalur error
• Fault injection testing dan FIS memudahkan pengujian perilaku sistem saat gangguan dan kegagalan, sehingga mengurangi kesenjangan kepadatan bug antara jalur normal dan jalur error
• Fault injection sendiri tidak dianggap sebagai teknik formal, tetapi dapat dikombinasikan dengan spesifikasi formal
  • Perilaku yang diharapkan didefinisikan dengan spesifikasi formal
  • Hasil selama dan setelah fault injection dibandingkan dengan perilaku yang dispesifikasikan
  • Ini dapat menangkap lebih banyak bug dibanding hanya memeriksa metrik dan error log atau mengandalkan penilaian visual manusia

Metastabilitas dan perilaku sistem yang emergen

• Dalam 10 tahun terakhir, perhatian terhadap kelas kegagalan sistem tertentu, yaitu kegagalan metastabil (metastable failures), meningkat
• Kegagalan metastabil adalah kegagalan ketika pemicu seperti overload atau pengosongan cache mendorong sistem terdistribusi ke keadaan yang tidak dapat pulih tanpa intervensi
  • Contoh intervensi adalah menurunkan beban ke tingkat yang lebih rendah dari normal
• Kelas kegagalan ini merupakan salah satu faktor penting penyebab ketidaktersediaan pada sistem cloud
• Pada perilaku metastabil yang umum, seiring beban meningkat, goodput mula-mula naik, lalu jenuh, melewati kemacetan, dan akhirnya turun ke 0 atau mendekati 0
• Setelah itu, sistem tidak dapat kembali ke keadaan sehat hanya dengan sedikit mengurangi beban; pemulihan memerlukan pengurangan beban yang signifikan
• Perilaku ini dapat muncul bahkan pada sistem sederhana, dan pada banyak sistem dapat dipicu hanya oleh logika klien retry setelah timeout
• Pemodelan formal sistem terdistribusi tradisional biasanya berfokus pada safety dan liveness, tetapi kegagalan metastabil menunjukkan adanya perilaku yang tidak masuk rapi ke dalam klasifikasi ini
• AWS semakin banyak memanfaatkan simulasi kejadian diskret untuk memahami perilaku sistem yang emergen
  • Berinvestasi pada simulasi sistem kustom
  • Berinvestasi pada alat yang dapat menggunakan model sistem yang sudah ada, dibuat dengan bahasa seperti TLA+ dan P, untuk simulasi
• Jika model checker eksplorasi menyeluruh seperti TLC pada TLA+ diperluas dengan simulasi probabilistik, hasil statistik seperti distribusi tail latency dapat dihasilkan
• Perluasan semacam itu memungkinkan model checking digunakan untuk memahami hal-hal seperti kemungkinan pencapaian SLA latensi

Batas keamanan yang memerlukan pembuktian formal

• Pada batas keamanan penting seperti otorisasi dan virtualisasi, teknik formal yang dibahas sebelumnya mungkin tidak cukup, dan pembuktian kebenaran layak mendapat investasi besar

• Bahasa kebijakan otorisasi Cedar

  • AWS memperkenalkan bahasa kebijakan otorisasi Cedar pada 2023 untuk menulis kebijakan yang menentukan izin secara rinci
  • Cedar dirancang dengan mempertimbangkan penalaran otomatis dan pembuktian formal
  • Implementasinya dibangun dengan bahasa pemrograman ramah verifikasi Dafny
  • Melalui Dafny, dibuktikan bahwa implementasinya memenuhi sejumlah properti keamanan
  • Pembuktian ini adalah bukti dalam makna matematis, melampaui pengujian
  • Tim juga menerapkan differential testing dengan menggunakan kode Dafny sebagai oracle kebenaran untuk memverifikasi implementasi Rust yang siap produksi
  • Bersama implementasi Cedar, AWS juga meng-open-source-kan kode Dafny dan prosedur pengujiannya agar pengguna dapat memeriksa pekerjaan kebenaran tersebut

• Firecracker VMM

  • Monitor mesin virtual Firecracker menggunakan protokol tingkat rendah bernama virtio untuk mengekspos perangkat keras emulasi seperti kartu jaringan atau SSD ke guest kernel di dalam VM
  • Perangkat emulasi ini adalah interaksi paling kompleks antara guest yang tidak tepercaya dan host yang tepercaya, sehingga menjadi batas keamanan yang penting
  • Tim Firecracker menggunakan Kani, yang memungkinkan penalaran formal atas kode Rust, untuk membuktikan properti inti dari batas keamanan ini
  • Pembuktian ini menjamin bahwa apa pun yang dicoba guest, properti penting dari batas tersebut tetap terjaga
  • AWS mendukung pengembangan alat dasar seperti Kani, Dafny, Lean, serta SMT solver yang menggerakkannya
  • Model formal dan spesifikasi digunakan kembali dalam berbagai cara
    • Model checking saat desain
    • Berperan sebagai oracle kebenaran dalam runtime monitoring
    • Simulasi perilaku sistem yang emergen
    • Membangun pembuktian properti inti

Di luar kebenaran: performa dan efisiensi biaya

• Teknik formal juga penting untuk meningkatkan performa sistem cloud secara aman
• Dengan memodelkan protokol commit inti pada engine database relasional Aurora menggunakan P dan TLA+, ditemukan peluang untuk menurunkan biaya distributed commit dari 2 network round trip menjadi 1,5 network round trip tanpa mengorbankan properti safety
• Hasil seperti ini umum terjadi pada tim yang mengadopsi teknik formal
  • Proses memikirkan protokol terdistribusi secara mendalam dan menuliskannya secara formal memaksa cara berpikir yang terstruktur
  • Memberikan wawasan yang lebih dalam tentang struktur protokol dan masalah yang harus dipecahkan
  • Jika optimisasi desain yang diusulkan dapat diverifikasi atau dibuktikan secara formal, engineer sistem terdistribusi bisa memilih desain yang lebih berani tanpa menambah risiko
• Produktivitas dan efisiensi biaya tidak terbatas pada optimisasi desain tingkat tinggi
• Tim AWS juga menemukan optimisasi untuk implementasi kriptografi kunci publik RSA pada prosesor berbasis ARM Graviton 2, yang meningkatkan throughput hingga 94%
• Mereka menggunakan interactive theorem prover HOL Light untuk membuktikan kebenaran optimisasi tersebut
• Karena porsi besar siklus CPU cloud digunakan untuk kriptografi, optimisasi semacam ini dapat berkontribusi pada pengurangan biaya infrastruktur, mendukung keberlanjutan, dan meningkatkan performa yang dirasakan pelanggan

Tantangan yang tersisa dan peluang ke depan

• AWS telah berhasil memperluas metode pengujian formal dan semi-formal selama 15 tahun terakhir, tetapi adopsi industri masih menghadapi tantangan
• Hambatan utama alat teknik formal adalah kurva pembelajaran yang curam dan kebutuhan akan pengetahuan domain yang khusus
• Banyak alat masih bersifat akademis dan kurang memiliki antarmuka yang ramah pengguna
• Bahkan pendekatan semi-formal yang sudah mapan pun masih menghadapi hambatan adopsi
  • Simulasi deterministik adalah teknik inti pengujian sistem terdistribusi yang telah berhasil digunakan di AWS dan proyek seperti FoundationDB, tetapi bahkan bagi pengembang sistem terdistribusi berpengalaman yang bergabung ke AWS, teknik ini kadang masih terasa asing
  • Kesenjangan serupa juga ada pada metodologi yang sudah terbukti seperti fault injection testing, property-based testing, dan fuzzing
• Pengembang sistem terdistribusi perlu diedukasi mengenai metode dan alat pengujian ini, serta diajarkan cara berpikir yang ketat
• Kesenjangan pendidikan dimulai bahkan di tingkat akademik
  • Pendekatan penalaran formal dasar pun jarang diajarkan
  • Lulusan institusi papan atas pun bisa kesulitan mengadopsi alat-alat ini
  • Teknik formal dan penalaran otomatis penting untuk penerapan industri, tetapi masih dianggap sebagai bidang niche
• Metastabilitas dan properti emergen lain pada sistem skala besar juga merupakan area riset penting dengan tantangan persepsi yang serupa
  • Praktik seperti “retry N kali saat timeout”, yang dapat memicu perilaku sistem metastabil, masih terus direkomendasikan secara luas meski merupakan masalah yang sudah diketahui
  • Alat dan teknik saat ini untuk memahami perilaku sistem emergen masih berada pada tahap awal
  • Pemodelan stabilitas sistem mahal dan kompleks
• AWS memandang model bahasa besar dan asisten AI akan sangat membantu meringankan masalah adopsi praktik teknik formal
  • Seperti bantuan AI untuk unit test yang telah populer, AI dapat membantu pengembang membuat model dan spesifikasi formal
  • Teknik tingkat lanjut bisa menjadi lebih mudah diakses oleh komunitas pengembang yang lebih luas

Kerangka kebenaran yang terus diinvestasikan AWS

• Untuk membangun perangkat lunak yang andal dan aman, diperlukan berbagai pendekatan untuk menalar kebenaran sistem
• AWS mengadopsi banyak teknik di samping pengujian standar industri seperti unit test dan integration test
  • Model checking
  • Fuzzing
  • Property-based testing
  • Fault injection testing
  • Simulasi deterministik
  • Simulasi berbasis kejadian
  • Verifikasi runtime atas execution trace
• Spesifikasi formal memainkan peran penting sebagai test oracle yang memberikan jawaban benar dalam berbagai praktik pengujian AWS
• Pengujian kebenaran dan teknik formal tetap menjadi area investasi inti AWS berdasarkan hasil investasi yang sudah mereka peroleh