Inductive Invariants for Noninterference in Multi-agent Workflows

Authors: Christian Müller, Helmut Seidl and Eugen Zalinescu

Paper Information

Title:Inductive Invariants for Noninterference in Multi-agent Workflows
Authors:Christian Müller, Helmut Seidl and Eugen Zalinescu
Proceedings:CSF CSF Proceedings
Editors: Stephen Chong, Stephanie Delaune and Deepak Garg
Keywords:Multi-agent workflows, Non-interference, Abstract interpretation, Inductive invariants

ABSTRACT. Our goal is to certify absence of information leaks in multi-agent workflows, such as conference management systems like \textsc{EasyChair}. These workflows can be executed by any number of agents some of which may form coalitions against the system. Therefore, checking noninterference is a challenging problem.

Our paper offers two main contributions: First, a technique is provided to translate noninterference (in presence of various agent capabilities and declassification conditions) into universally quantified invariants of an instrumented new workflow program. Second, general techniques are developed for checking and inferring universally quantified inductive invariants for workflow programs. In particular, a large class of workflows is identified where inductiveness of invariants is decidable, as well as a smaller, still useful class of workflows where the weakest inductive universal invariant implying the desired invariant, is effectively computable. The new algorithms are implemented and applied to certify noninterference for workflows arising from conference management systems.

Talk:Jul 11 10:00 (Session 60B: Information flow)