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 non-authorized 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.

We propose a new algorithm of secrecy analysis in a framework integrating declarative programming and concurrency. The analysis of a program ensures that information can only flow from less sensitive levels toward more sensitive ones. Our algorithm uses a terminating abstract operational semantics which reduces the problem of secrecy to constraint solving within finite lattices. It departs in that from the previous works essentially based on type systems. Furthermore, our proposal is general and tackles a very large class of programs, featuring dynamic process creation, general sequential composition, recursive process calls and high level synchronization.

Dependency analysis aims at identifying how different parts of a program depend on each other. It is the kernel of many issues in program analysis such as dead-code, binding time, strictness, program slicing etc. We address the problem of dependency analysis in the context of typed /spl lambda/-calculus. We consider all systems of the /spl lambda/-cube and extend them conservatively by the addition of new typing rules in order to determine which parts of a /spl lambda/-term may contribute to its evaluation. We show how typing information can be used to statically identify dependencies.