Idea: Action Refinement for Security Properties Enforcement

In this paper we propose an application of action refinement theory for enforcing security policies at different levels of abstraction. Indeed we assume to have a (high level) specification of a secure system with a possible untrusted component. It is controlled by a controller program, in such a way the system is secure. We show that it is possible to guarantee that the refinement of this system at a lower level of abstraction is still secure, regardless the behavior of the implementation of the untrusted component.