Anthropic, Claude ile 123 açık kaynak kütüphaneyi assembly seviyesinde resmen doğruladı

Anthropic 123 kütüphaneyi makine yazımı kanıtlarla doğruladı

22 Ekim'de yayınlanan ve Hacker News'in ana sayfasına çıkan bir araştırma yazısında Anthropic, 123 gerçek dünya açık kaynak kütüphanesi için doğruluk kanıtları üretmek üzere Claude'ı kullandığını, güvenlik özelliklerini kaynak kodu yerine doğrudan derlenmiş RISC-V assembly üzerinde kanıtladığını belirtiyor. Proje doğrulama şirketi Theorem ile birlikte yürütüldü ve Anthropic, bunun üretim yazılımına assembly seviyesinde yapay zeka destekli resmi doğrulamayı uygulayan ilk büyük çaplı girişim olduğuna inanıyor. Kanıtları oluştururken Claude, trilyonlarca test çalıştırmasından geçmiş kodlarda bile yıllardır yakalanamayan hataları ortaya çıkardı.

Resmi doğrulama neden pratik olmaktan uzaktı

Sıradan testler davranışı yalnızca örnekleyebilir. Programa çökme tetiklemeyi umarak çok büyük sayıda üretilmiş girdi besleyen fuzzing doğası gereği kaba kuvvettir: girdi uzayı sonsuzdur, bu yüzden hiçbir fuzzing miktarı her hata yolunu elleyemez. Resmi doğrulama farklı bir yol izler. Geliştiriciler kodu matematiksel bir modele çevirir ve belirtilen bir kural kümesine her zaman uyduğunu kanıtlamaya çalışır. Bir kanıt başarısız olursa, başarısızlığın doğası olası bir hataya işaret eder; her başarısızlık düzeltildikten ve kanıt tamamlandıktan sonra kodun bu kuralları ihlal edecek hatalardan arınmış olduğu garanti edilir.

Tarihsel engel maliyettir. Anthropic, kanıtların kapsadıkları koddan çok daha büyük olabileceğini ve nadir, uzmanlaşmış bir beceri seti gerektirdiğini belirtiyor. seL4 çekirdeğinin uygulanması yaklaşık iki kişi-yılı, resmi olarak doğrulanması ise yaklaşık yirmi kişi-yılı sürdü; bu da tekniği havacılık-elektronik gibi alanlarla sınırladı. Anthropic'e göre sınır modeller bu ekonomiyi değiştiriyor, çünkü doğrulamayı sıradan projeler için pratik olmaktan çıkaran devasa kanıt iş yükünü özerk biçimde aşabiliyorlar.

Fuzz testlerinden belirtimlere

Doğrulamanın en zor kısmı "doğru"nun ne anlama geldiğini ifade etmektir. Bir PNG çözücüsünün RFC 2083'te doğal bir belirtimi vardır; bir web tarayıcısının veya metin düzenleyicinin yoktur. Anthropic'in çözümü, belirtimleri projelerin kendi test paketlerinden otomatik olarak türetmekti — belirtim basitçe paketin her zaman başarılı olduğunu söyler.

Uygulamada ekip, açık kaynak C ve C++ projelerini sürekli fuzzlayan Google'ın OSS-Fuzz programındaki fuzzing giriş noktalarını aldı ve Claude'dan, derlenmiş RISC-V talimatları üzerinde, 64 MB'a kadar hiçbir girdinin çökmeye yol açamayacağını kanıtlamasını istedi. Bu kanıtlandıktan sonra o giriş noktasının daha fazla fuzzlanması bir şey katmaz: fuzzer sonsuz bir girdi uzayından örneklerken kanıt tamamını kapsar.

Özellikle Claude, bu programların 64 MB altındaki her girdi ve modellenen her Linux yanıtı ile bellek düzeni için bellek güvenliği ihlali ya da başarısız doğrulama olmaksızın her zaman normal şekilde sonlandığını kanıtladı. Garantiler tek iş parçacıklı statik bir binary, sabit bir bellek bütçesi, bir RISC-V CPU ve Linux varsayar. Anthropic bunun olası her hatayı ortadan kaldırmaktan çok uzak olduğunu açıkça belirtiyor, ancak bunu daha geniş kapsama doğru güvenilir bir yol olarak çerçeveliyor.

Neler yayınlanıyor

Anthropic, kanıtların bir alt kümesini RISC-V ve Linux ortamına ilişkin resmi semantiğiyle birlikte yayınlıyor, böylece herkes bunları denetleyip yeniden kullanabilir. Theorem aynı hattı diğer açık kaynak projeler için çalıştıracağını ve geliştiricilerin kendi kodlarını doğrulamaya başlamalarına yardımcı olacak bir Claude skill yayınladığını söylüyor. Yazıda ayrıca diğer doğrulama görevlerine yönelik erken araştırmalar anlatılıyor: zlib sıkıştırma algoritmasının güvenliğinin değerlendirilmesi, Rust ile yazılmış bir Python yorumlayıcısının davranışsal eşdeğerliğinin kanıtlanması ve kritik yazılımlardaki köklü kusurların ortaya çıkarılması.

Neden önemli

Anthropic'in açıkladığı motivasyon savunmaya yönelik. LLM'ler kusurları bulmada ve tek tek zararsız hataları ciddi istismarlara zincirlemede giderek daha iyi hale geliyor ve yalnızca Linux çekirdeğinde yakın zamanda 1.000'den fazla açıklanmış güvenlik açığı görüldü. Ne kadar kapsamlı olursa olsun test, hataların varlığını gösterebilir ama yokluklarını asla; kanıtlar ise belirtimlerinin ve varsayımlarının sınırları içinde bunu yapabilir. Kanıt yazma maliyeti modeller geliştikçe düşmeye devam eder ve kod tabanları arasında yeniden kullanılabilir kanıtlar birikirse, resmi doğrulama havacılık sınıfı bir lüksten günlük açık kaynak yazılımını güvene almanın rutin bir parçasına dönüşebilir. Uyarılar önemli — buradaki garantiler yalnızca sınırlı girdiler, tek iş parçacıklı binary'ler ve modellenmiş bir işletim sistemi için geçerli — ama bir modelin artık bir zamanlar insan-on yıllarını tüketen işi yapabildiğinin gösterimi, gerçek kod tabanları için "test edilmiş" ifadesinin makul anlamını değiştiriyor.