zbMATH — the first resource for mathematics

Confidentiality for multithreaded programs via bisimulation. (English) Zbl 1254.68087
Broy, Manfred (ed.) et al., Perspectives of system informatics. 5th international Andrei Ershov memorial conference, PSI 2003, Akademgorodok, Novosibirsk, Russia, July 9–12, 2003. Revised papers. Berlin: Springer (ISBN 3-540-20813-5/pbk). Lecture Notes in Computer Science 2890, 260-274 (2003).
Summary: Bisimulation has been a popular foundation for characterizing the confidentiality properties of concurrent programs. However, because a variety of bisimulation definitions are available in the literature, it is often difficult to pin down the “right” definition for modeling a particular attacker. Focusing on timing- and probability-sensitive confidentiality for shared-memory multithreaded programs, we clarify the relation between different kinds of bisimulation by proving inclusion results. As a consequence, we derive the relationship between scheduler-specific, scheduler-independent, and strong confidentiality definitions. A key result justifying strong confidentiality is that it is the most accurate (largest) compositional indistinguishability-based confidentiality property that implies scheduler-independent confidentiality.
For the entire collection see [Zbl 1088.68003].

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI