Amazon Web Services’in sistem doğruluğu uygulamaları

• AWS, güvenlik, dayanıklılık, bütünlük ve kullanılabilirliği korumak için sistem doğruluğunu temel dayanak olarak görüyor; TLA+ ile başlayıp model checking, fuzzing, özellik tabanlı test, çalışma zamanı doğrulaması ve biçimsel kanıtlara kadar uygulama alanını genişletti
• TLA+, geleneksel testlerle yakalanması zor hataları erken aşamada ortadan kaldırıp performans optimizasyonları konusunda güven sağladı; ancak geliştirici erişilebilirliğini artırmak için P programlama dili ve PObserve gibi araçlar da devreye alındı
• S3 ShardStore’un özellik tabanlı testleri, deterministik simülasyon ve Aurora Limitless Database’in SQL fuzzing’i, biçimsel yöntemleri günlük geliştirme ve entegrasyon testlerine daha yaklaştıran örnekler
• Fault Injection Service; API hataları, I/O duraklatmaları ve instance arızaları gibi sorunları enjekte ederek dayanıklılık mekanizmalarını doğruluyor; Amazon.com, Prime Day 2024 hazırlık sürecinde FIS tabanlı 733 deney yürüttü
• Cedar, Firecracker ve Graviton 2 RSA optimizasyonu gibi güvenlik sınırları ile performans optimizasyonunun kritik olduğu alanlarda biçimsel kanıtlar kullanılıyor; yüksek öğrenme eğrisi ve araç erişilebilirliği ise benimsemenin önünde hâlâ kısıt olarak duruyor

---

AWS’nin sistem doğruluğunu ele alma biçimi

• AWS’nin müşterilerin güvenebileceği hizmetler sunabilmesi için güvenlik, dayanıklılık, bütünlük ve kullanılabilirlik konularında yüksek standartları koruması gerekir; sistem doğruluğu da bunu destekler
• CACM’de 2015’te yayımlanan “How Amazon Web Services Uses Formal Methods”, AWS’nin temel hizmetlerinin doğruluğunu garanti altına almaya yönelik yaklaşımını tanıttı; bu hizmetler daha sonra AWS müşterileri tarafından yaygın biçimde kullanılmaya başladı
• Başlangıçtaki ana araç, Leslie Lamport tarafından geliştirilen biçimsel belirtim dili TLA+ idi
  • Geleneksel testlerin kaçırabileceği ince hataları geliştirme sürecinin erken aşamalarında bulup ortadan kaldırmaya yardımcı olur
  • Sistem doğruluğunu korurken agresif performans optimizasyonları uygulanabileceğine dair güven sağlar
• 15 yıl önce AWS’nin test uygulamaları çoğunlukla derleme zamanındaki birim testlerine ve dağıtım zamanındaki sınırlı entegrasyon testlerine dayanıyordu
• AWS daha sonra biçimsel ve yarı biçimsel yöntemleri geliştirme sürecine entegre etti
  • Teorem ispatı, tümdengelimsel doğrulama, model checking
  • Özellik tabanlı test, fuzzing, çalışma zamanı izleme

P programlama dili ve PObserve

• AWS, 2010’ların başında biçimsel yöntemleri ilk ekiplerin ötesine yayarken, birçok mühendisin TLA+ öğrenmekte ve üretkenlik kazanmakta zorlandığını gördü
• TLA+’ın matematiğe yakın üst düzey bir soyut dil olması güçlü yanıdır; ancak imperatif dillere alışkın geliştiriciler için bir erişim engeline dönüşür
• Dağıtık sistem modelleme ve analizi için durum makinesi tabanlı dil P, bu boşluğu kapatma rolünü üstlendi
  • Geliştiriciler sistem tasarımını iletişim kuran durum makineleri olarak modeller
  • Bu zihinsel model, mikroservisler ve servis odaklı mimariyle (SOA) yoğun çalışan Amazon geliştiricilerine tanıdıktır
  • P, 2019’dan beri AWS’de geliştiriliyor ve stratejik bir açık kaynak projesi olarak sürdürülüyor
• Birçok önde gelen AWS ürün ekibi, sistem tasarımı doğruluğu incelemelerinde P kullanıyor
  • Depolama: Amazon S3, EBS
  • Veritabanları: Amazon DynamoDB, MemoryDB, Aurora
  • İşlem: EC2, IoT
