Specification and verification of confidentialitiy in software architectures
Yazılım mimarilerinde gizlilik bildirimi ve doğrulanması
- Tez No: 153414
- Danışmanlar: YRD. DOÇ. DR. HALİT OĞUZTÜZÜN
- Tez Türü: Doktora
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
- Anahtar Kelimeler: Örgü-temelli erişim denetimi, veri akışı, gizlilik, yazılım mimarisi, mimari tanımlama dili, yetki, Lattice-based access control, data flow, confidentiality, software architecture, architecture description language, privilege. IV
- Yıl: 2004
- Dil: İngilizce
- Üniversite: Orta Doğu Teknik Üniversitesi
- Enstitü: Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Bilgisayar Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: 262
Özet
Öz YAZILIM MİMARİLERİNDE GİZLİLİK BELİRTİMİ VE DOĞRULAMASI ULU, Cemil Doktora, Bilgisayar Mühendisliği Bölümü Tez Yöneticisi : Yrd. Doç. Dr. Halit OĞUZTÜZÜN Mart 2004, 247 sayfa Bu çalışma bilgi güvenlik probleminin gizlilikle ilgili yönüne yazılım mimarisi bakış açısından hitap etmektedir. Güvenli bir sistem tasarımı için istenen güvenlik niteliklerinin, özellikle bilgi gizliliği, mimari seviyede taşındığının kanıtlandığı yeni bir yaklaşım önerilmektedir. Wright Mimari Tanım Diline (ADL- Architecture Description Language) gizlilik yetkilerinin belirtilebileceği şekilde genişlemeler yapılmıştır. Genişletilmiş dil olan Wright/c'deki bir mimari tanım, bileşenlerin arayüz yapılarına yetki tahsisi yapmakta ve güvenlik etiketlerim veri tipi bilgisinin bir parçası olarak ele almaktadır. Güvenlik etiketleri, yetki tahsisleri ile birlikte, Wright/c'de ifade edilen erişim denetimi örgü modelinde deklare edilmektedir. Bu yaklaşım, Bell-LaPadula prensiplerinin gizlilik gereksinimlerine bağlı kalarak, veri akışının bir yazılım mimarisi üzerinde statik olarak analizine imkan tanımaktadır. Wright/c tanımı ve örgü modelini input olarak alan bir algoritma, Bell-LaPadula prensiplerine karşı potansiyel bir uyumsuzluk olupolmadığını kontrol etmektedir. Algoritma ayrıca yetki fazlalıklarım da ortaya çıkarmaktadır. Ek olarak, algoritma için XML tabanlı ön işlemci kullanan bir yazılım aracı geliştirilmiştir. Çalışmanın son bölümünde ise algoritmanın doğruluk, tamlık ve ölçümsel karmaşıklık açısından analizi yapılmıştır.
Özet (Çeviri)
ABSTRACT SPECIFICATION AND VERIFICATION OF CONFIDENTIALITY IN SOFTWARE ARCHITECTURES ULU, Cemil Ph.D., Department of Computer Engineering Supervisor: Assist. Prof. Dr. Halit O?UZTÜZÜN March 2004, 247 pages This dissertation addresses the confidentiality aspect of the information security problem from the viewpoint of the software architecture. It presents a new approach to secure system design in which the desired security properties, in particular, confidentiality, of the system are proven to hold at the architectural level. The architecture description language Wright is extended so that confidentiality authorizations can be specified. An architectural description in Wright/c, the extended language, assigns clearance to the ports of the components and treats security labels as a part of data type information. The security labels are declared along with clearance assignments in an access control lattice model, also expressed in Wright/c. This enables the static analysis of data flow over the architecture subject to confidentiality requirements as per Bell-LaPadula principles. An algorithm takes the Wright/c description and the lattice model as inputs, and checks if there is a potential violation of the Bell-LaPadula principles. mThe algorithm also detects excess privileges. A software tool, which features an XML-based front-end to the algorithm is constructed. Finally, the algorithm is analyzed for its soundness, completeness and computational complexity.
Benzer Tezler
- Specification and verification of ISDN layer 2 using SDL 92
ISDN ikinci katmanının SDL 92 kullanılarak belirtimi ve geçerlilik sınaması
DOĞUŞ ÇENBERCİ
Yüksek Lisans
İngilizce
1997
Elektrik ve Elektronik MühendisliğiOrta Doğu Teknik ÜniversitesiElektrik-Elektronik Mühendisliği Ana Bilim Dalı
PROF. DR. KEMAL İNAN
- Specification and verification of the xpress transport protocol (XTJ)using SDL 92
Xpress taşıyıcı protokolünün S94 92 kullanılarak belirtimi ve geçerlilik sınaması
İSMAİL DALKIRAN
Yüksek Lisans
İngilizce
1997
Elektrik ve Elektronik MühendisliğiOrta Doğu Teknik ÜniversitesiElektrik-Elektronik Mühendisliği Ana Bilim Dalı
PROF. DR. KEMAL İNAN
- Model checking of ambient calculus specifications against ambient logic formulas
Çevrel cebir tanımlamalarının çevrel mantık formülleri ile model denetlemesi
OZAN AKAR
Yüksek Lisans
İngilizce
2009
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolBoğaziçi ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
PROF. DR. MEHMET UFUK ÇAĞLAYAN
- FPFM: A formal specification and verification framework for security policies in multi-domain mobile networks
FPFM: Çok etki alanlı gezgin ağlarda güvenlik politikaları betimleme ve doğrulama çerçevesi
DEVRİM ÜNAL
Doktora
İngilizce
2011
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolBoğaziçi ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
PROF. DR. MEHMET UFUK ÇAĞLAYAN
- Fırın enerji tüketiminin iyileştirilmesi için simülasyon programının geliştirilmesi ve doğrulanması
Improvement of simulation program for high efficiency of domestic oven energy consumption and verification of simulation program
AZİZ ÇELİK
Yüksek Lisans
Türkçe
2015
Makine Mühendisliğiİstanbul Teknik ÜniversitesiMakine Mühendisliği Ana Bilim Dalı
PROF. DR. SEYHAN ONBAŞIOĞLU