S-Promela: An executable specification security policies language

Security Policy constitutes the main basis of a secured system but can be its main vulnerability also since a wrongly configured policy or an inadequate one can be fatal for the system. Even if the network administrator is a high qualified person, the human interventions are error prone. Nevertheless, a formal specification can avoid such problem. This paper aims to give a first step towards a framework allowing to specify and to verify a given policy with respect to an expected one. Hence, we propose in this paper a new all-purpose security policy modeling based on the concepts of processes, channels, constraints, events and actions. This modeling is called all-purpose because it can be easily used to represent the several kinds of security rules i.e. authorization, obligation and prohibition. Moreover, it constitutes the first step towards the proposition of a new executable security specification language. This language, called S-Promela has a syntax supporting authorization, obligation and prohibition rules and a semantics facilitating the validation task.