Confidentiality for Probabilistic Multi-Threaded Programs and Its Verification

    Research output: Book/ReportReportProfessional

    54 Downloads (Pure)

    Abstract

    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.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages19
    Publication statusPublished - 12 Dec 2012

    Publication series

    NameCTIT Technical Report Series
    PublisherCentre for Telematics and Information Technology, University of Twente
    No.TR-CTIT-13-01
    ISSN (Print)1381-3625

    Keywords

    • METIS-296171
    • Verfication
    • Scheduler-specific
    • Algorithm
    • IR-84375
    • ConfidentialityScheduler-specificObservational determinismVerficationAlgorithm
    • EWI-22687
    • Confidentiality
    • Observational determinism

    Cite this

    Ngo, M. T., Stoelinga, M. I. A., & Huisman, M. (2012). Confidentiality for Probabilistic Multi-Threaded Programs and Its Verification. (CTIT Technical Report Series; No. TR-CTIT-13-01). Enschede: Centre for Telematics and Information Technology (CTIT).