SUMMARYThis paper concerns the study, the development and the synthesis of mechanisms for guaranteeing the security of complex systems, i.e. systems composed of 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 at 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 the 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 the 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. Copyright © 2010 John Wiley & Sons, Ltd.