In this chapter the authors present a policy-based security engineering process for service oriented applications, developed in the SERENITY and MISTICO projects. Security and dependability (S&D) are considered as first-class citizens in the proposed engineering process, which is based on the precise description of reusable security and dependability solutions. The authors’ process is based on the concept of S&D Pattern as the means to capture the specialized knowledge of security engineers and to make it available for automated processing, both in the development process (the focus of this chapter) and later at runtime. In particular, in this chapter they focus on the verification of the compliance with security policies, based on the formal specification of S&D Properties. The main advantages of the approach presented in this chapter are precisely that it allows us to define high-level policies and to verify that a secure oriented system complies with such policy (developed following the SERENITY approach). They also describe the application of the proposed approach to the verification of S&D properties in the web services (WS) environment. Concretely, the authors describe the use of SERENITY framework to facilitate the development of applications that use standard security mechanisms (such WS-Security, WS-Policy, WS-Security Policy, etc) and to ensure the correct application of these standard mechanisms, based on predefined policies. Finally, they show how to verify that the application complies with one or several S&D policies.