• S3, eventual consistency’den strong read-after-write consistency modeline geçiş sürecinde P kullandı
  • S3 indeks alt sistemi, hızlı veri sorgulamayı mümkün kılan nesne metadata deposudur
  • Güçlü tutarlılığa ulaşmak için S3 indeks protokol yığınında önemsiz olmayan bir dizi değişiklik gerekiyordu
  • P, protokol tasarımının biçimsel olarak modellenip doğrulanmasını sağlayarak tasarım düzeyindeki hataların erken elenmesine ve riskli optimizasyonların model checking ile kontrol edilebilmesine imkân verdi
• 2023’te AWS P ekibi PObserve’u geliştirdi
  • Dağıtık sistem çalıştırmalarından çıkan yapılandırılmış logları kullanır
  • Logların sistemin biçimsel P belirtiminin izin verdiği davranışlarla uyumlu olup olmadığını sonradan doğrular
  • Rust veya Java gibi dillerde yazılmış üretim uygulamaları ile tasarım zamanındaki P belirtimleri arasındaki boşluğu azaltır
  • Tasarım zamanı doğrulamasıyla uygulamanın çalışma zamanı izlemesini bağlayarak biçimsel belirtim yatırımının değerini artırır

Hafif biçimsel yöntemleri geliştirme akışına ekleme biçimi

• AWS, hafif biçimsel yöntemleri benimseyerek biçimsel yöntemleri mühendislik ekiplerinin geliştirme ve test akışına daha da yaklaştırdı

• Özellik tabanlı test

  • Amazon S3’ün ShardStore’u, geliştirme döngüsü boyunca doğruluk testi ve geliştirme hızını artırmak için özellik tabanlı test kullanır
  • Birkaç yöntemi birlikte kullanarak insanların beklenen davranışı belirtmesini, otomatik testlerin ise daha fazla girdi ve hata koşulunu keşfetmesini sağlar
    • Geliştiricinin sağladığı doğruluk belirtimi
    • Kod kapsamı metrikleriyle girdi dağılımını yönlendiren coverage-guided fuzzing
    • Donanım ve diğer sistem arızalarını test sırasında simüle eden hata enjeksiyonu
    • Karşı örnekleri otomatik olarak küçülterek insanların hata ayıklamasını kolaylaştıran minimizasyon

• Deterministik simülasyon

  • Deterministik simülasyon testi, dağıtık sistemi tek iş parçacıklı bir simülatörde çalıştırır ve tüm rastgelelik kaynaklarını kontrol eder
    • Thread scheduling
    • Zamanlama
    • Mesaj teslim sırası
  • Geliştiriciler, dağıtık protokolün belirli bir aşamasında katılımcıların başarısız olması gibi belirli başarısızlık/başarı senaryoları yazabilir
  • Test framework’ü determinizm dışılığı kontrol ettiği için geçmişte hatalara yol açmış sıralar gibi ilginç yürütme sıraları belirtilebilir
  • Zamanlayıcı, sıra fuzzing’i veya tüm olası sıraların keşfi ile genişletilebilir
  • Gecikme ve arıza durumlarına ilişkin sistem özellik testlerini entegrasyon testlerinden derleme zamanına daha yakın taşıyarak geliştirmeyi hızlandırır ve davranış kapsamını genişletir
  • AWS’nin thread sıralaması ve sistem arızalarına yönelik derleme zamanı test çalışmalarının bir kısmı shuttle ve turmoil projeleri olarak açık kaynak hâline getirildi

• Sürekli fuzzing ve rastgele test girdisi üretimi

  • Sürekli fuzzing, özellikle coverage-guided tabanlı ölçeklenebilir test girdisi üretimi, entegrasyon zamanındaki sistem doğruluğu testlerinde etkilidir
  • Amazon Aurora’nın veri sharding özelliği olan Aurora Limitless Database geliştirmesinde iki temel özelliğin doğrulanması için fuzzing yaygın biçimde kullanıldı
  • SQL sorguları ve tüm transaction’lar fuzz edilerek shard’lar arasında SQL yürütme mantıksal bölümlendirmesinin doğru olduğu doğrulandı
  • Büyük miktarda rastgele SQL şeması, veri kümesi ve sorgu sentezlenerek test edilen engine’de çalıştırılır ve sonuçlar shard edilmemiş engine tabanlı oracle ile karşılaştırılır
  • SQLancer’ın öncülük ettiği yaklaşımlar gibi başka doğrulama yöntemleri de birlikte kullanılır
  • Fuzzing ile hata enjeksiyonu testlerinin birleşimi, veritabanlarının atomicity, consistency, isolation gibi doğruluk yönleri için de yararlıdır
    • Transaction’lar otomatik üretilir
    • Doğru davranış, biçimsel olarak belirtilmiş doğruluk oracle’ı ile tanımlanır
    • Transaction’lar ve transaction içindeki ifadelerin olası interleaving’leri test edilen sistemde çalıştırılır
    • Elle benzeri yaklaşımlar izlenerek isolation gibi özellikler sonradan doğrulanır

