IIT Home Page CNR Home Page

A framework for automatic generation of security controller

This paper concerns the study, the development and the synthesis of mechanisms for guaranteeing the security of complex systems, i.e. , systems composed by several interacting components. A complex system under analysis is described as an open system, i.e. , a system in which an unspecified component (a component whose behaviour is not fixed in advance) interacts with the known part of the system. Within this formal approach, we propose techniques that aim to synthesize controller programs able to guarantee that, for all possible behaviours of the unspecified component, the system should work properly, e.g. , it should be able to satisfy a certain property. For performing this task, we first need to identify the set of necessary and sufficient conditions that the unspecified component has to satisfy in order to ensure that the whole system is secure. Hence, by exploiting satisfiability procedures for temporal logic, we automatically synthesize an appropriate controller program that forces the unspecified component to meet these conditions. This will ensure the security of the whole system. In particular, we contribute within the area of the enforcement of security properties by proposing a flexible and automated framework that goes beyond the definition of how a system should behave to work properly. Indeed, while the majority of related work focuses on the definition of monitoring mechanisms, we also address the synthesis problem. Moreover, we describe a tool for the synthesis of secure systems which is able to generate appropriate controller programs. This tool is also able to translate the synthesized controller programs into the ConSpec language. ConSpec programs can be actually deployed for enforcing security policies on mobile Java applications by using the run-time framework developed in the ambit of the European Project S3MS.
Software Testing, Verification & Reliability (STVR) Journal, 2010

IIT authors:

Type: Article in non-ISI Journal with international referees
Field of reference: Information Technology and Communication Systems
In: Software Testing, Verification & Reliability (STVR) Journal, vol. on-line article n. n/a. John Wiley & Sons, Ltd, 2010.