2013 | OriginalPaper | Buchkapitel
Confidentiality for Probabilistic Multi-threaded Programs and Its Verification
verfasst von : Tri Minh Ngo, Mariëlle Stoelinga, Marieke Huisman
Erschienen in: Engineering Secure Software and Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Confidentiality is an important concern in today’s information society: electronic payment and personal data should be protected appropriately. This holds in particular for multi-threaded applications, which are generally seen the future of high-performance computing. Multi-threading poses new challenges to data protection, in particular, data races may be exploited in security attacks. Also, the role of the scheduler is seminal in the multi-threaded context.
This paper proposes a new notion of confidentiality for probabilistic and non-probabilistic multi-threaded programs, formalized as scheduler-specific probabilistic observational determinism (
SSPOD
), together with verification methods. Essentially,
SSPOD
ensures that no information about the private data can be derived either from the public data, or from the probabilities of the public data being changed. Moreover,
SSPOD
explicitly depends on a given (class of) schedulers.
Formally, this is expressed by using two conditions: (i) each publicly visible variable individually behaves deterministically with probability 1, and (ii) for every trace considering all publicly visible variables, there always exists a matching trace with equal probability. We verify these conditions by a clever combination of new and existing algorithms over probabilistic Kripke structures.