Dil tabanlı güvenlik - Language-based security

Gelen bilgisayar bilimleri , dil tabanlı güvenlik ( LBS ) programlama dillerinin özelliklerini kullanarak bir yüksek düzeyde uygulamaların güvenliğini güçlendirmek için kullanılabilir tekniklerin kümesidir. LBS'nin bilgisayar güvenliğini uygulama düzeyinde uyguladığı ve geleneksel işletim sistemi güvenliğinin üstesinden gelemediği güvenlik açıklarını önlemeyi mümkün kıldığı kabul edilir.

Yazılım uygulamaları tipik olarak belirli programlama dillerinde belirtilir ve uygulanır ve bir uygulamanın kaynak kodunun savunmasız olabileceği saldırılara, kusurlara ve hatalara karşı koruma sağlamak için uygulama düzeyinde güvenliğe ihtiyaç vardır; programlama diline göre uygulamaların davranışını değerlendiren güvenlik. Bu alan genellikle dil tabanlı güvenlik olarak bilinir.

Motivasyon

SCADA gibi büyük yazılım sistemlerinin kullanımı tüm dünyada gerçekleşmekte ve bilgisayar sistemleri birçok altyapının çekirdeğini oluşturmaktadır. Toplum, su, enerji, iletişim ve ulaşım gibi altyapıya büyük ölçüde bağımlıdır ve bunların hepsi de tamamen işlevsel olarak çalışan bilgisayar sistemlerine dayanmaktadır. Bilgisayar belleği eksikliğinin LAX bilgisayarlarının çökmesine ve yüzlerce uçuşun ertelenmesine neden olması gibi, yazılımdaki hatalar veya hatalar nedeniyle kritik sistemlerin başarısız olduğuna dair iyi bilinen birkaç örnek vardır (30 Nisan 2014).

Geleneksel olarak, yazılımın doğru davranışını kontrol etmek için kullanılan mekanizmalar, işletim sistemi düzeyinde uygulanır. İşletim sistemi, bellek erişim ihlalleri, yığın taşma ihlalleri, erişim denetimi ihlalleri ve daha pek çok olası güvenlik ihlalini yönetir. Bu, bilgisayar sistemlerinde güvenliğin çok önemli bir parçasıdır, ancak yazılımın davranışını daha belirli bir düzeyde güvence altına alarak daha da güçlü güvenlik elde edilebilir. Derleme sırasında yazılımın birçok özelliği ve davranışı kaybolduğundan, makine kodundaki güvenlik açıklarını tespit etmek çok daha zordur. Kaynak kodun değerlendirilmesi ile derleme öncesinde programlama dilinin teorisi ve uygulaması da ele alınabilir ve daha fazla zafiyet ortaya çıkarılabilir.

"O halde geliştiriciler neden aynı hataları yapmaya devam ediyor? Programcıların hafızalarına güvenmek yerine, yaygın güvenlik açıkları hakkında bilinenleri kodlayan ve doğrudan geliştirme sürecine entegre eden araçlar üretmeye çalışmalıyız."

— D. Evans ve D. Larochelle, 2002

Dil tabanlı güvenliğin amacı

LBS kullanılarak, kullanılan tekniklere bağlı olarak yazılımın güvenliği birkaç alanda artırılabilir. Arabellek taşmalarına izin verilmesi ve yasadışı bilgi akışlarının gerçekleşmesi gibi yaygın programlama hataları , tüketici tarafından kullanılan yazılımlarda tespit edilebilir ve izin verilmeyebilir. Tüketiciye yazılımın güvenlik özellikleri hakkında bir miktar kanıt sağlamak, tüketicinin kaynak kodunu almak zorunda kalmadan yazılıma güvenebilmesini ve hataları kendi kendine kontrol etmesini sağlamak da istenmektedir.

Kaynak kodu girdi olarak alan bir derleyici, makine tarafından okunabilir koda çevirmek için kod üzerinde dile özgü birkaç işlem gerçekleştirir. Sözcüksel analiz , ön işleme , ayrıştırma , anlamsal analiz , kod oluşturma ve kod optimizasyonu derleyicilerde yaygın olarak kullanılan işlemlerdir. Derleyici, kaynak kodu analiz ederek ve dilin teorisini ve uygulamasını kullanarak, programın davranışını koruyarak yüksek seviyeli kodu düşük seviyeli koda doğru bir şekilde çevirmeye çalışacaktır.