Fault Injection Service ve arıza durumlarının doğrulanması

• AWS, 2021’in başında Fault Injection Service(FIS) hizmetini kullanıma sunarak hata enjeksiyonu tabanlı testleri çeşitli AWS müşterilerinin kullanabilmesini sağladı
• FIS, AWS altyapısındaki test veya üretim dağıtımlarına simüle edilmiş arızalar enjekte edebilir
  • API hataları
  • I/O duraklatmaları
  • Başarısız instance’lar
• Hata enjeksiyonu, mimariye yerleştirilmiş dayanıklılık mekanizmalarının gerçekten kullanılabilirliği iyileştirip iyileştirmediğini ve yeni doğruluk sorunları yaratıp yaratmadığını kontrol etmeyi sağlar
  • Failover
  • Health check
• FIS tabanlı hata enjeksiyonu testleri, AWS müşterileri ve Amazon içinde yaygın olarak kullanılır
• Amazon.com, Prime Day 2024 hazırlık sürecinde FIS tabanlı 733 hata enjeksiyonu deneyi yürüttü
• 2014’te Yuan ve diğerleri, test ettikleri dağıtık sistemlerdeki ölümcül arızaların %92’sinin ölümcül olmayan hataların yanlış ele alınmasından tetiklendiğini analiz etti
• Normal yoldaki ölümcül arızaların nadir olmasının nedeni, normal yolun sık çalıştırılması, daha iyi test edilmesi ve hata yollarından çok daha basit olmasıdır
• Hata enjeksiyonu testleri ve FIS, arıza ve başarısızlık durumlarında sistem davranışını test etmeyi kolaylaştırarak normal yol ile hata yolu arasındaki hata yoğunluğu farkını azaltır
• Hata enjeksiyonunun kendisi biçimsel yöntem sayılmaz; ancak biçimsel belirtimlerle birleştirilebilir
  • Beklenen davranış biçimsel belirtimle tanımlanır
  • Hata enjeksiyonu sırasında ve sonrasında sonuçlar belirtilmiş davranışla karşılaştırılır
  • Yalnızca metrikleri ve log hatalarını kontrol etmeye ya da insanın gözle karar vermesine kıyasla daha fazla hata yakalayabilir

Metastabilite ve ortaya çıkan sistem davranışı

• Son 10 yılda belirli bir sistem arızası sınıfı olan metastable failures konusuna ilgi arttı
• Metastable failure, aşırı yük veya cache boşaltma gibi bir tetikleyicinin dağıtık sistemi müdahale olmadan toparlanamayacağı bir duruma itmesiyle oluşan arızadır
  • Müdahaleye örnek olarak yükün normalin altına düşürülmesi verilebilir
• Bu arıza sınıfı, bulut sistemlerinin kullanılamaz hâle gelmesinde önemli katkı faktörlerinden biridir
• Tipik metastable davranışta yük arttıkça başlangıçta goodput artar, sonra doygunluğa ulaşır, tıkanıklık yaşanır ve goodput sıfıra ya da sıfıra yakın bir değere düşer
• Bundan sonra sistem, yükü biraz azaltmakla sağlıklı hâline dönemez; toparlanabilmek için yükün ciddi ölçüde azaltılması gerekir
• Bu davranış basit sistemlerde bile ortaya çıkabilir ve çoğu sistemde timeout sonrası yeniden deneme yapan istemci mantığıyla da tetiklenebilir
• Geleneksel dağıtık sistem biçimsel modelleme genellikle safety ve liveness üzerine odaklanır; ancak metastable failures bu sınıflandırmaya düzgün biçimde sığmayan davranışlar olduğunu gösterir
• AWS, ortaya çıkan sistem davranışını anlamak için discrete-event simulation kullanımını artırıyor
  • Özel sistem simülasyonlarına yatırım yapıyor
  • TLA+ ve P gibi dillerle oluşturulmuş mevcut sistem modellerinin simülasyonda kullanılmasını sağlayan araçlara yatırım yapıyor
