Kanıt taşıma kodu - Proof-carrying code - Wikipedia

Kanıt taşıma kodu (PCC), bir ana bilgisayar sisteminin bir uygulama hakkındaki özellikleri bir resmi kanıt uygulamanın çalıştırılabilir koduna eşlik eden. Ana bilgisayar sistemi kanıtın geçerliliğini hızlı bir şekilde doğrulayabilir ve kanıtın sonuçlarını kendi sonuçlarıyla karşılaştırabilir. güvenlik Politikası uygulamanın çalıştırılmasının güvenli olup olmadığını belirlemek için. Bu, özellikle sağlanmasında yararlı olabilir bellek güvenliği (örn. gibi sorunları önlemek arabellek taşmaları ).

Kanıt taşıma kodu ilk olarak 1996'da George Necula ve Peter Lee.

Paket filtre örneği

Kanıt taşıma yasasına ilişkin orijinal yayın 1996^[1] Kullanılmış paket filtreleri örnek olarak: bir kullanıcı modu uygulaması, bir uygulamanın belirli bir ağ paketini işlemeyle ilgilenip ilgilenmediğini belirleyen çekirdeğe makine kodunda yazılmış bir işlevi verir. Paket filtresi çalıştığı için çekirdek modu çekirdek veri yapılarına yazan kötü amaçlı kod içeriyorsa, sistemin bütünlüğünü tehlikeye atabilir. Bu soruna yönelik geleneksel yaklaşımlar arasında alana özgü dil paket filtreleme için, her bir bellek erişimine kontroller ekleyerek (yazılım hatası yalıtımı ) ve filtre çalıştırılmadan önce çekirdek tarafından derlenen yüksek seviyeli bir dilde yazılır. Bu yaklaşımlar, kod her çalıştırıldığında değil, yalnızca yüklendiği zaman derleyen çekirdek içi derleme yaklaşımı dışında, bir paket filtresi kadar sık ​​çalıştırılan kod için performans dezavantajlarına sahiptir.

Prova taşıma kodu ile çekirdek, herhangi bir paket filtresinin uyması gereken özellikleri belirten bir güvenlik politikası yayınlar: örneğin, paketin dışındaki belleğe ve çalışma belleği alanına erişmez. Bir teorem atasözü makine kodunun bu politikayı karşıladığını göstermek için kullanılır. Bu ispatın adımları kaydedilir ve çekirdek program yükleyicisine verilen makine koduna eklenir. Program yükleyici daha sonra ispatı hızlı bir şekilde doğrulayabilir ve daha sonra herhangi bir ek kontrol olmaksızın makine kodunu çalıştırmasına izin verebilir. Kötü niyetli bir taraf makine kodunu veya kanıtı değiştirirse, ortaya çıkan kanıt taşıma kodu geçersiz veya zararsızdır (yine de güvenlik politikasını karşılar).

Ayrıca bakınız

• Yazılan derleme dili
• Program türetme
• Resmi doğrulama

Referanslar

• George C. Necula ve Peter Lee. Proof-Carrying Kodu. Teknik Rapor CMU-CS-96-165, Kasım 1996. (62 sayfa)
• George C. Necula ve Peter Lee. Prova Taşıma Kodunu Kullanan Güvenli, Güvenilmeyen Aracılar. Mobil Aracılar ve Güvenlik, Giovanni Vigna (Ed.), Bilgisayar Bilimi Ders Notları, Cilt. 1419, Springer-Verlag, Berlin, ISBN  3-540-64792-9, 1998.
• George C. Necula. Prova ile Derleme. Doktora tezi, Bilgisayar Bilimleri Fakültesi, Carnegie Mellon Univ., Eylül 1998.