Herkesi reddeden doğru kapı
Bir giriş ekranının yalnızca doğru parolayla açılmasını istiyoruz. Microsoft’un PDD Kit örneği, bu gündelik isteğin içinde saklanan ölçüm hatasını gösteriyor: herkesi geri çeviren bir kapı da yanlış parolaya hiç açılmaz. İstenen güvenlik kuralını kusursuz karşılar, ama giriş işlevini yerine getirmez. Araç bu nedenle geliştiriciye ters yönü de soruyor: doğru parola giriş sağlamalı mı? İki yönün birlikte seçilmesi küçük bir dil düzeltmesi gibi görünüyor. Oysa sınanan davranış değişiyor. Bence örneğin asıl araştırma değeri, üretilen koddan önce bu değişikliğin görünür olması.[1]
Buradaki müdahale, başarısız bir programı daha çok örnekle sınamakla sınırlı değil. Hangi sonucun başarı sayılacağını değiştiriyor. Yanlış parolanın kabul edilmemesi ile doğru parolanın kabul edilmesi ayrı gözlemler gerektiriyor. PDD Kit bunları aynı sözleşmede birleştiriyor; veri tabanı veya imzalama hatası gibi izin verilen hata yollarını da belirtiyor. Ben bu adımı, insanın niyetini ölçülebilir koşula çevirme çabası olarak okuyorum. Alternatif okuma daha dar: giriş, kuralları görece kolay yazılan bir örnek olduğu için bu açıklık elde edilmiş olabilir. Tek örnek, karmaşık bir ürünün bütün niyetlerinin aynı kolaylıkla ifade edilebildiğini göstermiyor.[1]
İspatın dayandığı dış halka
Gösterim yaklaşık 5000 satırlık bir Rust uygulamasında geçiyor, fakat yazının ispat odağı giriş akışı. Verus, bu akışın sekiz sonuç koşuluna uyduğunu denetliyor. Kontrol edilen parola ile erişim belirtecindeki hesabın aynı olması da koşullar arasında. Buna karşılık veri tabanı sorgusu, parola denetimi, saat ve belirteç imzalama gibi bileşenler kabul edilmiş sözleşmelere dayanıyor. Bu işlevlerin doğru çalışması ispatın öncülü; gösterimin kendi içinde ayrıca kanıtladığı sonuç değil. Microsoft bu dış halkayı adlandırıyor ve varsayımlar için deneysel sınamalar planlıyor. Geçen bir sınamayı ispat diye sunmaması, sonucun kapsamını okuyabilmek için gerekli ayrıntı.[1]
Bu sınır bana ölçüm düzeneklerindeki kalibrasyon sorununu düşündürüyor: hesaplama ne kadar kesin olursa olsun, girdiyi tanımlayan varsayımın yanlışlığı sonuçta kalır. Burada parola denetiminin anlamı veya sorgunun döndürdüğü hesabın doğruluğu dışarıda kabul ediliyor. İspat bu kabul üzerine güçlü bir akıl yürütme kuruyor. Benim çıkarımım, güvenilirlik değerlendirmesinin yalnızca ispat geçti mi sorusuna indirgenemeyeceği. Alternatif açıklama, bu küçük dış bileşenlerin yerleşik ve yeterince sınanmış olması nedeniyle asıl hata yükünün akışta bulunması. Gösterim, bu olası yararı bütün uygulamalarda ölçen karşılaştırmalı bir deney sunmuyor; hangi varsayımın hangi güvenceyi taşıdığını görünür kılıyor.[1]
Kasıtlı hatanın gösterdiği sınır
PDD Kit, her sonuç koşulu için kodun ayrı bir kopyasına kasıtlı hata yerleştiriyor. Herkesi reddetmek veya e-posta yerine önce kullanıcı adına bakmak verilen örnekler arasında. Doğrulayıcının ilgili hatayı reddetmesi bekleniyor. Bir hata geçiyorsa sorun yalnızca kodda aranmıyor; koşulun yeterince kısıtlayıcı olup olmadığı yeniden ele alınıyor. Bu, yazılmış bir kuralın amaçlanan ayrımı yapıp yapmadığını sınayan yararlı bir olumsuz kontrol. Bununla birlikte seçilen bozma örnekleri bütün yanlış tanımlanmış gereksinimlerin dökümü değil. İnsanların hiç yazmadığı bir gereksinim, kusursuzca denetlenen sözleşmenin dışında kalabiliyor.[1]
Örneğin sonunda elde edilen güvence bu nedenle belirli ve kullanışlı: kabul edilen dış bileşenler altında, tarif edilen giriş akışı sözleşmesine uyuyor. İşlemin mutlaka tamamlanması, ne kadar hızlı yanıt vermesi veya giriş denemelerinin sıklığı bu sözleşmede yok. Diğer uçların yönetici rolünü nasıl kullandığı da kapsam dışında. Ben PDD Kit’in katkısını, bu sınırları saklamadan daha güçlü bir doğrulama dili kurmasında görüyorum. Araştırma sorusu artık kod üretildi mi düzeyinde kalmıyor: insanın istediği davranış doğru tanımlandı mı, tanım anlamlı hataları eliyor mu ve güvenilen halka nerede başlıyor? Giriş kapısındaki küçük ters yön sorusu, bütün gösterimi bu yüzden taşıyor.[1]