The importance of information systems security in today’s technology-driven world cannot be overstated. Every organization, government, and business relies heavily on computer systems, making it crucial to ensure that the programs we develop are secure and free from any potential vulnerabilities that could result in devastating damage and financial losses. This paper presents a formal program-rewriting approach that automates the enforcement of security policies on untrusted programs. Given a program P and a security policy Φ we generate a new program P’ that respects the security policy Φ and behaves similarly (with respect to trace equivalence) to the original program P except when the security policy is about to be violated. The solution is made possible through the use of the ℰBPA*_0,1 algebra, which is a modified version of BPA*_0,1 (Basic Process Algebra) extended with variables, environments, and conditions. The ℰBPA*_0,1 algebra provides the necessary formalization to tackle the problem, transforming the complex and challenging task of securing a program into a manageable task of solving a linear system with a known solution.