Confidentiality for Probabilistic Multi-Threaded Programs and Its Verification

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    13 Citations (Scopus)
    15 Downloads (Pure)


    Confidentiality is an important concern in today’s informa- tion 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 sched- uler 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, SS- POD 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.
    Original languageEnglish
    Title of host publicationProceedings of the 5th International Conference on Engineering Secure Software and Systems, ESSoS 2013
    Place of PublicationLondon
    Number of pages16
    ISBN (Print)978-3-642-36562-1
    Publication statusPublished - Feb 2013
    Event5th International Conference on Engineering Secure Software and Systems, ESSoS 2013 - Paris, France
    Duration: 27 Feb 20131 Mar 2013
    Conference number: 5

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag


    Conference5th International Conference on Engineering Secure Software and Systems, ESSoS 2013
    Abbreviated titleESSoS
    Internet address


    • Confidentiality
    • Algorithm
    • Multi-threaded programs
    • Scheduler-specific
    • algorithmic approach
    • Verification
    • probabilistic attack


    Dive into the research topics of 'Confidentiality for Probabilistic Multi-Threaded Programs and Its Verification'. Together they form a unique fingerprint.

    Cite this