Gayriresmî İspatlar Neden Yeterli Değildir?

Protokol tasarımcıları düzenli olarak biçimsel olmayan güvenlik savları üretir — bir saldırganın neden başarılı olamayacağına ilişkin düzyazı biçiminde akıl yürütürler. Tarih, uzmanlar tarafından tasarlanan protokollerde bile bu savların sıklıkla yanlış olduğunu göstermektedir.

Needham-Schroeder (1978), karşılıklı kimlik doğrulama için tasarlanmıştı. Gavin Lowe, 1995'te otomatik doğrulama kullanarak ortadaki adam saldırısını buldu — yayımlanmasından 17 yıl sonra. Biçimsel olmayan kanıt, incelikli bir yeniden oynatma saldırısını gözden kaçırmıştı.

WEP, biçimsel olmayan güvenlik savlarıyla 1997'de IEEE tarafından onaylandı. 2001 yılına gelindiğinde araştırmacılar RC4 anahtar akışının yeniden kullanımını, IV çakışmalarını ve bütünlük eksikliğini buldu; bu sorunlar WEP'i dakikalar içinde kırılabilir hale getiriyordu. Biçimsel olmayan akıl yürütme bunların hiçbirini fark etmedi.

Protokol güvenliği; çok sayıda eşzamanlı oturum, etkin saldırganlar ve kriptografik varsayımlar arasındaki etkileşimlere bağlıdır. İnsan akıl yürütmesi, durum uzayı patlamaları ve iç içe geçmiş eşzamanlı yürütmeler karşısında zorlanır.

Biçimsel yöntemler protokolü matematiksel olarak modeller ve güvenlik özelliklerini (gizlilik, kimlik doğrulama, ileriye dönük gizlilik) yalnızca tasarımcının değerlendirdiği saldırılar için değil, tüm olası saldırgan stratejileri için kanıtlar veya çürütür.

Sembolik (Dolev-Yao): kriptografi kusursuz bir kara kutudur; odak noktası protokol mantığıdır. Hesaplamalı: gerçek olasılıksal güvenlik oyunları kullanılır; gerçek dünyadaki güvencelere daha yakındır. Her ikisi de gerçek hataları yakalar.

POODLE (2014), SSL 3.0 CBC'deki bir dolgu oracle'ından yararlandı. Güvenlik açığı bir uygulama hatası değil, protokol düzeyinde bir tasarım kusuruydu. SSL 3.0 belirtiminin biçimsel analizi, oracle'ı dağıtımdan önce ortaya çıkarabilirdi.

TLS 1.3 (RFC 8446), ProVerif ve miTLS kullanılarak yapılan biçimsel analizlerle birlikte tasarlandı. Belirtim, biçimsel bulgular temel alınarak yinelendi — standart kuruluşlarının biçimsel yöntemleri benimsemesinde bir dönüm noktası oldu.

Biçimsel araçlar uygulamayı değil, protokol modelini doğrular. Biçimsel olarak doğrulanmış bir protokolün uygulaması yine de güvensiz olabilir. F* / HACL*, doğrulamayı kriptografik kodun kendisine de genişletir.

Biçimsel doğrulama pahalıdır: protokol modellemesi haftalar sürer ve uzmanlık gerektirir. Ancak yüksek değerli hedefler (TLS, SSH, Signal) için maliyet haklıdır — tek bir protokol kusuru milyarlarca kullanıcıyı etkileyebilir.

Biçimsel olmayan kanıtlar başarısız olur; çünkü insan akıl yürütmesi eşzamanlı oturumlar arasındaki etkileşimleri ve saldırgan stratejilerini gözden kaçırır. Needham-Schroeder, WEP ve POODLE örneklerinin hepsinde biçimsel olmayan güvenlik savları vardı. TLS 1.3, tasarım sırasında biçimsel analizi sürece kattı. Biçimsel araçlar, protokol düzeyindeki hataları dağıtımdan önce yakalar.