Güvenliğin ve Güvenilirliğin Geleceği

Mars Insight’deki bilgisayar(lar) kısır döngüye girerse bu fotoğraflar gelemez.

Bu makale bir çağrıdır. Güvenlik konusunda “Yama mı tedavi mi?” sorusuna cevap vermek gerek.

Şimdilik yamalarla uğraşıyoruz. Gelecek için bu yeterli olmayacak! İşletim sistemleri ve yazılımların boyutları ve karmaşıklıkları devamlı artıyor. Linux çekirdeği (Kernel) 20 milyondan fazla satır kod içeriyor¹. Bu sadece çekirdeği. İşletim sisteminin bütünü bundan kat kat fazla.

Donanımımız aynı derecede karmaşık. 20 milyar (doğru okuyorsunuz milyon değil, milyar) kadar transistora sahip çipler de var²; 10 milyar transistorlu işlemciler artık normal olmaya başladı.

Her iki alanda çok eski ihtiyaçlara göre tasarlanmış sistemlerimiz var. C dili, Unix 45 senelik, Microsoft Windows ise 32 senelik. Linux 27 senelik. Intel x86 mimarisi 40 senelik, ARM 33 senelik.

Bu yüzden ne güvenlik ne de güvenirlilik dikkate alınarak tasarlanmamış bu sistemleri sağlamlaştırmak artık çok zor oluyor.

Güvenlik kelimesiyle bir sistemin olası saldırılara karşı bağışıklığını ifade etmek istiyoruz. Güvenirlilik kelimesiyle ise bir sistemin vaad ettiği işi çökmeden, durmadan ne kadar yapabileceğini kast ediyoruz.

Uçakların, arabaların, bizi hayatta tutan tıbbi aletlerin ve daha nicesinin bilgisayar tarafından yönetildiğini düşünürsek hem güvenlik hem güvenilirlik artık can alıcı bir öneme sahip.

Gelecekte IoT (Internet of Things), yazılımların güvenliği ve güvenilirliğine olan bağımlılığımızı daha da arttıracak.

Geçmişteki ve Bugünkü Çözümler

Yazılım tarihinde en eski yüksek güvenilirlik mazisine sahip yazılımlar uçak ve uzay araçlarında. Geçmişte bilgisayarları çoğaltarak bu sorun çözülmeye çalışıldı. Farklı donanım ve ayrı ayrı yazılmış yazılımlara sahip olan  bir kaç bilgisayar arasında kritik işlemler için oylama yapılırdı. Space Shuttle’in iki farklı tipte 5 kontrol bilgisayarı vardı³. Genellikle Avionics (uçak elektronikleri) alanında çoklu bilgisayar sistemleri kullanılır. Ancak bu bir noktaya kadar günü kurtarsa da hiçbir zaman nihai çözüm olmadı. Çoklu sistemlere ek olarak, sistematik ve her olası durumu öngörmeye çalışan testler  gerçekleştirmek, “Formal” yani yazılımın doğru çalıştığına dair matematikte gördüğümüz gibi bir ispat üretmek gerekmektedir.

Burada, maalesef, Türkiye’deki okur için duraksamak gerekiyor. “Matematikte gördüğümüz gibi” varsayımı Türkiye için bir yalan. Zira en az lise düzeyinde Türkiye’de hiç kimse “ispat” görmüyor. Üniversite düzeyinde matematikçiler dışında, örneğin mühendislik öğrencileri de “ispat” görmüyor.  İspat evrensel bir teoremin doğruluğunu belli aksiyomlardan başlayarak belli mantık kurallarını kullanarak göstermek anlamına geliyor.

Örneğin “Bu bilgisayar sistemi uçağın ‘stall’ (havada kalma gücünü yitirmek) etmesine izin vermez.” bir teorem olabilir.  Önemli bir teorem. Önkoşullar, aksiyomlar, varsayımlar, hepsi önemli, tabii. Ancak teoremin varolması sadece bir kaç defa uçağı uçurarak ve “bak düşmedi” demekten daha güvenli. Ancak genellikle yazılımlar için kullanılan yöntemler ikincisine daha çok benziyor.

