Confidentiality for Probabilistic Multi-Threaded Programs and Its Verification

Research output: Book/ReportReportProfessional

38 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).
Ngo, Minh Tri ; Stoelinga, Mariëlle Ida Antoinette ; Huisman, Marieke. / Confidentiality for Probabilistic Multi-Threaded Programs and Its Verification. Enschede : Centre for Telematics and Information Technology (CTIT), 2012. 19 p. (CTIT Technical Report Series; TR-CTIT-13-01).
@book{5ec947472af04b22aaa2945b7ced4d65,
title = "Confidentiality for Probabilistic Multi-Threaded Programs and Its Verification",
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.",
keywords = "METIS-296171, Verfication, Scheduler-specific, Algorithm, IR-84375, ConfidentialityScheduler-specificObservational determinismVerficationAlgorithm, EWI-22687, Confidentiality, Observational determinism",
author = "Ngo, {Minh Tri} and Stoelinga, {Mari{\"e}lle Ida Antoinette} and Marieke Huisman",
note = "This is the extended version of the ESSoS-13 paper",
year = "2012",
month = "12",
day = "12",
language = "Undefined",
series = "CTIT Technical Report Series",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "TR-CTIT-13-01",
address = "Netherlands",

}

Ngo, MT, Stoelinga, MIA & Huisman, M 2012, Confidentiality for Probabilistic Multi-Threaded Programs and Its Verification. CTIT Technical Report Series, no. TR-CTIT-13-01, Centre for Telematics and Information Technology (CTIT), Enschede.

Confidentiality for Probabilistic Multi-Threaded Programs and Its Verification. / Ngo, Minh Tri; Stoelinga, Mariëlle Ida Antoinette; Huisman, Marieke.

Enschede : Centre for Telematics and Information Technology (CTIT), 2012. 19 p. (CTIT Technical Report Series; No. TR-CTIT-13-01).

Research output: Book/ReportReportProfessional

TY - BOOK

T1 - Confidentiality for Probabilistic Multi-Threaded Programs and Its Verification

AU - Ngo, Minh Tri

AU - Stoelinga, Mariëlle Ida Antoinette

AU - Huisman, Marieke

N1 - This is the extended version of the ESSoS-13 paper

PY - 2012/12/12

Y1 - 2012/12/12

N2 - 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.

AB - 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.

KW - METIS-296171

KW - Verfication

KW - Scheduler-specific

KW - Algorithm

KW - IR-84375

KW - ConfidentialityScheduler-specificObservational determinismVerficationAlgorithm

KW - EWI-22687

KW - Confidentiality

KW - Observational determinism

M3 - Report

T3 - CTIT Technical Report Series

BT - Confidentiality for Probabilistic Multi-Threaded Programs and Its Verification

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -

Ngo MT, Stoelinga MIA, Huisman M. Confidentiality for Probabilistic Multi-Threaded Programs and Its Verification. Enschede: Centre for Telematics and Information Technology (CTIT), 2012. 19 p. (CTIT Technical Report Series; TR-CTIT-13-01).