FASER (Formal and Automatic Security Enforcement by Rewriting): An algebraic approach

Recent research confirmed that program rewriting techniques are powerful mechanisms for security enforcement, since they gather advantages of both static and dynamic approaches. In a previous work, we introduced the basic ideas underlying a program rewriting approach allowing to automatically enforce a security policy on an untrusted program. In this approach, a security policy and an untrusted program are specified as two processes in an extended version of the BPA (Basic Process Algebra) and the security enforcement problem is transformed to a resolution of a linear system generated from them. The enforced version of a program "behaves" like the original one except that it will be aborted when it tries to violate the security policy. In this paper, we better formalize the approach; we prove its foundation; we endow it with a high level logic to specify security policy and we implement a prototype that shows its efficiency.