Geri Dön

Specification and verification of confidentialitiy in software architectures

Yazılım mimarilerinde gizlilik bildirimi ve doğrulanması

  1. Tez No: 153414
  2. Yazar: CEMİL ULU
  3. Danışmanlar: YRD. DOÇ. DR. HALİT OĞUZTÜZÜN
  4. Tez Türü: Doktora
  5. Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
  6. 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
  7. Yıl: 2004
  8. Dil: İngilizce
  9. Üniversite: Orta Doğu Teknik Üniversitesi
  10. Enstitü: Fen Bilimleri Enstitüsü
  11. Ana Bilim Dalı: Bilgisayar Mühendisliği Ana Bilim Dalı
  12. Bilim Dalı: Belirtilmemiş.
  13. 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

  1. 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

    İngilizce

    1997

    Elektrik ve Elektronik MühendisliğiOrta Doğu Teknik Üniversitesi

    Elektrik-Elektronik Mühendisliği Ana Bilim Dalı

    PROF. DR. KEMAL İNAN

  2. 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

    İngilizce

    1997

    Elektrik ve Elektronik MühendisliğiOrta Doğu Teknik Üniversitesi

    Elektrik-Elektronik Mühendisliği Ana Bilim Dalı

    PROF. DR. KEMAL İNAN

  3. 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

    İngilizce

    2009

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolBoğaziçi Üniversitesi

    Bilgisayar Mühendisliği Ana Bilim Dalı

    PROF. DR. MEHMET UFUK ÇAĞLAYAN

  4. 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

    İngilizce

    2011

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolBoğaziçi Üniversitesi

    Bilgisayar Mühendisliği Ana Bilim Dalı

    PROF. DR. MEHMET UFUK ÇAĞLAYAN

  5. 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

    Türkçe

    2015

    Makine Mühendisliğiİstanbul Teknik Üniversitesi

    Makine Mühendisliği Ana Bilim Dalı

    PROF. DR. SEYHAN ONBAŞIOĞLU