Confidentiality for Probabilistic Multi-Threaded Programs and Its Verification

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

6 Citations (Scopus)

Abstract

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 languageUndefined
Title of host publicationProceedings of the 5th International Conference on Engineering Secure Software and Systems, ESSoS 2013
Place of PublicationLondon
PublisherSpringer
Pages107-122
Number of pages16
ISBN (Print)978-3-642-36562-1
DOIs
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
https://distrinet.cs.kuleuven.be/events/essos/2013/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Number7781

Conference

Conference5th International Conference on Engineering Secure Software and Systems, ESSoS 2013
Abbreviated titleESSoS
CountryFrance
CityParis
Period27/02/131/03/13
Internet address

Keywords

  • METIS-296183
  • IR-83549
  • Confidentiality
  • Algorithm
  • Multi-threaded programs
  • Scheduler-specific
  • algorithmic approach
  • Verification
  • probabilistic attack
  • EWI-22760

Cite this

Ngo, M. T., Stoelinga, M. I. A., & Huisman, M. (2013). Confidentiality for Probabilistic Multi-Threaded Programs and Its Verification. In Proceedings of the 5th International Conference on Engineering Secure Software and Systems, ESSoS 2013 (pp. 107-122). (Lecture Notes in Computer Science; No. 7781). London: Springer. https://doi.org/10.1007/978-3-642-36563-8_8
Ngo, Minh Tri ; Stoelinga, Mariëlle Ida Antoinette ; Huisman, Marieke. / Confidentiality for Probabilistic Multi-Threaded Programs and Its Verification. Proceedings of the 5th International Conference on Engineering Secure Software and Systems, ESSoS 2013. London : Springer, 2013. pp. 107-122 (Lecture Notes in Computer Science; 7781).
@inproceedings{42bd5333ca184c6cb63fd8094e67a386,
title = "Confidentiality for Probabilistic Multi-Threaded Programs and Its Verification",
abstract = "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.",
keywords = "METIS-296183, IR-83549, Confidentiality, Algorithm, Multi-threaded programs, Scheduler-specific, algorithmic approach, Verification, probabilistic attack, EWI-22760",
author = "Ngo, {Minh Tri} and Stoelinga, {Mari{\"e}lle Ida Antoinette} and Marieke Huisman",
note = "10.1007/978-3-642-36563-8_8",
year = "2013",
month = "2",
doi = "10.1007/978-3-642-36563-8_8",
language = "Undefined",
isbn = "978-3-642-36562-1",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
number = "7781",
pages = "107--122",
booktitle = "Proceedings of the 5th International Conference on Engineering Secure Software and Systems, ESSoS 2013",

}

Ngo, MT, Stoelinga, MIA & Huisman, M 2013, Confidentiality for Probabilistic Multi-Threaded Programs and Its Verification. in Proceedings of the 5th International Conference on Engineering Secure Software and Systems, ESSoS 2013. Lecture Notes in Computer Science, no. 7781, Springer, London, pp. 107-122, 5th International Conference on Engineering Secure Software and Systems, ESSoS 2013, Paris, France, 27/02/13. https://doi.org/10.1007/978-3-642-36563-8_8

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

Proceedings of the 5th International Conference on Engineering Secure Software and Systems, ESSoS 2013. London : Springer, 2013. p. 107-122 (Lecture Notes in Computer Science; No. 7781).

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

TY - GEN

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

AU - Ngo, Minh Tri

AU - Stoelinga, Mariëlle Ida Antoinette

AU - Huisman, Marieke

N1 - 10.1007/978-3-642-36563-8_8

PY - 2013/2

Y1 - 2013/2

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

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

KW - METIS-296183

KW - IR-83549

KW - Confidentiality

KW - Algorithm

KW - Multi-threaded programs

KW - Scheduler-specific

KW - algorithmic approach

KW - Verification

KW - probabilistic attack

KW - EWI-22760

U2 - 10.1007/978-3-642-36563-8_8

DO - 10.1007/978-3-642-36563-8_8

M3 - Conference contribution

SN - 978-3-642-36562-1

T3 - Lecture Notes in Computer Science

SP - 107

EP - 122

BT - Proceedings of the 5th International Conference on Engineering Secure Software and Systems, ESSoS 2013

PB - Springer

CY - London

ER -

Ngo MT, Stoelinga MIA, Huisman M. Confidentiality for Probabilistic Multi-Threaded Programs and Its Verification. In Proceedings of the 5th International Conference on Engineering Secure Software and Systems, ESSoS 2013. London: Springer. 2013. p. 107-122. (Lecture Notes in Computer Science; 7781). https://doi.org/10.1007/978-3-642-36563-8_8