Synthesis of Local Controller Programs for Enforcing Global Security Properties

In this paper we present a framework based on contexts theory and logic to study how, given a partially specified system, i.e., a system in which there are some unspecified/ unknown components, i.e., potential attackers, it is possible to enforce a global security property by controlling all the unspecified parts of the given system. We propose two methods to control them: A centralized method, in which there is a unique controller program that controls all the unspecified components, and a decentralized one in which each unspecified component is monitored by a controller program that forces it to behave correctly, i.e., according to a local requirement found by a reduction of the global one. In both cases we show how to synthesize controller programs that solve the problem.