Image
Sertifika veren bir derleyiciyi gösterme

Java gibi güvenli bir dilde yazılmış programların derlenmesi sırasında , kaynak kodun derlemeden önce başarıyla tür denetimi yapması gerekir. Tip denetimi başarısız olursa derleme gerçekleştirilmez ve kaynak kodun değiştirilmesi gerekir. Bu, doğru bir derleyici verildiğinde, başarıyla tip denetimi yapılmış bir kaynak programdan derlenen herhangi bir kodun geçersiz atama hatalarından arındırılmış olması gerektiği anlamına gelir. Bu, programın belirli bir hata nedeniyle çökmeyeceğine dair bir dereceye kadar garanti sağladığından, kod tüketicisi için değerli olabilecek bilgilerdir.

LBS'nin bir amacı, yazılımın güvenlik politikasına karşılık gelen kaynak kodunda belirli özelliklerin varlığını sağlamaktır. Derleme sırasında toplanan bilgiler, verilen programda tüketiciye güvenlik kanıtı olarak sunulabilecek bir sertifika oluşturmak için kullanılabilir. Böyle bir kanıt, tüketicinin tedarikçi tarafından kullanılan derleyiciye güvenebileceğini ve sertifikanın, kaynak koduyla ilgili bilgilerin doğrulanabileceğini ima etmelidir.

Şekil, sertifikalandırma derleyicisi kullanılarak düşük seviyeli kodun sertifikalandırılmasının ve doğrulanmasının nasıl oluşturulabileceğini göstermektedir. Yazılım tedarikçisi, kaynak kodunu açıklamak zorunda kalmama avantajını elde eder ve tüketiciye, kaynak kodun kendisinin değerlendirilmesi ve derlenmesine kıyasla kolay bir iş olan sertifikayı doğrulama görevi bırakılır. Sertifikayı doğrulamak için yalnızca derleyici ve doğrulayıcıyı içeren sınırlı bir güvenilir kod tabanı gerekir.

teknikler

Program analizi

Ana madde: Program analizi

Program analizinin ana uygulamaları , program optimizasyonu (çalışma süresi, alan gereksinimleri, güç tüketimi vb.) ve program doğruluğudur (hatalar, güvenlik açıkları vb.). Program analizi, derlemeye ( statik analiz ), çalışma süresine ( dinamik analiz ) veya her ikisine de uygulanabilir. Dil tabanlı güvenlikte program analizi, tür denetimi (statik ve dinamik), izleme , kusur denetimi ve denetim akışı analizi gibi birkaç yararlı özellik sağlayabilir .

Bilgi akışı analizi

Ana madde: Bilgi akışı

Bilgi akışı analizi, düzenli erişim kontrol mekanizmalarının yetersiz kaldığı yerlerde gizliliği ve bütünlüğü korumak için bir programdaki bilgi akışı kontrolünü analiz etmek için kullanılan bir dizi araç olarak tanımlanabilir .

"Bilgiye erişim hakkını, bilgiyi yayma hakkından ayırarak, akış modeli, güvenli bilgi akışını belirleme yeteneğinde erişim matrisi modelinin ötesine geçer. Pratik bir sistem, tüm güvenlik gereksinimlerini karşılamak için hem erişim hem de akış kontrolüne ihtiyaç duyar."

— D. Denning, 1976

Erişim kontrolü , bilgiye erişim kontrollerini zorlar , ancak bundan sonra ne olacağı ile ilgilenmez. Bir örnek: Bir sistemin iki kullanıcısı vardır, Alice ve Bob. Alice'in sadece kendisi tarafından okunmasına ve düzenlenmesine izin verilen bir secret.txt dosyası var ve bu bilgiyi kendisine saklamayı tercih ediyor. Sistemde ayrıca , sistemdeki tüm kullanıcılar için okunması ve düzenlenmesi ücretsiz olan public.txt dosyası da bulunmaktadır . Şimdi Alice'in yanlışlıkla kötü amaçlı bir program indirdiğini varsayalım. Bu program, secret.txt üzerindeki erişim kontrol kontrolünü atlayarak sisteme Alice olarak erişebilir . Kötü niyetli bir program daha sonra kopya içeriğini secret.txt ve yerlerde bunu public.txt okumak için Bob ve diğer tüm kullanıcıları sağlayan. Bu, sistemin amaçlanan gizlilik politikasının ihlali anlamına gelir.

