مدلبندی و رسمی سازی الگوهای امنیتی و توسعه الگو-محور سیستم های نرم افزارزی ایمن
چکیده
با رسیدگی به چالش‌های جدیدی از قبیل امنیت و قابلیت اطمینان، توسعه الگو-محور سیستم‌های نرم‌افزاری به تازگی توجه بیشتری را جلب کرده است. با این حال، هنوز شکاف‌هایی در فرمالیسم‌ها و/یا زبان‌های مدلبندی موجود در رابطه با مدلبندی الگوهای طراحی و نحوه استفاده مجدد از آن‌ها در اتوماسیون توسعه نرم‌افزاری وجود دارند. راه‌حل در نظر گرفته شده در اینجا بر اساس ترکیب تکنیکهای متا-مدلبندی و روش‌های رسمی برای نمایش الگوهای امنیتی در دو سطح انتزاع برای تقویت استفاده مجدد است. هدف این مقاله، ایجاد پیشرفت در امنیت مبتنی بر الگو و مدل برای مهندسی نرم‌افزارها و سیستم‌ها در تعریف الگوهای امنیتی با استفاده از تکنیکهای متامدلبندی در سه حوزه‌های مربوطه است: ۱) توسعه یک زبان مدلبندی برای پشتیبانی از تعریف الگوهای امنیتی با استفاده از تکنیکهای متامدلبندی؛ ۲) فراهم ساختن یک نمایش رسمی و مکانیسم‌های معتبرسازی مربوطه آن برای تایید ویژگی‌های امنیتی؛ و ۳) به دست آوردن مجموعه‌ای از دستوالعمل‌ها برای مدلبندی الگوهای ساختاری در محدوده یکپارچه‌سازی این دو نوع نمایش.
۱. پیشگفتار
۱.۱. انگیزه و پیش زمینه
در طول دهه‌های گذشته، سیستم‌ها از نظر پیچیدگی و اتصال رشد کرده‌اند. در گذشته، امنیت، دغدغه‌ای بدین مهمی برای تیم‌های توسعه سیستم نبود، زیرا احتمالا بر این حقیقت تکیه داشت که یک سیستم را می‌توان به سادگی به دلیل اتصال محدود آن و در اکثر موارد، تمرکز اختصاصی آن، کنترل کرد. با این حال، امروزه سیستم‌ها در زمینه پیچیدگی، کارکردپذیری و اتصال در حال رشد هستند. چالش‌های ذکر شده در بالا در توسعه سیستم مدرن، جامعه تکنیکهای اطلاعات و ارتباطات (ICT) را در جهت جستجوی روش‌ها و ابزارهای نوآورانه برای خدمت به این نیازها و اهداف جدید هدایت کرده‌اند. صرف نظر از امنیت سیستم، در مورد سیستم‌های مدرن، پارادایم «باغ محصور» نامناسب است و مفاهیم سنتی امنیت، ناکارامد هستند زیرا بر اساس این حقیقت هستند که امکان ایجاد یک دیواره (حصار) بین سیستم و جهان بیرونی وجود دارد.
۹. نتیجه‌گیری
توسعه دهندگان برنامه کاربردی معمولا دارای تخصص در امنیت و قابلیت اطمینات نیستند. از اینرو، کسب و فراهم ساختن این تخصص توسط الگوهای امنیتی تبدیل به حوزه پژوهشی در سال‌های اخیر شده است. الگوهای امنیتی، توسعه برنامه‌های کاربردی ایمن و قابل اطمینان را ممکن می‌سازند و در عین حال به طور همزمان، توسعه دهنده را از نیاز به پردازش جزئیا فنی رها می‌کنند. مهندسی مدل محور (MDE)، کمک بسیار مفیدی را برای طراحی سیستم‌های ایمن و قابل اطمینان فراهم می‌سازد، زیرا شکاف بین مسائل طراحی و دغدغه‌های پیاده‌سازی را پر می‌کند. از این رو، ادغام الگوی امنیتی باید در نقطه‌ای در فرایند MDE در نظر گرفته شود.
در این مقاله، ما رویکردی را برای مدلبندی و معتبرسازی الگوی امنیتی ارائه داده‌ایم که از پارادایم MDE پیروی می‌کند. رویکرد ما بر اساس تکنیکهای متامدلبندی است که امکان مشخص کردن و معتبرسازی الگوهای امنیتی را در سطوح مختلف انتزاع فراهم می‌سازند. یک الگوی امنیتی در سطح مستقل از دامنه، توسعه دهنده برنامه کاربردی را قادر به شناسایی الزامات امنیتی و انتخاب راه‌حل انتزاعی مربوطه بدون دانش ویژه در مورد نحوه طراحی و پیاده‌سازی راه‌حل می‌سازد. بنابراین، یک الگوی DIPM را می‌توان به سادگی در مشخصات سیستم انتزاعی کلی ادغام کرد. با پیروی از فرایند MDE، مدل سیستم سپس در جهت یک سطح خاص دامنه با در نظر گرفتن مصنوعات دامنه، عناصر واقعی از قبیل مکانیسم‌های مورد استفاده، دستگاه‌های قابل دسترس و غیره اصلاح می‌شود. در نتیجه، الگوی امنیتی در سطح خاص دامنه شامل اطلاعات مربوطه است.
Abstract
Pattern-based development of software systems has gained more attention recently by addressing new challenges such as security and dependability. However, there are still gaps in existing modeling languages and/or formalisms dedicated to modeling design patterns and the way how to reuse them in the automation of software development. The solution envisaged here is based on combining metamodeling techniques and formal methods to represent security patterns at two levels of abstraction to fostering reuse. The goal of the paper is to advance the state of the art in model and pattern-based security for software and systems engineering in three relevant areas: (1) develop a modeling language to support the definition of security patterns using metamodeling techniques; (2) provide a formal representation and its associated validation mechanisms for the verification of security properties; and (3) derive a set of guidelines for the modeling of security patterns within the integration of these two kinds of representations.
1 Introduction
1.1 Motivation and background
During the last decades, the systems have grown in terms of complexity and connectivity. In the past security was not such a critical concern of system development teams, since it was possible to rely on the fact that a system could be easily controlled due to its limited connectivity and, in most of the cases, its dedicated focus. However, nowadays, systems are growing in terms of complexity, functionality and connectivity. The aforementioned challenges in modern system development push the Information and Communication Technologies (ICT) community to search for innovative methods and tools for serving these new needs and objectives. Regarding system security, in the cases of modern systems, the “walled-garden” paradigm is unsuitable and the traditional security concepts are ineffective, since they are based on the fact that it is possible to build a wall between the system and the outer world.
9 Conclusion
Application developers usually do not have expertise in security and dependability. Hence capturing and providing this expertise by way of security patterns has become an area of research in the last years. Security patterns shall enable the development of secure and dependable applications while at the same time liberating the developer from having to deal with the technical details. Model-driven engineering (MDE) provides a very useful contribution for the design of secure and trusted systems, since it bridges the gap between design issues and implementation concerns. Hence Security pattern integration has to be considered at some point in the MDE process.
In this paper, we have proposed an approach for security pattern modeling and validation that follows the MDE paradigm. Our approach is based on metamodeling techniques that allow to specify and validate security patterns at different levels of abstraction. A security pattern at domain-independent level allows the application developer to identify security requirements and select a respective abstract solution without specific knowledge on how the solution is designed and implemented. Thus a DIPM pattern can easily be integrated into the overall abstract system specification. Following the MDE process, the system model is then refined towards a domain-specific level, taking into account domain artifacts, concrete elements such as mechanisms to use, devices that are available, etc. Consequently, a security pattern at domain-specific level contains the respective information.
عکس
چکیده
۱. پیشگفتار
۱.۱. انگیزه و پیش زمینه
۱.۲. نقش مورد نظر
۱.۳. سازماندهی نقش
۲. کارهای مربوطه
۲.۱. رویکرد مدلبندی الگو – انتزاع
۲.۲. ترکیب و کاربرد الگو
۲.۳. مهندسی امنیتی مدل-محور
۲.۴. روش‌ها رسمی برای مهندسی امنیتی
۲.۵. موقعیت‌بندی
۳. مدل مفهومی
۳.۱. توصیف غیر رسمی مثال انگیزشی
۳.۲. تعاریف و مفاهیم
۴. متامدل مشخصه‌بندی الگو (SEPM)
۴.۱. متامدل ویژگی کلی (GRPM)
۴.۲. فرایند مشخصه‌بندی مدل الگو: مرور اجمالی
۴.۳. مدلبندی الگو در DIPM
۴.۴. الگوی مدلبندی در DSPM
۵. فرایند رسمی‌سازی و معتبرسازی
۵.۱. چارچوب مدلبندی امنیتی SeMF
۵.۲. مصنوعات معتبرسازی
۶.۱. رسمی‌سازی الگوی ارتباطی ایمن DIPM
۶.۲. اثبات راه‌حل DIPM
۶.۳. رسمی‌سازی الگوی ارتبطات ایمن DSPM
۶.۴. اثبات مکانیسم TLS
۶.۴.۱. مفروضات و M-SeBBها
۶.۴.۲. مکانیسم‌های خاص دامنه
۶.۴.۳. اثبات
۶.۴.۴. سایر ویژگی‌های TLS
۶.۵. تناظر بین DIPM و DSPM
۷. ادغام (یکپارچه‌سازی) تکنیکهای مدلبندی و روش‌های معتبرسازی رسمی
۷.۱. در جهت مدلبندی یکپارچه و چارچوب طراحی رسمی برای تعریف الگوی امنیتی
۷.۲. بازبینی مثال انگیزشی
۸. ترکیب (سنتز) و بحث
۸.۱. مرور اجمالی و چشم‌اندازها
۸.۲. بازبینی مورد استفاده
۸.۳. ادغام الگو و توسعه برنامه کاربردی
۹. نتیجه‌گیری
ضمیمه
منابع
Abstract
1. Introduction
1.2 Intended contribution
1.3 Organization of the contribution
2. Related work
2.1 Pattern modeling approach -abstraction
2.2 Pattern composition and application
2.3 Model-driven security engineering
2.4 Formal methods for security engineering
2.5 Positioning
3. Conceptual model
3.1 Informal description of the motivating example
3.2 Definitions and concepts
4. Pattern specification metamodel (SEPM)
4.1 Generic property metamodel (GPRM)
4.2 Pattern model specification process: overview
4.3 Modeling pattern at DIPM
4.4 Modeling pattern at DSPM
5. The formalization and validation process
5.1 The security modeling framework SeMF
5.2 Validation artifacts
6. Validating secure communication patterns
6.1 Formalizing the DIPM secure communication pattern
6.2 Proving the DIPM solution
6.3 Formalizing the DSPM secure communication pattern
6.4 Proving the TLS mechanism
6.1 Formalizing the DIPM secure communication pattern
6.4.2 Domain specific mechanisms
6.4.3 The proof
6.4.4 Other properties of TLS
6.5 Correspondence between DIPM and DSPM
7. Integration of modeling techniques and formal validation methods
7.1 Towards a unified modeling and formal design framework for security pattern definition
7.2 Revisiting the motivating example
8 .Synthesis and discussion
8.1 Recapitulation and perspectives
8.2 Revisiting the use case
8.3 Integrating pattern and application development
9 .Conclusion
References
- اصل مقاله انگلیسی با فرمت ورد (word) با قابلیت ویرایش
- ترجمه فارسی مقاله با فرمت ورد (word) با قابلیت ویرایش، بدون آرم سایت ای ترجمه
- ترجمه فارسی مقاله با فرمت pdf، بدون آرم سایت ای ترجمه