In this paper, we present a formal technique for enforcing security policies on programs. Our technique takes an untrusted program and a security policy as input and produces a new safe program with respect to the considered policy. The proposed technique is based on the use of automata and a special composition operator called injection over automata. Injection consists in embedding the automaton representing the safety property into the automaton representing the untrusted program, so that we get a new automaton. This latter can merely be converted into a safe program which always satisfies the safety property. Consequently, our enforcement method is based on rewriting, since it takes an untrusted program and transforms it, so it produces another equivalent program satisfying the safety property. Finally, we prove that our technique is both sound and complete, i.e.: all the possible executions of the new generated program are possible executions of the original one and any possible execution of the original program respecting the security policy is a possible execution of the new generated one.