Girişimsizlik

Girişimsizlik , daha düşük güvenlik sınıflandırmasına sahip değişkenlerin girişine bağlı olarak, daha yüksek güvenlik sınıflandırmasına sahip değişkenlerin bilgilerini sızdırmayan veya ifşa etmeyen programların bir özelliğidir . Girişimsizliği sağlayan bir program , alt değişkenlerde karşılık gelen aynı girdi kullanıldığında aynı çıktıyı üretmelidir . Bu, girişteki her olası değer için geçerli olmalıdır. Bu , programdaki daha yüksek değişkenlerin bir yürütmeden diğerine farklı değerlere sahip olsa bile , bunun alt değişkenlerde görünmemesi gerektiği anlamına gelir .

Saldırgan, davranışını eşlemeye çalışmak için tekrar tekrar ve sistematik olarak müdahalesizliği karşılamayan bir programı çalıştırmayı deneyebilir. Birkaç yineleme, daha yüksek değişkenlerin ifşa edilmesine yol açabilir ve saldırganın örneğin sistem durumu hakkında hassas bilgileri öğrenmesine izin verebilir .

Bir programın enterferanssızlığı karşılayıp karşılamadığı, güvenlik tipi sistemlerin varlığı varsayılarak derleme sırasında değerlendirilebilir .

Güvenlik tipi sistem

Ana madde: Güvenlik tipi sistem

Bir güvenlik tür sistemi bir tür tipi sisteminin kendi kodunun güvenlik özelliklerini kontrol etmek için yazılım geliştiriciler tarafından kullanılabilir. Güvenlik türleri olan bir dilde, değişken türleri ve ifadeler uygulamanın güvenlik politikası ile ilgilidir ve programcılar uygulama güvenlik politikasını tür bildirimleri aracılığıyla belirleyebilirler. Türler, yetkilendirme ilkeleri (erişim denetimi veya yetenekler olarak) ve bilgi akışı güvenliği dahil olmak üzere çeşitli güvenlik ilkeleri hakkında akıl yürütmek için kullanılabilir. Güvenlik türü sistemler, temel güvenlik ilkesiyle resmi olarak ilişkili olabilir ve tür denetimi yapan tüm programlar ilkeyi anlamsal anlamda karşılıyorsa, bir güvenlik türü sistemi sağlamdır. Örneğin, bilgi akışı için bir güvenlik türü sistemi, müdahale etmemeyi zorunlu kılabilir, yani tür denetimi, programda herhangi bir gizlilik veya bütünlük ihlali olup olmadığını ortaya çıkarır.

Düşük seviyeli kodun güvenliğini sağlama

Düşük seviyeli koddaki güvenlik açıkları, programı, programın daha fazla davranışının kaynak programlama dili tarafından tanımlanmadığı bir duruma götürecek hatalar veya kusurlardır. Düşük seviyeli programın davranışı derleyiciye, çalışma zamanı sistemine veya işletim sistemi ayrıntılarına bağlı olacaktır. Bu, bir saldırganın programı tanımsız bir duruma sürmesine ve sistemin davranışından yararlanmasına olanak tanır.

Güvenli olmayan düşük seviyeli kodun yaygın açıkları, bir saldırganın bellek adreslerine yetkisiz okuma veya yazma işlemleri gerçekleştirmesine olanak tanır. Bellek adresleri rastgele veya saldırgan tarafından seçilebilir.

Güvenli dilleri kullanma

