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
- Tez No: 297863
- Danışmanlar: PROF. DR. MEHMET UFUK ÇAĞLAYAN
- Tez Türü: Doktora
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
- Anahtar Kelimeler: Bilgi güvenliği, Bilgisayar ağları güvenliği, Formel dil, Formel doğrulama, Güvenlik politikaları, Güvenlik yönetimi, Model doğrulama, Teorem ispatlama, Information security, Computer networks security, Formal language, Formal verification, Security policies, Security management, Model check, Theorem proving
- Yıl: 2011
- Dil: İngilizce
- Üniversite: Boğaziçi Üniversitesi
- Enstitü: Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Bilgisayar Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: Belirtilmemiş.
Özet
Çok etki alanlı ağlarda gezgin bilgisayarların, kaynakların ve kullanıcıların hareketliliğigüvenlik açısından zorluklar meydana getirmektedir. Güvenlik etki alanları arasındahareketlilik içeren eylemler, etki alanında ve etki alanları arasında oluşturulmuş güvenlikpolitikaları bağlamında betimlenmeli ve doğrulanmalıdır. Bu tez kapsamında,FPFM (Gezginlik için Formal Güvenlik Politikası Çerçevesi) adında, çok etki alanlı gezginağlarda kullanıma yönelik, bir güvenlik politikası betimleme ve doğrulama çerçevesiortaya konulmaktadır. FPFM, gezginlik ve konum kısıtları, rol hiyerarşileri eşleştirme,etki alanları arası servisler, etki alanları arası erişim hakları ve görevlerin ayrımı unsurlarınıiçeren güvenlik politikalarının betimlenmesini desteklemektedir. Güvenlikpolitikalarının betimlenmesi için FPM-RBAC adı verilen bir formal güvenlik politikasımodeli ve XFPM-RBAC adı verilen XML tabanlı bir güvenlik politikası diliönerilmektedir. Güvenlik politikalarının doğrulanması, belirli bir ağ yapılandırmasıiçerisinde, güvenlik politikalarının sağlandığının onaylanmasını sağlar. FPFM bu kapsamdatanımlı ağ yapılandırması, etki alanı güvenlik politikası ve etki alanları arasıgüvenlik politikasından formal betimlemelerin üretilmesini sağlamaktadır. FPFM'inkatkı sağladığı alanlardan bir başkası, birden fazla etki alanı içerisindeki gezginlikkaynaklı bilgi akışlarının formal analizidir. Formal betimlemelerin otomatik doğrulanmasıiçin model denetleme ve teorem ispatlama yöntemleri kullanılmaktadır. Güvenlikpolitikaları içerisindeki konum ve hareketlilik kısıtlarının uzay-zaman tabanlı modeldenetlemesi için bir uzay-zaman tabanlı algoritma önerilmiş ve bir model denetlemearacı geliştirilmiştir. Coq etkileşimli teorem doğrulama aracı kullanılarak güvenlikpolitikaları içerisindeki çelişkilerin çözümlenmesi sağlanmıştır.
Özet (Çeviri)
We present a framework called Formal Policy Framework for Mobility (FPFM)for the specification and verification of domain and inter-domain security policies ina multi-domain mobile network environment. FPFM supports the specification ofsecurity policies with mobility and location constraints, role hierarchy mapping, interdomainservices, inter-domain access rights and separation of duty. The specification of securityolicies in FPFM is based on a formal security policy model, called FPM-RBAC (Formal PolicyModel for Mobility with Role Based Access Control) and a XML based security policyspecification language called XFPM-RBAC (XML Based FormalPolicy Language for Mobility with Role Based Access Control). Formal verification ofsecurity policies ensure that the security policy is satisfied by the network elements in agiven network configuration. FPFM supports extraction of formal specifications fromdefined network configurations, domain and inter-domain security policies. Anothernovel aspect of FPFM is the support for formal information flow analysis related tomobility within multiple security domains. Automated verification of formal specificationsare carried out through model checking and theorem proving. A spatio-temporalmodel checking algorithm has been proposed and a model checking tool has beendeveloped for spatio-temporal model checking of location and mobility constraints insecurity policy rules. Conflicts within security policy rules are resolved through theoremproving with the help of the Coq interactive theorem prover.
Benzer Tezler
- Global optimizasyon metodu kullanılarak bir doğru akım motorunun hız konrolunun gerçekleştirilmesi
Speed control of a DC motor with global optimization method
OGÜN TIĞLI
Yüksek Lisans
Türkçe
1990
Elektrik ve Elektronik Mühendisliğiİstanbul Teknik ÜniversitesiDOÇ.DR. İBRAHİM EKSİN
- Farklı periferal sinir anastomoz tekniklerinin sinir rejenerasyonu yönünden karşılaştırılmalı araştırılması
Comparative investigation of different peripheral nerve anastomosis techniques for nerve regeneration
HİLAL ACAR
Doktora
Türkçe
2023
NöroşirürjiBursa Uludağ ÜniversitesiVeterinerlik Cerrahisi Ana Bilim Dalı
PROF. DR. HAKAN SALCI
- Gestasyonel diabetik plasentalarda, PI3K p85/p110 alfa ve glukoz transport proteinleri korelasyonu
Correlation of PI3K p85/p110 alpha and glucose transport proteins in gestational diabetes
SELMA AYDEMİR
Yüksek Lisans
Türkçe
2019
Histoloji ve EmbriyolojiDokuz Eylül ÜniversitesiHistoloji ve Embriyoloji Ana Bilim Dalı
DOÇ. DR. BAŞAK BAYKARA
- Global optimizasyon yöntemi ile asenkron motor hız kontrolu
Speed control of an induction machine using with new global optimization method
MURAT ATA DEMİRÖZ
Yüksek Lisans
Türkçe
1992
Elektrik ve Elektronik Mühendisliğiİstanbul Teknik ÜniversitesiDOÇ. DR. İBRAHİM EKSİN
