Bilgisayar Programlarında Güvenlik
Prof. C. A. R. Hoare
Programming Research Group, Computation Laboratory
Oxford Üniversitesi, Oxford, İngiltere
“Bilgisayar programlarının doğruluğunu, modelleme, hesaplama ve ispat gibi olağan matematiksel tekniklerle ortaya koyabilirsiniz … ancak bu yöntem, uygun tutumlar ve yönetsel tekniklerle desteklenmedikçe, uygulamada asla etkili olamaz.”
Bilgisayarları Denetleyen Programlar
Yayın Bilgileri
Editör ve Yayıncı: Edmund C. Berkeley
Yardımcı Yayıncı: Judith P. Callahan
Yardımcı Editörler: Neil D. Macdonald; Judith P. Callahan
Sanat Editörü: Grace C. Hertlein
Yayın Asistanı: Katherine M. Toto
Yayın Kurulu: Elias M. Awad; Grace C. Hertlein; Ed Burnett
Ofisler:
Berkeley Enterprises, Inc.
815 Washington St.
Newtonville, MA 02160, ABD
(617) 332-5453
“Computers and People” (ISSN 0361-1442) iki ayda bir Berkeley Enterprises, Inc. tarafından yayımlanır. ABD’de basılmıştır.
Abonelik Ücretleri (1 Eylül 1986’dan itibaren geçerli):
ABD: bir yıl için 22,00 $; iki yıl için 43,00 $
Diğer yerler: yıl başına 7,00 $ eklenir
© Telif Hakkı 1987, Berkeley Enterprises, Inc.
Dijital bilgisayarlar, insanlığın geliştirdiği en güvenilir mekanizmalar olmalıdır. Dünya genelinde milyonlarca bilgisayar ve uzayda binlercesi, her bir bilgisayarı oluşturan milyonlarca bitten herhangi birinde tek bir hata olmaksızın, saniyede milyarlarca komutu milyarlarca saniye boyunca yürütmektedir. Buna rağmen, çok azımız hayatımızı bir bilgisayara emanet ederiz.
Sorun bilgisayarın donanımında değil, onu denetleyen programlardadır. Programlar, onları yazan programcıların hatalarını, ihmallerini, yetersizliklerini ve yanlış anlamalarını sadakatle yeniden üretir. Yaygın biçimde kullanılan bazı büyük programlarda, işletim sistemlerinde ve derleyicilerde her yıl yüzlerce yeni hata keşfedilmektedir. Programcılar hataları düzelttiklerinde bile, kullanıcıların yeni hatalar bulmaya devam etme oranı on yıllar boyunca sabit kalmaktadır. Hatta bazıları, her düzeltmenin birden fazla yeni hata getirdiğinden kuşkulanmaktadır. Ve bu programlardaki hataların yalnızca çok az bir bölümü, programlar yeni ürünlerle yer değiştirmeden önce keşfedilecektir. Bu yeni ürünler de elbette aynı derecede güvenilmezdir.
İnce Hatalar
Genel amaçlı bilgisayar programlarında bulunan hataların çoğu son derece incedir: etkileri ciddi değildir ve yazılımın sağlayıcısı bunları düzeltmeye sıra getirene kadar onlardan kaçınmak kolaydır. Ancak bilgisayarlar, "yaşam açısından kritik uygulamalar"da giderek daha fazla rol oynamaya başlamaktadır; yani hataların keşfedildikten sonra düzeltilmesinin kabul edilebilir bir seçenek olmadığı durumlarda—örneğin endüstriyel süreçlerin, nükleer reaktörlerin, silah sistemlerinin, petrol platformlarının, uçak motorlarının ve demiryolu sinyalizasyonunun denetiminde. Bu tür projelerden sorumlu mühendisler, bu görevleri yerine getiren programların doğruluğu konusunda doğal olarak kaygılıdır ve sorunu ele almak için çeşitli geçici çözümler önermişlerdir. Önerilen dört yönteme ilişkin bazı örnekler vereyim.
Düzeltme Örnekleri
İlk yöntem en basit olanıdır. Bunu bir hikâye ile açıklayayım.
Brunel’in SS Great Britain adlı gemisi Thames Nehri’ne indirildiğinde, öyle büyük bir sıçrama yaptı ki karşı kıyıdaki birkaç seyirci boğuldu. Günümüzde mühendisler, suya giriş kuvvetini, dikkatle hesaplanmış aralıklarla kopacak şekilde tasarlanan halat bağlarıyla azaltmaktadır.
Amsterdam’daki Mathematisch Centrum’da ilk bilgisayar faaliyete geçtiğinde, ilk görevlerden biri bu bağların uygun aralıklarını ve kopma dayanımlarını hesaplamaktı. Hesaplamaları yapan programın doğruluğunu güvence altına almak için, programcılar karşı kıyıda kurulan tören seyir tribününün ön sırasından indirmeyi izlemeye davet edildiler. Daveti kabul ettiler ve hayatta kaldılar.
Benzer bir çözüm, sert deniz koşullarında bir petrol sondaj platformunun ayağına yakın konumunu korumak zorunda olan bir geminin pervane ve dümenini denetleyen programlar için de önerilmiştir. Rüzgârın ve dalgaların etkisi o kadar ani olur ki, hiçbir insan dümenci çarpışmayı önleyemez; bu görev bir bilgisayar programına devredilmelidir. Ancak programcıdan, programının güvenilirliğini gemi mürettebatına katılarak göstermesini istersek, yüksek maaşlı görevinden ayrıldığında bir soru ortaya çıkar. Bu ayrılış can sıkıntısından mı, deniz tutmasından mı, yoksa daha kötü bir şey korkusundan mı kaynaklanmaktadır?
Programların İncelenmesi
İlk Amerikan uyduları başlangıçta yerleşik bilgisayarlar tarafından denetlendiğinde, programlar dış yükleniciler tarafından yazılmıştı. Teslim alındıklarında, denetçiler programların mutlak ikili kodunu görsel olarak incelediler: satır satır ham ikili rakamlar. Daha üst düzey herhangi bir programlama dili kullanamazlardı; çünkü assembler’lar ve derleyiciler büyük programlardır ve bu nedenle derledikleri programlardan bile daha az güvenilirdirler.
Bu "gözle inceleme"yi desteklemek için NASA, örneğin teslim edilen ikili koddan assembly kodunu yeniden oluşturmak, akış şemaları çizmek ve tüm denetim yollarını analiz etmek gibi amaçlarla devasa bir program paketi geliştirdi. İnsan denetçiler daha sonra bu şemaları, aritmetik işlemlerin ölçekleme katsayılarına ilişkin önermelerle notlandırdılar; makinelerin yardımıyla, program her döngüden geçtiğinde ölçekleme katsayısının değişmeyeceğini denetlediler.
İkili Kodun Hiçbir Şeye Karşı Denetlenmesi
Bu yaklaşımın temel kusuru şudur: bir şeyi denetlerken, onu her zaman ya güvenilir olduğunu bildiğiniz ya da bir başkası tarafından benzer biçimde denetlenmiş olan başka bir şeye karşı denetlemelisiniz. İkili kodu, kendisinden başka hiçbir şeye karşı denetlemek son derece ürkütücü bir görevdir ve belgeleri, tasarımları ve teknik şartnameleri yeniden kurmak için ilham verici tahminler gerektirir. Denetlemenin, soyuttan somuta, şartnameden tasarıma ve oradan kodun hacimli ayrıntılarına doğru ilerleyen daha doğal yönde gelişen asıl programlamadan bile daha pahalı olması şaşırtıcı değildir.
Bu tür makine destekli analizler, güvenlik açısından kritik yazılımların denetlenmesinde hâlâ çok popülerdir. Gösterilen gerekçe hiç de güven verici değildir: programların çoğu hiçbir şartname olmaksızın yazılmaktadır; dolayısıyla denetlenecek tek şey nihai koddur. Temel hata, denetlemenin çok geç yapılmasıdır: kalite kontrolün temel bir ilkesi, denetlenmesi gerekenin ürün değil, onun üretildiği yöntemler olduğudur. Güvenilirliğe ulaşmak ancak yöntemlerin iyileştirilmesiyle mümkün olur.
Simüle Edilmiş Bir Ortamda Denetleme
Kritik süreçleri denetleyen programları, başlangıçta simüle edilmiş bir ortamda—örneğin hızlı bir ana bilgisayarın içinde—çalıştırarak sıklıkla test edebiliriz. Varsayalım ki simülasyon gerçek zamandan çok daha hızlı çalışıyor. Böylece bir yıl içinde, örneğin sürecin bin yıllık işletimini simüle etmek ve programın verdiği tüm yanıtları denetlemek mümkün olabilir. Yalnızca birkaç hata saptanırsa, bu tür bir hatanın canlı çalışmanın ilk 10 yılı içinde ortaya çıkması pek olası değildir—ki bu süre programın yararlı ömrünün uzunluğu olabilir.
Bu çekici yöntem birkaç yıkıcı sakınca taşır. Bunlardan ilki ve en hafifi, çalışan bir programın kurulmasından önceki gecikmenin genellikle kabul edilemez olmasıdır.
İkinci kusur felsefidir: bilinen hataları olan bir programla insanların hayatını riske atmak ahlaken son derece zordur. Oysa bilinen hataları "düzeltmek" yalnızca tamamen etkisiz olmakla kalmaz; aynı zamanda felaketle sonuçlanabilir, çünkü tamamen bilinmeyen yeni bir hata grubunu ortaya çıkarabilir. Bu olasılığa karşı koymak için, tüm testlerin baştan itibaren yeniden yapılması gerekir.
Üçüncüsü pratik bir kusurdur. Bin yıllık testte 10 hata tespit edilirse ne olur? Bu sonuç, gerçek kullanımın 10 yılı içinde bir hatanın ortaya çıkması açısından oldukça kabul edilemez bir risk verir. Tek çare, tüm programı yeniden yazmak ve testi yeniden başlatmaktır. O zamana kadar proje değerini ve güncelliğini yitirmiş olacaktır.
Dördüncüsü mantıksal bir kusurdur: yöntem, simüle edilen ortamın doğruluğuna ve denetleme programının doğruluğuna bağlıdır. Oysa denetleme programı doğruysa, neden onu gerçek süreci denetleyen programın bir parçası ya da tamamı olarak kullanmayalım?
Beşinci sakınca, neyse ki önceki dördünü önemsiz kılar: yalnızca çok basit ve giderek daha da nadir hale gelen uygulamalarda, en hızlı süper bilgisayarlarda bile, gerçek zamandan daha hızlı bir hızda simülasyon çalıştırmak mümkündür. Bu nedenle bu yöntem yalnızca tasarım ömrü dakika ya da saatlerle ölçülen programlar için uygulanabilir; dolayısıyla çoğu sivil uygulama için uygun değildir.
Oylama
Hayat açısından kritik birçok uygulamada, donanımın güvenilirliği sorunu, çıkışlarında her eylemin en az ikisinin onayını sağlayan bir oylama devresi bulunan, üç ya da daha fazla özdeş bilgisayar gerektirir. İki ya da daha fazla bilgisayarın aynı anda bozulma olasılığı, yalnızca birinin bozulma riskinden çok daha küçüktür. Donanım mevcut olduğuna göre, aynı tekniği yazılıma da uygulamak mümkündür. Üç ya da daha fazla bağımsız programcı ekibine, üç ya da daha fazla bağımsız program yazdırırsınız ve her bilgisayara farklı birini yüklersiniz. Programlardan biri ara sıra hataya düşerse, aynı anda hataya düşmeleri olası olmayan diğer programlar onu oylamayla saf dışı bırakır.
Donanımda bu tür bir yöntem, silikon yonga üzerine ara sıra çarpan kozmik bir ışının yol açabileceği türden geçici hatalarla başa çıkar. Ancak kalıcı arızalarla başa çıkamaz; bunların manuel (ya da otomatik) bileşen değişimiyle giderilmesi gerekir. Ne yazık ki yazılımda hataların geçici olduğunu varsaymak için hiçbir neden yoktur; tek bir hatalı alt indis, programın üzerine yazılmasına yol açabilir ve böylece bir daha hiç çalışmamasına neden olabilir. Bu olasılığa karşı korunmak için, donanımın her çalışma çevrimi arasında belleği temizleyecek ve programı yeniden yükleyecek şekilde tasarlanması gerekir. Dolayısıyla bu teknik yalnızca çalışması birbirinden bağımsız çevrimler dizisi olan, uzun vadeli depolaması bulunmayan programlara uygulanabilir. Böyle bir program geçmiş ölçümleri biriktiremez; onları tümleştiremez ya da yumuşatamaz. Bu nedenle teknik yalnızca basit denetim süreçleri için geçerlidir.
Bu yöntemdeki ikinci bir zayıflık, bağımsız programcılar tarafından üretilen programlardaki hataların bağımsız olacağını varsaymak için hiçbir neden olmamasıdır. Tam tersine. Programcılar çoğu zaman aynı “kültür” içinde eğitim alırlar; aynı şeyleri zor bulurlar ve aynı tür yanlış anlamalara ve ihmallere maruz kalırlar—örneğin uç bir durumu test etmeyi unutmak ya da bir döngünün sıfır yinelemesi durumunu ele almamak gibi.
Yazılımla İlişkili Donanım
Ancak büyük sistemlerde çeşitliliği pratik olmaktan çıkaracak yeni bir durum vardır. Gerçek zamanlı uygulamalarda, bir bilgisayarın tepkisi, yanıt verdiği sinyallerin zamanlamasının ayrıntılarına bağlıdır—örneğin bir kesmenin geliş anına. Bu nedenle, sinyalleri biraz farklı zamanlarda alan iki doğru program farklı sonuçlar verebilir; her ikisi de doğru sonuçlardır. Ne yazık ki donanımdaki basit bir oylama devresi bunu bilemez ve gereksiz alarmlar tetikler. Bunu önlemek için yoğun çabalar gösterilmesine rağmen, Amerikan uzay mekiğinin ilk fırlatma girişiminde gerçekte olan da buydu. Columbia, bir bilgisayar programının ilk son derece gösterişli ve kamuoyuna yansıyan başarısızlığının kurbanı oldu. Başarısızlığın nedeni, güvenilirliği sağlamak için tasarlanmış olan tekniğin ta kendisiydi.
Uzun süre çalışan programlar için çeşitlilik kullanmanın daha sinsi bir tehlikesi vardır. Bir yazılım hatası meydana geldiğinde, donanım karşılaştırma devresi bir alarm verecektir; ancak operatörler bu uyarıyı bir yazılım hatasına bağlayacak ve görmezden geleceklerdir. Sonuç olarak, gerçekten donanım bozulduğunda, operatörlerin bunu bir yazılım hatasından ayırt etmeleri imkânsız olacak ve uyarıyı görmezden gelmeye devam edeceklerdir. Böylece aralıklı ve kusurlu donanım zamanında değiştirilmeyecektir.
Donanımın, yazılımın güvenilmezliğiyle bu şekilde enfekte olması, ALGOL (ALGOrithmic Language, sayısal işlemlerin standart bir biçimde bilgisayara kesin olarak sunulmasını sağlayan aritmetik bir dil) derleyicisinin, başlatılmamış bir değişkenin programlama hatasını tespit etmek için donanım eşlik ihlali devrelerini kullandığı bir bilgisayarda gerçekten gözlemlenmiştir. Kısa bir süre içinde, bakım eksikliğinin bir sonucu olarak, bu derleyiciyi kullanan her bilgisayarın ana belleğinin donanımı güvenilmez hale gelmiştir.
Matematik Bir Çözüm Sunar
Bunlar, güvenlik açısından kritik yazılımların geliştirilmesi için insanların önerdiği ve pratikte kullandığı dört yöntemdir. Bildiğim kadarıyla, şimdiye kadar neredeyse tamamen başarılı olmuşlardır ve hiçbir büyük ölçekli insan kaybı bir programlama hatasına atfedilmemiştir. Buna rağmen, her yöntem, güvenliği bilgisayar programları tarafından izlenen sistemlerin ölçeği ve karmaşıklığındaki yaklaşan artışla birlikte daha ciddi hale gelebilecek çeşitli sakıncalardan muzdariptir.
Bu nedenle, programların güvenilirliğini artırma vaadi taşıyan ek bir yöntemi araştırmamız gerektiğini öneriyorum. Aynı yöntem, mühendisliğin diğer dallarında da tasarımların güvenilirliğine yardımcı olmuştur; yani bir tasarımı inşa ve kuruluma geçmeden önce, matematik kullanarak parametrelerini hesaplamak ve sağlamlığını denetlemek.
Alan Turing bu öneriyi yaklaşık 40 yıl önce ilk kez dile getirdi; bilgisayar biliminin diğer büyük öncüsü John von Neumann tarafından da zaman zaman uygulamaya kondu. Shigeru Igarashi ve Bob Floyd, yaklaşık 20 yıl önce bu fikri yeniden gündeme getirdiler ve ilgili matematiksel tekniklerin geliştirilmesini amaçlayan geniş ve derin bir araştırma hareketinin temelini sağladılar. Wirth, Dijkstra, Jones, Gries ve daha pek çok kişi (ben de dahil) önemli katkılarda bulundu. Yine de bildiğim kadarıyla, mevcut matematiksel yöntemler kullanılarak tek bir güvenlik açısından kritik program bile hiçbir zaman denetlenmemiştir. Dahası, güvenlik açısından kritik projelerin çeşitli kademelerinde çalışan ve bilgisayar programlarının tam doğruluğunun, modelleme, hesaplama ve ispat gibi normal matematiksel tekniklerle ortaya konabileceği olasılığını hiç duymamış birçok programcı ve yöneticiyle karşılaştım.
Böylesi bir tam cehalet kasıtlı gibi görünebilir ve belki de öyledir. Güvenlik açısından kritik projelerde çalışan insanlar ağır bir sorumluluk taşırlar. Güvenilirlikte bir iyileşmeye yol açabilecek bir yöntemden haberdar olurlarsa, bunu derinlemesine incelemekle yükümlüdürler. Bu ise onlara mevcut projelerini zamanında ve bütçe dahilinde tamamlama fırsatı bırakmaz. Sanırım bu nedenle hiçbir endüstri ve hiçbir meslek, etkili ve ilgili bir güvenli çalışma uygulamaları kodunu gönüllü ve kendiliğinden geliştirmemiş ya da benimsememiştir. Gönüllü kodlar bile ancak kamuoyundaki huzursuzluktan kaynaklanan, dergiler ve gazeteler tarafından beslenen ve politikacılar tarafından sahiplenilen bir tür dış baskı ya da tehdit karşısında oluşturulur.
Bir Programın Çalıştığını Gösteren Matematiksel Bir İspat
Matematiksel bir ispat, teknik olarak, programların doğruluğunu güvence altına almanın tamamen güvenilir bir yoludur; ancak bu yöntem, uygun tutumlar ve yönetsel tekniklerle birlikte kullanılmadıkça pratikte asla etkili olamaz. Bu teknikler aslında geçmişte başarıyla kullanılmış olan fikirlerin aynısına dayanmaktadır.
Programlamadaki hataları anında ölümle cezalandırmak pratik değildir ve arzu edilir de değildir. Buna rağmen, programcılar hatayı günlük yaşamlarının kaçınılmaz bir özelliği olarak görmeyi bırakmalıdır. Cerrahlar ya da hava yolu pilotları gibi, hatayı ortadan kaldıran teknikleri benimseme konusunda kişisel bir bağlılık hissetmeli ve başarısız olduklarında uygun utancı ve gelişme kararlılığını duymalıdırlar.
Güvenlik açısından kritik bir projede, her başarısızlık tarafsız bir soruşturmayla incelenmeli; sorumlu programcıyı adlandırma ve o kişiye güvenlik açısından kritik işlerde daha fazla çalışma yasağı koyma yetkisine sahip olunmalıdır. Kanıtlanmış ihmal durumlarında, cezai yaptırımlar göz ardı edilmemelidir.
Diğer mühendislik disiplinlerinde bu önlemler, kişisel ve mesleki sorumlulukta ve kamu güvenliğinde belirgin iyileşmelere yol açmıştır. Programcılara daha fazla dokunulmazlık tanınması için hiçbir neden yoktur.
Matematiksel hesaplamalar ve ispatlar, birçok yönden programlara çok benzer. Bunlar, en küçük bir hatanın geçersizliğe yol açtığı uzun ve karmaşık metinlerdir. İlke olarak, bir programcı tamamen biçimsel ispatlar yazmayı öğrenebilir ve bir bilgisayar bu ispatları denetleyecek şekilde programlanabilir. Bu ilke, bazı mükemmel araştırmalara ve ispat denetleme programlarının geliştirilmesine ilham vermiştir. Ancak, makinelerin denetleyebilmesi için yeterli biçimsellikle ispatlar kurmanın emeği aşırı derecede fazla çıkmıştır.
Matematiksel Bir İspatın Denetlenmesi
Şimdilik, ispatları denetlemenin en etkili yöntemi, onları başka bir programcının ya da matematikçinin incelemesine sunmaktır. Denetleyici, programın doğruluğu konusunda sorumluluğu programcıyla paylaşır. Bir mühendisin çalışmasının, daha deneyimli ve yetkin başka bir mühendis tarafından incelenip onaylanması gerektiği ilkesi, mühendisliğin tüm dallarındaki güvenli çalışma uygulamaları kodlarının merkezinde yer alır.
İspatların denetlenmesi, kodun gözle incelenmesiyle birçok ortak noktaya sahiptir; ancak ilke olarak daha etkilidir, çünkü iyi sunulmuş bir ispattaki bir boşluğu tespit etmek, bir programdaki bir ihmali bulmaktan daha kolaydır. Bunun nedeni, bir ispat denetleyicisinin yalnızca ispatın her satırının geçerliliğini, onu yalnızca bir ya da iki önceki satırla karşılaştırarak denetlemesinin yeterli olmasıdır. Bir programda ise denetleyici, her satırı programdaki diğer tüm kod satırlarının bağlamı içinde denetlemek zorundadır — bu görev büyük programlar için tamamen imkânsızdır.
Test Etme
Bir mühendis bir ürünü ne kadar dikkatle belirtmiş, tasarlamış ve uygulamış olursa olsun, ürünü mümkün olduğunca gerçekçi ve kapsamlı testlere tabi tutmadan hizmete sokmak son derece akılsızca olur. Bu tür testler, özgün belirtimin yeterliliğini ve onun dayandığı genel varsayımları denetlemek için gereklidir. Donanım, yazılım ve çalışma ortamları arasındaki ilişkileri anladığımızdan emin olmak için bu testlere ihtiyaç duyarız. Bu tür değerlendirmeler, sistemin belirtilme, tasarlanma ve inşa edilme yöntemlerinin yeterliliğini de denetler.
Tüm testlerin büyük çoğunluğu başarılı olmalıdır — aksi takdirde üründe o kadar ciddi bir sorun vardır ki, onu atmak en iyisi olur. Ancak kaçınılmaz olarak, doğru olduğu kanıtlandığı düşünülen programlarda bile ara sıra bir başarısızlık olacaktır. Bu durumlarda doğru tepki, önce hatanın nedenini bulmaktır: örneğin dikkatsizlik, yanlış anlama ya da yetersiz yöntemlerin kullanımı. İkinci olarak, aynı nedenin programın diğer bölümlerinde başka hatalara yol açmış olup olmadığını değerlendirmelisiniz. Bu tür tüm şüpheli alanlar yeniden denetlenmelidir. Ancak bundan sonra tespit edilen hata düzeltilmeli ve düzeltmenin kendisi, yeni hatalar getirme olasılığına karşı daha da sıkı denetimlerden geçirilmelidir. Bu sağduyulu ilkeler mühendisliğin birçok dalında standart uygulamalardır; yine de programlamaya uygulanmaları yavaş kabul görmüştür.
Makine Dili Testi
Günümüzde bilgisayar programlarının çoğu, çalıştırılmadan önce makinenin diline çevrilmesi gereken yüksek seviyeli programlama dillerinde yazılmaktadır. Bu çeviriyi yapan programın kendisi büyük, karmaşık ve hataya açıktır. Bu durum, güvenlik açısından kritik programlama için yüksek seviyeli dillerin kullanımını engellemiştir. Bu bir hatadır. Basit yüksek seviyeli diller için bazı derleyiciler, yaygın kullanımda güvenilir olduklarını kanıtlamıştır ve belirli bir güvenlik açısından kritik programı derlerken hata yapma olasılıkları çok küçüktür. Böyle bir hatanın rutin testlerde fark edilmeden kalma olasılığı ise daha da küçüktür. En son çare olarak, makine kodunun özgün yüksek seviyeli programla görsel olarak karşılaştırılması hâlâ mümkündür — özgün programı yazmaktan daha kolay ve daha güvenlidir.
Çeşitlilik ilkesi, programların güvenilirliğini artırmada temeldir. İspatları denetleyen kişiler, onları kuranlardan bağımsız olmalıdır. Test düzenlerini tasarlayanlar, test edilen nesneleri tasarlayanlardan bağımsız olmalıdır.
Son olarak, en yüksek güven için, tercihen farklı ispat yöntemleri kullanılarak yapılmış iki bağımsız ispata sahip olmak ideal olurdu. Fiziğin yasaları bağımsız deneylerle doğrulanır; matematikçiler bile birden fazla kez kanıtlanmış temel teoremlerle daha rahat hissederler.
İspata uygulandığında çeşitlilik ilkesi, programlara uygulandığındakinden daha etkili olacak ve muhtemelen daha pahalı olmayacaktır. Yazılım hatalarına karşı bir koruma olarak donanım hata denetimlerinin kullanımından doğan hiçbir sorun ya da tehlikeyi barındırmaz.
Programlamanın Matematiksel Yönleri
Matematik, programcılar arasında da genel nüfusta olduğu gibi, geleneksel olarak sevilmeyen bir derstir. Saf ve uygulamalı matematik alanında üniversite derecesine sahip programcılar bile, matematiksel becerilerini mesleklerinin pratiğine nasıl uygulayacaklarını bilmezler. Neyse ki programlamanın matematiksel yönleri artık üniversite müfredatlarında yer bulmaya başlamıştır. Bu konuların ortaöğretimde uzmanlaşmış öğretime de gireceği günü sabırsızlıkla bekliyorum. Öngörüm şudur ki, programlamanın matematiksel incelemesi, matematiğin daha geniş ölçekte takdir edilmesine, anlaşılmasına ve sevilmesine katkıda bulunacaktır; çünkü matematik, yeni uygulamaların keşfiyle sürekli olarak yenilenir. O zamana kadar, güvenlik açısından kritik programlamada matematiğin profesyonel kullanımı, bilgisayar programlarının içinde yer aldıkları herhangi bir sistemin en güvenilir bileşeni olmasını sağlayacaktır.
Programlamanın Güvenilirliği
Bu arzu edilen hedefe ulaşmak için, hâlihazırda önerilen ve kullanımda olan bazı yöntemlerin yetersizliği konusunda kamuoyunu açıkça uyarmanın gerekli olduğuna inanıyorum. Ancak riski abartmamak ya da aşırı tepkiyi kışkırtmamak önemlidir. Bilgisayar programları tarafından denetlenen kritik süreçler, büyük olasılıkla daha eski analog aygıtlar tarafından denetlenenlerden çok daha güvenilirdir ve kuşkusuz elle yürütülen yöntemlerden de daha güvenilirdir. Bu durum esas olarak bilgisayar donanımının güvenilirliğindeki büyük artıştan kaynaklanmaktadır. Nitekim günümüzde, programlamadaki hatalara duyulan korku, güvenlik açısından kritik uygulamalarda bilgisayarlı denetimin devreye alınmasındaki gecikmenin başlıca nedenidir. Bu gecikmenin kendisi kamu güvenliği açısından bir risk oluşturmaktadır. Programların doğruluğunu kanıtlamak için matematiksel yöntemlerin devreye sokulması bu nedenle çifte yarar sağlayacaktır — mevcut uygulamaların güvenilirliğini artıracak ve insanlara bu yararları yeni uygulamalara da yayma konusunda güven verecektir.
Kaynaklar
Roland C. Backhouse, "Program Construction and Verification," Prentice Hall (1986). Program geliştirme ve kanıtlama için önermesel yöntemlere giriş niteliğinde bir metin. Bu yöntemler, güvenlik açısından kritik programlar için titizlik ve doğruluk konusunda bir standart oluşturur.
"Software, Vital Key to UK Competitiveness," ACARD Raporu, HMSO, 1986, £6.00. Bu rapor, her amaç için yazılım geliştirilmesinde iyileştirilmiş yöntemlerin önemini vurgular. Güvenlik açısından kritik programlar için devreye alınan matematiksel yöntemlerin, tüm yazılım endüstrisi genelinde iyileştirmeler sağlayacağını öne sürer.
18 Eylül 1986 tarihli New Scientist dergisinde (No. 1526) yayımlanan bir makaleye dayanmaktadır; telif hakkı IPC Magazines Ltd., 205 East 42nd St., New York, NY 10017. İzin alınarak yeniden basılmıştır.