Máté Kovács and Helmut Seidl. Runtime Enforcement of Information Flow Security in Tree Manipulating Processes (Proofs) . , pages 17, 2011. Fakultät für Informatik der Technischen Universität München.
We consider the problem of enforcing information flow policies in XML manipulating programs such as Web services and business processes implemented in current workflow languages. We propose a runtime monitor that can enforce the secrecy of freely chosen subtrees of the data throughout the execution. The key idea is to apply a generalized constant propagation for computing the public effect of branching constructs whose conditions may depend on the secret. This allows for a better precision than runtime monitors which rely on tainting of variables or nodes alone. We demonstrate our approach for a minimalistic tree manipulating programming language and prove its correctness w.r.t. the concrete semantics of programs.