Güvenli düşük seviyeli kod elde etmek için bir yaklaşım, güvenli yüksek seviyeli dilleri kullanmaktır. Güvenli bir dil, programcıların el kitabı tarafından tamamen tanımlanmış olarak kabul edilir. Güvenli bir dilde uygulamaya bağlı davranışa yol açabilecek herhangi bir hata, derleme zamanında algılanacak veya çalışma zamanında iyi tanımlanmış bir hata davranışına yol açacaktır. In Java , sınırların dizisi out erişmeleri halinde, bir özel durum olacaktır. Diğer güvenli dillere örnek olarak C# , Haskell ve Scala verilebilir .

Güvenli olmayan dillerin savunma amaçlı yürütülmesi

Güvenli olmayan bir dilin derlenmesi sırasında, kaynak düzeyinde tanımsız davranışı algılamak için düşük düzeyli koda çalışma zamanı denetimleri eklenir. Bir örnek, sınır ihlallerini keşfederken bir programı sonlandırabilen kanaryaların kullanımıdır . Sınır denetimi gibi çalışma zamanı denetimlerini kullanmanın bir dezavantajı, önemli ölçüde performans yükü getirmeleridir.

Yürütülebilir olmayan yığın ve/veya yığın kullanma gibi bellek koruması , ek çalışma zamanı denetimleri olarak da görülebilir. Bu, birçok modern işletim sistemi tarafından kullanılır.

Modüllerin izole yürütülmesi

Genel fikir, kaynak kodu analiz ederek uygulama verilerinden hassas kodu belirlemektir. Bu yapıldıktan sonra farklı veriler ayrılır ve farklı modüllere yerleştirilir. Her modülün içerdiği hassas bilgiler üzerinde tam kontrole sahip olduğu varsayıldığında, modülden ne zaman ve nasıl ayrılacağını belirlemek mümkündür. Bir örnek, anahtarların modülden şifrelenmemiş olarak ayrılmasını engelleyebilen bir şifreleme modülüdür.

Sertifikalı derleme

Derlemenin sertifikalandırılması, kaynak kodun derlenmesi sırasında üst düzey programlama dili semantiğinden gelen bilgileri kullanarak bir sertifika üretme fikridir. Bu sertifika, kaynak kodun belirli bir dizi kurala göre derlendiğine dair tüketiciye bir tür kanıt sağlamak için derlenmiş kodla birlikte eklenmelidir. Sertifika farklı şekillerde üretilebilir, örneğin Proof-taşıma kodu (PCC) veya Yazılan derleme dili (TAL).

Kanıt taşıma kodu

PCC'nin ana yönleri aşağıdaki adımlarda özetlenebilir:

  1. Tedarikçi, sertifika veren bir derleyici tarafından üretilen çeşitli açıklamalar içeren yürütülebilir bir program sağlar .
  2. Tüketici, bir güvenlik politikasına dayalı olarak bir doğrulama koşulu sağlar . Bu tedarikçiye gönderilir.
  3. Tedarikçi , programın güvenlik politikasını gerçekten karşıladığını tüketiciye kanıtlamak için doğrulama koşulunu bir teorem kanıtlayıcısında çalıştırır .
  4. Tüketici daha sonra kanıt geçerliliğini doğrulamak için kanıtı bir kanıt denetleyicisinde çalıştırır .

Onaylayıcı bir derleyici örneği, Java'da uygulanan programlar için tür ve bellek güvenliğinin PCC biçimsel kanıtını sağlayan Touchstone derleyicisidir .

Yazılan derleme dili

TAL, bir tür sisteminden yararlanan programlama dillerine uygulanabilir . Derlemeden sonra, nesne kodu , sıradan bir tür denetleyicisi tarafından kontrol edilebilecek bir tür açıklama taşıyacaktır. Burada üretilen açıklama, bazı sınırlamalarla birlikte PCC tarafından sağlanan açıklamalara birçok yönden benzerdir. Bununla birlikte, TAL, diğerleri arasında bellek güvenliği ve kontrol akışını içerebilen tip sisteminin kısıtlamalarıyla ifade edilebilecek herhangi bir güvenlik politikasını işleyebilir.

seminerler

Referanslar

Kitabın

  • G. Barthe, B. Grégoire, T. Rezk, Sertifikaların Derlenmesi , 2008
  • Brian Chess ve Gary McGraw, Güvenlik için Statik Analiz , 2004.

daha fazla okuma