Yine de bu kritik sistemler için, sistematik test, çoklu bilgisayar yanında, formal metotlar, yani ispat gerektiren yöntemler kullanılmaya başlanmıştır.

Örneğin Airbus 330/340 yazılım kılavuzuna göz atarsak formal metotların kullanılmaya başlandığını görüyoruz⁴.

Görsel 2: Airbus şirketinin yazılım geliştirme politikası

Formal ispat metotlarının kullanıldığı diğer bir güncel alan Mars’a giden robot uzay araçları.

NASA Departmanı olan JPL’nin (Jet Propulsion Laboratory) bir makalesinde araçtaki yazılımların, formal metotların ispat edilmesinin çeşitli matematiksel tekniklerle,  nasıl pratik haâle getirildiği anlatılıyor⁵. 100 milyon km. ötede seyredecek bir aracın bilgisayarının kısır döngüye girebilmesi, tabii ki, her halükârda önlenmeli.  

Ticari yazılımlara gelince bu formal metotlar hem pahalı oluyor, hem de yazılımların büyüklüğü yüzünden pratik olmuyor.⁶

Gelecekteki çözümler

Bu derginin geçen sayısındaki makalemde seL4⁷ kernelden bahsetmiştim⁸. Böyle girişimler güvenlik ve güvenilirliğinin geleceğini temsil ediyorlar.

Makale yayınlandıktan sonra CACM dergisinde seL4 kernelini kullanan bir sistem hakkında  bilimsel bir makalenin çıkması güzel bir tesadüf oldu.

Boeing’in AH-6 otonomu, insansız helikopter küçük bir drone ya da IHA değil. Tam boyutlu bir helikopter. Bu sistem hep güvenilirliği için test edildi, ancak 2013 yılında sızma testi için görevlendirilen bir “red team” helikopter sistemine başarılı bir siber saldırı gerçekleştirdi.

Saldıranlar helikoptere takılan bir USB cihazı vasıtasıyla helikopteri herhangi bir yere yönlendirmek ya da helikopteri düşürmek yetkilerini elde etmeyi başardılar.

Orijinal helikopter sistemi Linux tabanlı. Linux tamamen ortadan kaldırılamadı. Ancak seL4 kernel altında Linux’un izole edildiği bir sanal makine yaratıldı ve helikopterin kamera kontrolu gibi kritik olmayan yazılımları orada tutuldu. Bu yazılımların helikopteri uçuran yazılımlara ulaşması engellendi.

Ayrıca bir de “White Box saldırısı” denendi. “White Box saldırısı” şu anlama geliyor: saldıran takıma sistemin bütün kaynak kodları ve belgeleri ve ayrıca zayıf olan kamera sistemine kök erişim de veriliyor. Bütün bunlara rağmen, bu sefer, “red team” helikopterin uçuş sistemlerini etkileyemedi.

Görsel 3: Boeing Little Bird uçuşta – Pilotun yokluğu dikkatinizi çekmiş olmalı.

Peki bu nasıl başarıldı? Önce ispat edilmiş bir işletim sistemi, seL4 mikroçekirdeği kullanıldı. Çekirdeğin kendisi, kullanılan C derleyicisi ve diğer yazılımlar formal yöntemlerle ispat edilmiş sistemlerdi. Bu çekirdek altında birbirinden izole edilmiş sanal makinelerde çalışan yazılımlar üzerinde tek tek ispatlar sınanmış. Birbirinden izole olmadıkları için her yazılıma aynı sert kriterler uygulamak zorunda kalınmamış.

Projeyi uygulayanlar bu tarz yöntemler kullanarak yani mevcut bir sisteme “retrofit” yaparak sistemi daha güvenli bir hale getirebildiler.

