Model Driven Security Framework for Software Design and Verification
Summary:
Information system security is receiving increasing attention every day because a security problem can cause serious financial loss or even loss of lives. Some of these security problems occur as a result of poor design practices, where important security functionality is not designed properly and is directly implemented later in the development cycle in an unmethodical way. Researchers have put a great deal of effort into defining processes and tools to design and develop more secure information systems. However, verification of the designed and developed security functionality is of utmost importance. In some cases, designs and codes also need to be formally or semi-formally verified and certified by authorities. The Common Criteria is one of the widely used universal frameworks for evaluating the security functionality of information systems. In this thesis, we propose a new framework, Model Driven Security Framework (MDSF), for the analysis, design and evaluation of security properties of the information systems. Our aim is to support information system developers and evaluation authorities who implement the higher-level Common Criteria (Levels 6 and 7) security assurance process using formal methods based on Unified Modelling Language (UML), Object Constraint Language (OCL), Promela and Spin. With MDSF, we extend UML to support security analysis and design on the UML models of the information system. In addition to UML, we use OCL in MDSF for threat identification, consistency checking among diagrams and security policy enforcement in the design model. We also propose a model transformation and model checking approach to formally verify whether the design model satisfies the security requirements listed in the analysis model.
Özet:
Uygulama ve sistemlerdeki güvenlik problemleri bilgi kaybına, finansal kayıplara ve hatta insan yaşamının kaybına varabilecek kadar ciddi sonuçlar doğurmaktadır. Bu nedenle bilgi sistemleri güvenliği her geçen gün daha fazla dikkat çekmektedir. Bu güvenlik problemlerinin büyük bir kısmı, güvenlik fonksiyonlarının tasarım aşamasında düşünülmemesinden ve geliştirme aşamasında doğrudan yazılıma eklenmesinden kaynaklanmaktadır. Halbuki, güvenlik fonksiyonlarının analizi, tasarımı ve doğrulanması çok yüksek önem derecesine sahiptir. Hatta bazı durumlarda, yazılım tasarımlarının ve kodlarının formel veya yarı-formel olarak doğrulanması ve yetkili otoritelerce sertifikalandırılması beklenmektedir. Bilgi sistemlerinin güvenlik fonksiyonlarının değerlendirilmesi için sıklıkla kullanılan standartlardan birisi Ortak Kriterler'dir. Bu tez çalışmasında, bilgi sistemlerinin güvenlik özelliklerinin analizi, tasarımı ve değerlendirmesi için yeni bir çerçeve olarak Model Güdümlü Güvenlik Çerçevesi'ni (MDSF) önermekteyiz. Amacımız, bilgi sistemleri geliştiren kişileri ve üst seviye Ortak Kriterler sertifikasyonu (EAL 6 ve EAL 7) için değerlendirme yapan yetkilileri, hazırlık ve inceleme süreçlerinde Unified Modelling Language (UML), Object Constraint Language (OCL), Promela ve Spin dil ve araçlarını kullanarak desteklemektir. MDSF ile, IT ürününün UML modeli üzerinden, güvenlik analizi ve tasarımı yapılabilmesini desteklemek amacıyla, UML diline yeni bir profil önermekteyiz. UML'e ek olarak, güvenlik tehditlerinin belirlenmesi, farklı model seviyeleri üzerinde uyumluluk kontrolü ve IT ürününün UML tasarım modeli üzerinde güvenlik poliçelerinin doğrulanması amacıyla OCL'in kullanılabileceğini göstermekteyiz. Ayrıca, tasarım modelinin, güvenlik ihtiyaçlarını karşılayıp karşılamadığını formel olarak göstermek amacı ile model dönüştürme ve model doğrulama tekniklerini UML, OCL ve PROMELA üzerinde kullanmaktayız.