FPFM: A Formal Specification and Verification Framework for Security Policies in Multi-Domain Mobile Networks
Summary:
We present a framework called Formal Policy Framework for Mobility (FPFM) for the specification and verification of domain and inter-domain security policies in a multi-domain mobile network environment. FPFM supports the specification of security policies with mobility and location constraints, role hierarchy mapping, interdomain services, inter-domain access rights and separation of duty. The specification of security olicies in FPFM is based on a formal security policy model, called FPM-RBAC (Formal Policy Model for Mobility with Role Based Access Control) and a XML based security policy specification language called XFPM-RBAC (XML Based Formal Policy Language for Mobility with Role Based Access Control). Formal verification of security policies ensure that the security policy is satisfied by the network elements in a given network configuration. FPFM supports extraction of formal specifications from defined network configurations, domain and inter-domain security policies. Another novel aspect of FPFM is the support for formal information flow analysis related to mobility within multiple security domains. Automated verification of formal specifications are carried out through model checking and theorem proving. A spatio-temporal model checking algorithm has been proposed and a model checking tool has been developed for spatio-temporal model checking of location and mobility constraints in security policy rules. Conflicts within security policy rules are resolved through theorem proving with the help of the Coq interactive theorem prover.
Özet:
Çok etki alanlı ağlarda gezgin bilgisayarların, kaynakların ve kullanıcıların hareketliliği güvenlik açısından zorluklar meydana getirmektedir. Güvenlik etki alanları arasında hareketlilik içeren eylemler, etki alanında ve etki alanları arasında oluşturulmuş güvenlik politikaları 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ı gezgin ağlarda kullanıma yönelik, bir güvenlik politikası betimleme ve doğrulama çerçevesi ortaya 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üvenlik politikaları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 kapsamda tanı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'in katkı sağladığı alanlardan bir başkası, birden fazla etki alanı içerisindeki gezginlik kaynaklı 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üvenlik politikaları içerisindeki konum ve hareketlilik kısıtlarının uzay-zaman tabanlı model denetlemesi için bir uzay-zaman tabanlı algoritma önerilmiş ve bir model denetleme aracı geliştirilmiştir. Coq etkileşimli teorem doğrulama aracı kullanılarak güvenlik politikaları içerisindeki çelişkilerin çözümlenmesi sağlanmıştır.