Security enforcement by rewriting: An algebraic approach

Abstract

This paper introduces a formal program-rewriting approach that can automatically enforce security policies on non trusted programs. For a program P and a security policy Φ, we generate another program P' that respects the security policy and behaves like P except that it stops any execution path whenever the enforced security policy is about to be violated. The presented approach uses the EBPA ∗ 0,1 algebra which is a variant of BPA (Basic Process Algebra) extended with variables, environments and conditions. The problem of computing the expected enforced program P' will turn to resolve a linear system which we already know how to extract the solution by a polynomial algorithm.