9th International Workshop on
Security Issues in Concurrency
|09:20 - 09:30
|09:30 - 10:30
||Invited talk: Carroll Morgan.
Shadow- and Hyperdistribution Semantics for Noninterference and Refinement
|10:30 - 11:00
|11:00 - 11:30
||Vincent Cheval, Stephanie Delaune and Hubert Comon-Lundh.
A Decision Procedure for Trace Equivalence.
|11:30 - 12:00
||Alessandro Armando and Silvio Ranise.
Automated Analysis of Infinite State Workflows with Access Control Policies
|12:00 - 12:30
Unwinding Theorems for Conditional Information Flow Policies.
|12:30 - 14:30
|14:30 - 15:00
||Mahrooghi Hamidreza and Mohammadreza Mousavi.
Reconciling Operational and Epistemic Approaches to the Formal Analysis of Crypto-Based Security Protocols
|15:00 - 15:30
||Tri Ngo Minh and Marieke Huisman.
Scheduler-related Condentiality for Multi-threaded Programs
|15:30 - 16:00
|16:00 - 17:00
||Invited talk: Catuscia Palamidessi.
Quantitative Information Flow and Applications to Differential Privacy in a Distributed Perspective
|17:00 - 17:10
Morgan, University of New South Wales
Title: Shadow- and Hyperdistribution Semantics for Noninterference and
When concurrent processes exhibit both probabilistic and demonic choice, a third
semantic question arises naturally: to what extent can demonic choices exploit
probabilistic choices made at another time (eg earlier) or in another place (eg
in a separate process)? This "locality issue" has been studied intensively for
more than a decade, but is not yet resolved.
Since the effect of locality is in essence to hide (or not to hide) some choices
from others, it turns out that the semantic structures for that can also be
exploited for hiding as in noninterference-style security. We have worked on
this for some time, eg noninterference with demonic choice (but not
probabilistic) [A], and more recently noninterference with probabilistic choice
(but not demonic) [B]; some progress has been made on compositionality and, in
the latter case, also on the relation between various measures of entropy.
The technical component of the talk will be to describe the so-called "shadow"
(qualitative, possibilistic) and "hyperdistribution" (quantitative,
probabilistic) structures we have built for noninterference with a refinement
partial order (ie an implementation order that respects secrecy). Less
technically, I will outline how we came to this topic in the first place, and
how what we have done by approaching security from refinement theory might match
what others have done in the opposite direction, approaching refinement from
[a] C.C. Morgan. The Shadow Knows: Refinement of ignorance in sequential
Conference version in Proc. Math Prog Construction 2006, LNCS 4014:359-78,
Journal version in Science of Computer Programming, 74(8):629-653, 2009.
[b] Annabelle McIver, Larissa Meinicke, and Carroll Morgan.
Compositional closure for Bayes Risk in probabilistic noninterference.
ICALP'10 Part II, pages 223-235, 2010.
- Catuscia Palamidessi,
INRIA and LIX, Ecole Polytechnique
Title: Quantitative Information Flow and Applications to Differential Privacy in a Distributed Perspective