Computer Science – Formal Languages and Automata Theory
Scientific paper
2010-07-07
Computer Science
Formal Languages and Automata Theory
Scientific paper
We give a sequential model for noninterference security including probability (but not demonic choice), thus supporting reasoning about the likelihood that high-security values might be revealed by observations of low-security activity. Our novel methodological contribution is the definition of a refinement order and its use to compare security measures between specifications and (their supposed) implementations. This contrasts with the more common practice of evaluating the security of individual programs in isolation. The appropriateness of our model and order is supported by our showing that our refinement order is the greatest compositional relation --the compositional closure-- with respect to our semantics and an "elementary" order based on Bayes Risk --- a security measure already in widespread use. We also relate refinement to other measures such as Shannon Entropy. By applying the approach to a non-trivial example, the anonymous-majority Three-Judges protocol, we demonstrate by example that correctness arguments can be simplified by the sort of layered developments --through levels of increasing detail-- that are allowed and encouraged by compositional semantics.
McIver Annabelle
Meinicke Larissa
Morgan Carroll
No associations
LandOfFree
Compositional closure for Bayes Risk in probabilistic noninterference does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Compositional closure for Bayes Risk in probabilistic noninterference, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Compositional closure for Bayes Risk in probabilistic noninterference will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-344970