Specification of Security and Dependability Properties

SERENITY S&D Classes as well as S&D Patterns specify the security properties they provide. In order for a system designer to select the correct class and pattern, the security property specification must be both unambiguous and intuitive. Furthermore, in case no class or pattern can be found that provides the exact property desired by the system designer, classes and patterns providing stronger properties will also serve his/her needs. Hence there is the necessity to be able to find and prove relations between properties. In this chapter we introduce the SERENITY approach for the specification of S&D properties that are both intuitively understandable and based on a formal semantics that allows to prove relations between properties. In fact, we use two different languages: the Operational S\&D Properties Language, and the Formal S&D Properties Language.