Abstract :BT ürünlerinin güvenlik özellikleri firmaların en önemli satın alma kriterlerinden birisidir. Eğer BT ürünü, ilgili özellikler için bir güvenlik sertifikasına sahipse firmanın satın alma kararı vermesi daha kolaydır. Ortak Kriterler (ISO/IEC 15408), BT ürünlerinin güvenlik incelemesi ve sertifikasyonu için iyi bilinen uluslararası bir standarttır. Ortak Kriterler’in Türkiye dahil on yedi ülkede sertifika yetkili üyesi bulunmaktadır. BT ürünleri, bu ülkelerde, lisanslı bağımsız laboratuvarlarda, seçilen güvenlik özellikleri için incelenmekte ve sertifikalandırılmaktadır. Ortak Kriterler’de yedi farklı sertifika teminat seviyesi (EAL) vardır. EAL 7, güvenlik incelemesi için formel metotları kullanmaktadır ve bu nedenle ulaşması en zor olan teminat seviyesidir. Bu bildiride, Ortak Kriterler sertifikasyonu için hazırlık ve inceleme süreçlerini kolaylaştıracak bir yöntem önermekteyiz. Bu yeni yöntemde, BT ürününün işlevsel özellikler tasarımı ve güvenlik poliçelerinin modellenmesi için UML ve OCL kullanılmaktadır. Daha sonra, bu güvenlik poliçelerinin BT ürününün tasarım modeli üzerinde SPIN aracı kullanılarak formel olarak doğrulanması sağlanmaktadır. Keywords : Güvenli Yazılım Tasarımı, Güvenlik, Ortak Kriterler, BT Güvenliği, Güvenlik Açıkları, Güvenlik Tehditleri, UML, OCL, Güvenlik Sertifikaları, Biçimsel Yöntemler
