The University of New South Wales

COVERN: A logic for compositional verification of information flow control


Toby Murray, Robert Sison and Kai Engelhardt


University of Melbourne


Shared memory concurrency is pervasive in modern programming, including in systems that must protect highly sensitive data. Recently, verification has finally emerged as a practical tool for proving interesting security properties of real programs, particularly information flow control (IFC) security. Yet there remain no general logics for verifying IFC security of shared-memory concurrent programs. In this paper we present the first such logic, COVERN (Compositional Verification of Noninterference) and its proof of soundness via a new generic framework for general rely-guarantee IFC reasoning. We apply COVERN to model and verify the security-critical software functionality of the Cross Domain Desktop Compositor, an embedded device that facilitates simultaneous and intuitive user interaction with multiple classified networks while preventing leakage between them. To our knowledge this is the first foundational, machine-checked proof of IFC security for a non-trivial shared-memory concurrent program in the literature.

BibTeX Entry

    year             = {2018},
    month            = apr,
    publisher        = {IEEE},
    paperurl         = {},
    booktitle        = {European Conference on Security and Privacy (EuroS\&P)},
    author           = {Murray, Toby and Sison, Robert and Engelhardt, Kai},
    address          = {London, United Kingdom},
    title            = {{COVERN}: {A} Logic for Compositional Verification of Information Flow Control},
    date             = {2018-4-24}