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.