• TLA+’ın TLC’si gibi tam keşif yapan model checker’lar olasılıksal simülasyonla genişletilirse uçtan uca gecikme dağılımı gibi istatistiksel sonuçlar üretilebilir
• Bu tür genişletmeler, gecikme SLA’larına ulaşılabilirliği anlamak gibi işlerde model checking’den yararlanmayı sağlar

Biçimsel kanıt gerektiren güvenlik sınırları

• Yetkilendirme ve sanallaştırma gibi kritik güvenlik sınırlarında önceki biçimsel yöntemler tek başına yeterli olmayabilir; doğruluk kanıtları büyük yatırım değeri taşır

• Cedar yetki politikası dili

  • AWS, 2023’te ince taneli yetkileri belirten politikalar yazmak için Cedar yetki politikası dilini tanıttı
  • Cedar, otomatik akıl yürütme ve biçimsel kanıtlar dikkate alınarak tasarlandı
  • Uygulama, doğrulamaya elverişli programlama dili Dafny ile inşa edildi
  • Dafny aracılığıyla uygulamanın çeşitli güvenlik özelliklerini sağladığı kanıtlanır
  • Bu kanıt, testlerin ötesinde matematiksel anlamda bir kanıttır
  • Ekip ayrıca Dafny kodunu doğruluk oracle’ı olarak kullanan differential testing uygulayarak üretime hazır Rust uygulamasının doğruluğunu doğruladı
  • Cedar uygulamasıyla birlikte Dafny kodu ve test prosedürleri açık kaynak olarak yayımlanarak kullanıcıların doğruluk çalışmalarını inceleyebilmesi sağlandı

• Firecracker VMM

  • Firecracker sanal makine monitörü, virtio adlı düşük seviyeli protokolü kullanarak ağ kartı veya SSD gibi emüle edilmiş donanım aygıtlarını VM içindeki guest kernel’e sunar
  • Bu emülasyon aygıtları, güvenilmeyen guest ile güvenilen host arasındaki en karmaşık etkileşim olduğundan kritik bir güvenlik sınırıdır
  • Firecracker ekibi, Rust kodu üzerinde biçimsel akıl yürütmeye imkân veren Kani ile bu güvenlik sınırının temel özelliklerini kanıtladı
  • Bu kanıt, guest ne denerse denesin sınırın önemli özelliklerinin korunacağını garanti eder
  • AWS; Kani, Dafny, Lean ve bunları çalıştıran SMT solver’lar gibi temel araçların geliştirilmesini destekler
  • Biçimsel modeller ve belirtimler birden çok şekilde yeniden kullanılır
    • Tasarım zamanında model checking
    • Çalışma zamanı izlemede doğruluk oracle’ı görevi
    • Ortaya çıkan sistem davranışının simülasyonu
    • Temel özelliklerin kanıtlarının inşası

Doğruluğun ötesinde performans ve maliyet etkisi

• Biçimsel yöntemler, bulut sistemi performansını güvenli biçimde iyileştirmede de önemlidir
• Aurora ilişkisel veritabanı engine’inin temel commit protokolünü P ve TLA+ ile modellemek, safety özelliklerinden ödün vermeden dağıtık commit maliyetini 2 ağ gidiş-dönüşünden 1,5 ağ gidiş-dönüşüne düşürme fırsatını ortaya çıkardı
• Bu tür sonuçlar biçimsel yöntemleri benimseyen ekiplerde yaygındır
  • Dağıtık protokoller üzerine derinlemesine düşünmek ve bunları biçimsel olarak yazmak yapılandırılmış düşünmeyi zorunlu kılar
  • Protokol yapısı ve çözülmesi gereken problem hakkında daha derin içgörü sağlar
  • Önerilen tasarım optimizasyonunun doğru olduğu biçimsel olarak kontrol edilebilir veya kanıtlanabilirse, dağıtık sistem mühendisleri riski artırmadan daha cesur tasarımlar seçebilir