Tabii bu belirli şartlar altında mümkün: seL4 mikroçekirdeği, Linux çekirdeği gibi 20 milyar satır değil, 10 bin satır C kodundan ibaret. Linux için böyle bir girişim imkansız.

İspatların geleceği

Uzay ve uçakların dışında güvenlik ve güvenilirlik nasıl sağlanır? Milyonlarca satırdan oluşan yazılımlarla ve C gibi dillerle bu iş kotarılamayacak. Başka faktörleri hesaba katmasak bile, C dilinin “undefined behavior” tuzağı tek başına bunu zorlaştırmak için yeterli. Birçok koşulda C dilinde yazılan programlar farklı davranışlar sergileyebilir. Bu güvenlik için bir felaket. Pratikte C dilinin bu niteliğinin en kötü sonuçlarını önlemek için hem programlara hem de derleyici davranışlarına ciddi sınırlamalar getirmek lazım. Bu sorunun ciddiyetini anlamak için John Egher’in makalelerini okumak yeterli⁹. C dilinde 200 farklı “undefined behavior” varken, saf C programların davranışlarını ispat etmek çok zor.

Formal yöntemler artık çok daha yaygın kabul görmeye başlıyor.  Çok önemli bir güvenlik zafiyeti olarak web tarayıcılarda çalıştırılan programlar. Genellikle bu programlar Javascript dilinde yazılıyor. Maalesef Javascript değişken tipleri konusunda zorlayıcı değil, ayrıca karışık ve programların anlamlarını tanımak için net bir formal sisteme sahip değil. Bu yüzden Google, Apple, Mozilla ve Micosoft’un ortak girişimi ile istemci programları için WebAssembly dili geliştirildi¹⁰. Başka dillerden farklı olarak WebAssembly’nin başta gelen özelliği formal oluşu, matematiksel bir semantics (dildeki programların anlamları belirleyen tanımlar) ve tip sistemi. Tiplerin önemini birazdan açıklayacağız.

İspat ve tip sistemleri önemli olacak. Bunun için yeni diller ve yeni işletim sistemleri gelecek. Yeni dillerde ispat, tip sistemi, formal semantics gibi yeni kavramlar önemli olacak. Bunlara alışmalı ve öğrenmeliyiz.

Tiplerin önemi

Güvenlik ve güvenilirlik istiyorsak, 40 senelik arkadaşlarımıza, Unix ve C diline hoşçakal, demek zorundayız. Bunların yerine işletim sistemi olarak seL4 gibi ispat edilebilir mikro çekirdekleri benimsemek zorundayız. Peki ya programlama dilleri için çözümümüz ne olacak?

İhtiyacımız iyi programlar yazmamızı kolay kılan bir dil değil. İhtiyacımız yanlış programlar yazmamızı imkânsız kılan bir dil.  Bu bir hedef. Teorik sebeplerden dolayı bu hedefe %100 ulaşamayabiliriz. Fakat bu hedefi yine de korumalıyız. Bunun için daha büyük programlarda ispatı kullanabilmek için dillerimize bazı önemli nitelikler eklemek işimizi kolaylaştıracak.

Programlarda “referential transparency” (şeffaflık), yani bir fonksiyon aynı parametrelerle değerlendirildiğinde aynı sonucu üretmesinin garanti ediliyor olması lazım. Dolasıyla dilimizde “mutation” yani değişkenin değerini değiştirmek mümkün olmamalı.

Yazılım dilimizde “undefined behavior” ‘a neden olabilen davranışlar yasaklanmalı, yani derleyici tarafından reddedilmeli. Bu da güçlü bir tip sistemini gerektiriyor.

Bunları gerçekleştirmek için functional typed bir dile ihtiyacımız var. Bügün elimizdeki diller bu ihtiyaca uygun olmayabilir. Fazla karmaşık ve fazla güçlüler. Turing Completeness ile beraber gelen arzu etmeyeceğimiz belirsizlikler var.

