Microsoft, yapay zekânın yazdığı giriş kodunu açık kurallarla doğruluyor
Microsoft Research, eylemcilerin yazdığı Rust web uygulamasının giriş akışında PDD Kit adlı doğrulama aracını gösterdi. Geliştiricinin niyeti açık koşullara dönüştürülüp bu koşullara ilişkin ispat denetleniyor. Örnek, parola kuralındaki eksik yönü ortaya çıkarırken doğrulanan giriş özelliklerini güvenilen bileşenlerden ve deneysel sınamalardan ayırıyor. Bütün uygulamanın güvenliğinin ispatlandığı ileri sürülmüyor; kapsam, tanımlanan giriş koşullarıyla sınırlı.
Yapay Zekâ··Gece
Giriş niyeti açık koşullara dönüşüyor
Microsoft Research, geliştiricinin istediği davranışı açık kurallara dönüştüren PDD Kit aracını, eylemcilerin yazdığı bir web uygulamasının giriş akışında gösterdi. Rust dilindeki örnek yaklaşık beş bin satır kod içeriyor. Axum ve SQLite arka uçta, WebAssembly’ye derlenen Leptos ise kullanıcıya görünen ön yüzde çalışıyor. PDD Kit, GitHub Next’in Chopin planlama ortamı içinde kullanılıyor. Rust için geliştirilen Verus doğrulayıcısı, ortaya çıkan ispatı denetliyor. Örnek giriş özelliklerine odaklanırken ispatın dışında kalan bileşenler ve kullanıcı arayüzündeki davranışlar deneysel sınamalarla ele alınıyor. Microsoft, bütün uygulamanın ispatlandığını ileri sürmüyor. Çalışmanın kapsamını, giriş sırasında beklenen davranışa ilişkin yazılmış koşullar belirliyor.[1], [2]
Doğru parola kuralı iki yönüyle kuruluyor
Geliştiricinin ilk isteği, yalnızca doğru parola girildiğinde erişim belirteci verilmesini ve yönetici belirtecinin yalnızca yöneticilere gitmesini söylüyor. PDD Kit, herkesi reddeden bir girişin de ilk sınırlamaya uyacağını ortaya koyuyor. Bunun üzerine ters yönü soruyor: doğru parola gerçekten erişim sağlamalı mı? Geliştirici iki yönü de seçiyor. Kurallar daha sonra veri tabanı sorgusunun sonucunu bekleyen ve belirteci imzalayan eş zamansız akışı da kapsıyor. Sekiz sonuç koşulu, parolası denetlenen hesapla belirteçteki kimliğin bağlantısını ve yönetici rolünün hangi yoldan verilebileceğini açıklaştırıyor. Bu ilişkilerin yazılması, doğrulayıcının neyi kanıtlamasının istendiğini değiştiriyor. Böylece genel bir giriş beklentisi, ayrı ayrı denetlenebilen davranış koşullarına dönüşüyor.[1]
Güvenilen bileşenler ispatın dışında kalıyor
Veri tabanı sorguları, parola denetimi, belirteç imzalama, saat, hata dönüşümü ve isteğin alanlarını açan dış katman için güvenilen varsayımlar ayrıca belirtiliyor. Bu varsayımlar sınamalarla incelenecek; geçen bir sınama, ispat yerine kanıt olarak adlandırılıyor. Örnek ayrıca işlemin mutlaka tamamlanmasını, hızını, yinelenen giriş denemelerinin sınırını veya diğer uçların rolleri nasıl yorumladığını garanti etmiyor. Microsoft, her sonuç koşulu için kasıtlı bir hata ekleyerek doğrulayıcının bunu reddedip reddetmediğini de deniyor. Bu değişiklik sınamaları, yazılan kuralların anlamlı sınırlamalar getirip getirmediğini araştırıyor. Geliştirici, güvenilen varsayımları tek tek kabul ediyor. Kurallar onaylandıktan sonra yapım aşaması görevleri oluşturuyor; eylemciler uygulamayı ve ispatı yazıyor, Verus bunları denetliyor ve güvenilen bileşenler planlanan sınamalardan geçiyor. İnsan, niyetini seçip kuralları belirlerken araç bunları ispatın denetleyeceği biçime getiriyor. Üçüncü taraf bileşenlerin davranışına ilişkin varsayımlar da bu ispatın hangi temellere dayandığını görünür kılıyor.[1], [2]
İlgili köşe yazıları
Bu gündem hakkında daha fazla bilgi için ilgili köşe yazılarını okuyabilirsiniz.