• Üretkenlik ve maliyet etkileri yalnızca üst düzey tasarım optimizasyonlarıyla sınırlı değildir
• AWS ekibi, ARM tabanlı Graviton 2 işlemcilerde RSA açık anahtar şifreleme uygulaması optimizasyonları bularak throughput’u %94’e kadar artırabildi
• Bu optimizasyonun doğruluğu, HOL Light etkileşimli teorem ispatlayıcısı kullanılarak kanıtlandı
• Bulut CPU döngülerinin yüksek bir oranı şifrelemeye harcandığı için bu tür optimizasyonlar altyapı maliyetlerinin azaltılmasına, sürdürülebilirliğin desteklenmesine ve müşterilerin hissettiği performansın iyileştirilmesine katkı sağlayabilir

Kalan zorluklar ve gelecekteki fırsatlar

• AWS, son 15 yılda biçimsel ve yarı biçimsel test yöntemlerini genişletmede başarılı oldu; ancak endüstriyel benimsemede hâlâ zorluklar var
• Biçimsel yöntem araçlarının başlıca engelleri dik öğrenme eğrisi ve uzman alan bilgisi gereksinimidir
• Birçok araç hâlâ akademik karakter taşır ve kullanıcı dostu arayüzlerden yoksundur
• İyi yerleşmiş yarı biçimsel yaklaşımlarda da benimseme engelleri sürer
  • Deterministik simülasyon, AWS ve FoundationDB gibi projelerde başarıyla kullanılan temel bir dağıtık sistem test yöntemidir; ancak AWS’ye katılan deneyimli dağıtık sistem geliştiricilerine bile yabancı gelebilir
  • Hata enjeksiyonu testi, özellik tabanlı test ve fuzzing gibi doğrulanmış metodolojilerde de benzer boşluklar bulunur
• Dağıtık sistem geliştiricilerine bu test yöntemleri ve araçlarını öğretmek, ayrıca titiz düşünme biçimini kazandırmak gerekir
• Eğitim açığı akademik düzeyde başlar
  • Temel biçimsel akıl yürütme yaklaşımları bile nadiren öğretilir
  • Üst düzey kurumlardan mezun olanlar bile bu araçları benimsemekte zorlanır
  • Biçimsel yöntemler ve otomatik akıl yürütme endüstriyel uygulama için önemli olsa da hâlâ niş alanlar olarak görülür
• Metastabilite ve büyük ölçekli sistemlerin diğer ortaya çıkan özellikleri de benzer farkındalık sorunları taşıyan önemli araştırma alanlarıdır
  • “Timeout olduğunda N kez yeniden dene” gibi metastable sistem davranışını tetikleyebilecek pratikler, bilinen sorunlara rağmen yaygın biçimde önerilmeye devam eder
  • Ortaya çıkan sistem davranışını anlamaya yönelik mevcut araç ve yöntemler erken aşamadadır
  • Sistem kararlılığı modellemesi maliyetli ve karmaşıktır
• AWS, büyük dil modelleri ve AI asistanlarının biçimsel yöntemlerin pratikte benimsenmesi sorununu hafifletmede büyük fayda sağlayacağını düşünüyor
  • AI destekli birim testlerinin popülerleşmesi gibi, geliştiricilerin biçimsel model ve belirtimler oluşturmasına yardımcı olabilir
  • Gelişmiş yöntemler daha geniş geliştirici topluluğu için erişilebilir hâle gelebilir

AWS’nin yatırım yapmayı sürdürdüğü doğruluk çerçevesi

• Güvenilir ve emniyetli yazılım oluşturmak için sistem doğruluğu üzerine akıl yürütmeye yönelik çeşitli yaklaşımlar gerekir
• AWS, birim testi ve entegrasyon testi gibi endüstri standardı testlerle birlikte çeşitli yöntemleri benimser
  • Model checking
  • Fuzzing
  • Özellik tabanlı test
  • Hata enjeksiyonu testi
  • Deterministik simülasyon
  • Olay tabanlı simülasyon
  • Yürütme izlerinin çalışma zamanı doğrulaması
• Biçimsel belirtimler, AWS’nin çeşitli test uygulamalarında doğru cevabı sağlayan test oracle’ı olarak önemli rol oynar
• Doğruluk testi ve biçimsel yöntemler, şimdiye dek sağladıkları yatırım getirisine dayanarak AWS’nin temel yatırım alanlarından biri olmaya devam ediyor