Compositional closure for Bayes Risk in probabilistic noninterference

Annabelle McIver, Larissa Meinicke, Carroll Morgan

We give a sequential model for noninterference security including probability (but not demonic choice), thus supporting reasoning about the likelihood that high-security values mig…