Máté Kovács and Helmut Seidl. Runtime Enforcement of Information Flow Security in Tree Manipulating Processes. In Gilles Barthe, Benjamin Livshits and Riccardo Scandariato, editors, Engineering Secure Software and Systems, volume 7159 of Lecture Notes in Computer Science, pages 46-59, 2012. 10.1007/978-3-642-28166-2_6. Springer Berlin / Heidelberg.
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.