Yine de seL4 işletim sistemi referans uygulamasının Haskell’de yazılmış olması tesadüf değil.  Haskell pure functional typed bir dil.

Tiplerin gerekliliği iki basit örnekle anlatılabilir.  Başımıza bela olan iki önemli güvenlik açığı var. Biri Buffer Overflow, diğeri SQL injection. İkisi de tip uyumsuzluğundan kaynaklanıyor.   

Kullanıcının girdiği bir metin ve bir SQL komutu aynı tipte olmazsa, derleyicimiz, başka bir tedbire gerek olmaksızın, SQL injection saldırılarını engelleyebilir.  Yani SQL injection’a maruz kalabilecek bir program yazmak imkânsız hâle gelir. Buffer Overflow daha zor bir mesele. Tabii ki Java dili gibi ortamlarda, runtime’da Buffer Overflow gibi zafiyetleri önlemek mümkün, ama derdimiz derleyici aşamasında  bunu önleyebilmek.

Yaşantımızda her gün daha önemli bir yer işgal eden yazılımlara güvenebilmemiz için bu sorunları çözmek zorundayız. Her mühendislik sorunu gibi uzlaşmalar olacak. Yine de ispat edilebilen yazılımlar büyük önem kazanacak. Bunun için eski işletim sistemlerimiz ve programlama dillerimiz yetmeyecek.

Sonuç

Her zamanki gibi referans olarak verdiğim orijinal makalelerin okunmasını şiddetle tavsiye ediyorum. Bu makalelerin dili İngilizce, fakat yapacak bir şey yok! Zorlanarak da olsa okuyunuz. Çabanıza değecektir. Aynı zamanda makale okuma işini sürekli hâle getirdiğinizde teknik İngilizce’niz de gelişecektir.

Haskel, Rust gibi güçlü tip sistemleri olan programlama dillerini öğreniniz. Coq gibi ispat sistemlerini de öğreniniz. Güvenlik ve güvenilirlik ile uğraşmak istiyorsanız, gelecek budur.

Kaynaklar;

1. https://www.linuxcounter.net/statistics/kernel
2. EPYC: A Study in Energy Efficient CPU Design Nathan Brookwood https://www.amd.com/system/files/documents/The-Energy-Efficient-AMD-EPYC-Design.pdf
3. Architecture of the space shuttle primary avionics software system Gene D. Carlow Communications of the ACM CACM Volume 27 Issue 9, Sept. 1984 pp 926-936
4. New Avionics Systems —Airbus A330/A340 J.P. Potocki de Montalk http://www.davi.ws/avionics/TheAvionicsHandbook_Cap_30.pdf
5. Exploiting Traces in Static Program Analysis, Alex Groce, Rajeev Joshi https://agroce.github.io/sttt08.pdf
6. Formally Verified Software in the Real World, Gerwin Klein, June Andronick, Matthew Fernandez, Ihor Kuz, Toby Murray, Gernot Heiser, Communications of the ACM Volume 61 Issue 10, October 2018
7. Mathematically Verified Software Kernels: Raising the Bar for High Assurance Implementations Dr Daniel Potts, Rene Bourquin, Leslie Andresen, Dr June Andronick, Dr Gerwin Klein, Prof Gernot Heiser
8. Meltdown, Spectre ve Foreshadow, Yaklaşan Devrimin Ayak Sesleri,Chris Stephenson, Arka Kapı Dergi Sayı 4
9. A Guide to Undefined Behavior in C and C++, John Regehr, https://blog.regehr.org/archives/213
10. Bringing the web up to speed with WebAssembly Andreas Rossberg, Ben L. Titzer, Andreas Haas, Derek L. Schuff, Dan Gohman, Luke Wagner, Alon Zakai, J. F. Bastien, Michael Holman Communications of the ACM Volume 61 Issue 12, December 2018 Pages 107-115