Security policy in a declarative style

We address the problem of controlling information leakage in a concurrent declarative programming setting. Our aim is to define verification tools in order to distinguish between authorized, or declared, information flows such as password testing (e.g., ATM, login processes, etc.) and nonauthorized ones. In this paper, we first propose a way to define security policies as confluent and terminating rewrite systems. Such policies define how the privacy levels of information evolve. Then, we provide a formal definition of secure processes with respect to a given security policy. We also define an actual verification algorithm of secure processes based on constraint solving.

• Type: Conference
• Year: 2005
• Where: PPDP
• Authors: Rachid Echahed, Frédéric Prost
• Keywords: Concurrent Declarative Programming, PPDP 2005, Secure Processes, Terminating Rewrite Systems