Scheduler-Specific Confidentiality for Multi-Threaded Programs and Its Logic-Based Verification

Marieke Huisman, Minh Tri Ngo

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

8 Citations (Scopus)
8 Downloads (Pure)

Abstract

Observational determinism has been proposed in the literature as a way to ensure condentiality for multi-threaded programs. Intuitively, a program is observationally deterministic if the behavior of the public variables is deterministic, i.e., independent of the private variables and the scheduling policy. Several formal denitions of observational determinism exist, but all of them have shortcomings; for example they accept insecure programs or they reject too many innocuous programs. Besides, the role of schedulers was ignored in all the proposed denitions. A program that is secure under one kind of scheduler might not be secure when executed with a dierent scheduler. The existing definitions do not ensure that an accepted program behaves securely under the scheduler that is used to deploy the program. Therefore, this paper proposes a new formalization of scheduler-specic observational determinism. It accepts programs that are secure when executed under a specic scheduler. Moreover, it is less restrictive on harmless programs under a particular scheduling policy. We discuss the properties of our denition and argue why it better approximates the intuitive understanding of observational determinism. In addition, we discuss how compliance with our denition can be veried, using model checking. We use the idea of self-composition and we rephrase the observational determinism property for a single program $C$ as a temporal logic formula over the program $C$ executed in parallel with an independent copy of itself. Thus two states reachable during the execution of $C$ are combined into a reachable program state of the selfcomposed program. This allows to compare two program executions in a single temporal logic formula. The actual characterization is done in two steps. First we discuss how stuttering equivalence can be characterized as a temporal logic formula. Observational determinism is then expressed in terms of the stuttering equivalence characterization. This results in a conjunction of n LTL and a CTL formula, that are amenable to model checking.
Original languageUndefined
Title of host publication2nd International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2011), Revised Selected Papers
EditorsB. Beckert, F. Damiani, D. Gurov
Place of PublicationBerlin
PublisherSpringer
Pages178-195
Number of pages18
ISBN (Print)978-3-642-31761-3
DOIs
Publication statusPublished - 2012

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume7421
ISSN (Print)0302-9743

Keywords

  • METIS-285035
  • Confidentiality
  • IR-79437
  • Multi-threaded programs
  • EWI-21337
  • Security
  • Observational determinism
  • Temporal Logic
  • noninterference
  • Verification

Cite this

Huisman, M., & Ngo, M. T. (2012). Scheduler-Specific Confidentiality for Multi-Threaded Programs and Its Logic-Based Verification. In B. Beckert, F. Damiani, & D. Gurov (Eds.), 2nd International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2011), Revised Selected Papers (pp. 178-195). (Lecture Notes in Computer Science; Vol. 7421). Berlin: Springer. https://doi.org/10.1007/978-3-642-31762-0_12
Huisman, Marieke ; Ngo, Minh Tri. / Scheduler-Specific Confidentiality for Multi-Threaded Programs and Its Logic-Based Verification. 2nd International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2011), Revised Selected Papers. editor / B. Beckert ; F. Damiani ; D. Gurov. Berlin : Springer, 2012. pp. 178-195 (Lecture Notes in Computer Science).
@inproceedings{c3cbe994aa2c42fc88efcf377791f9dd,
title = "Scheduler-Specific Confidentiality for Multi-Threaded Programs and Its Logic-Based Verification",
abstract = "Observational determinism has been proposed in the literature as a way to ensure condentiality for multi-threaded programs. Intuitively, a program is observationally deterministic if the behavior of the public variables is deterministic, i.e., independent of the private variables and the scheduling policy. Several formal denitions of observational determinism exist, but all of them have shortcomings; for example they accept insecure programs or they reject too many innocuous programs. Besides, the role of schedulers was ignored in all the proposed denitions. A program that is secure under one kind of scheduler might not be secure when executed with a dierent scheduler. The existing definitions do not ensure that an accepted program behaves securely under the scheduler that is used to deploy the program. Therefore, this paper proposes a new formalization of scheduler-specic observational determinism. It accepts programs that are secure when executed under a specic scheduler. Moreover, it is less restrictive on harmless programs under a particular scheduling policy. We discuss the properties of our denition and argue why it better approximates the intuitive understanding of observational determinism. In addition, we discuss how compliance with our denition can be veried, using model checking. We use the idea of self-composition and we rephrase the observational determinism property for a single program $C$ as a temporal logic formula over the program $C$ executed in parallel with an independent copy of itself. Thus two states reachable during the execution of $C$ are combined into a reachable program state of the selfcomposed program. This allows to compare two program executions in a single temporal logic formula. The actual characterization is done in two steps. First we discuss how stuttering equivalence can be characterized as a temporal logic formula. Observational determinism is then expressed in terms of the stuttering equivalence characterization. This results in a conjunction of n LTL and a CTL formula, that are amenable to model checking.",
keywords = "METIS-285035, Confidentiality, IR-79437, Multi-threaded programs, EWI-21337, Security, Observational determinism, Temporal Logic, noninterference, Verification",
author = "Marieke Huisman and Ngo, {Minh Tri}",
note = "eemcs-eprint-21337",
year = "2012",
doi = "10.1007/978-3-642-31762-0_12",
language = "Undefined",
isbn = "978-3-642-31761-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "178--195",
editor = "B. Beckert and F. Damiani and D. Gurov",
booktitle = "2nd International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2011), Revised Selected Papers",

}

Huisman, M & Ngo, MT 2012, Scheduler-Specific Confidentiality for Multi-Threaded Programs and Its Logic-Based Verification. in B Beckert, F Damiani & D Gurov (eds), 2nd International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2011), Revised Selected Papers. Lecture Notes in Computer Science, vol. 7421, Springer, Berlin, pp. 178-195. https://doi.org/10.1007/978-3-642-31762-0_12

Scheduler-Specific Confidentiality for Multi-Threaded Programs and Its Logic-Based Verification. / Huisman, Marieke; Ngo, Minh Tri.

2nd International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2011), Revised Selected Papers. ed. / B. Beckert; F. Damiani; D. Gurov. Berlin : Springer, 2012. p. 178-195 (Lecture Notes in Computer Science; Vol. 7421).

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

TY - GEN

T1 - Scheduler-Specific Confidentiality for Multi-Threaded Programs and Its Logic-Based Verification

AU - Huisman, Marieke

AU - Ngo, Minh Tri

N1 - eemcs-eprint-21337

PY - 2012

Y1 - 2012

N2 - Observational determinism has been proposed in the literature as a way to ensure condentiality for multi-threaded programs. Intuitively, a program is observationally deterministic if the behavior of the public variables is deterministic, i.e., independent of the private variables and the scheduling policy. Several formal denitions of observational determinism exist, but all of them have shortcomings; for example they accept insecure programs or they reject too many innocuous programs. Besides, the role of schedulers was ignored in all the proposed denitions. A program that is secure under one kind of scheduler might not be secure when executed with a dierent scheduler. The existing definitions do not ensure that an accepted program behaves securely under the scheduler that is used to deploy the program. Therefore, this paper proposes a new formalization of scheduler-specic observational determinism. It accepts programs that are secure when executed under a specic scheduler. Moreover, it is less restrictive on harmless programs under a particular scheduling policy. We discuss the properties of our denition and argue why it better approximates the intuitive understanding of observational determinism. In addition, we discuss how compliance with our denition can be veried, using model checking. We use the idea of self-composition and we rephrase the observational determinism property for a single program $C$ as a temporal logic formula over the program $C$ executed in parallel with an independent copy of itself. Thus two states reachable during the execution of $C$ are combined into a reachable program state of the selfcomposed program. This allows to compare two program executions in a single temporal logic formula. The actual characterization is done in two steps. First we discuss how stuttering equivalence can be characterized as a temporal logic formula. Observational determinism is then expressed in terms of the stuttering equivalence characterization. This results in a conjunction of n LTL and a CTL formula, that are amenable to model checking.

AB - Observational determinism has been proposed in the literature as a way to ensure condentiality for multi-threaded programs. Intuitively, a program is observationally deterministic if the behavior of the public variables is deterministic, i.e., independent of the private variables and the scheduling policy. Several formal denitions of observational determinism exist, but all of them have shortcomings; for example they accept insecure programs or they reject too many innocuous programs. Besides, the role of schedulers was ignored in all the proposed denitions. A program that is secure under one kind of scheduler might not be secure when executed with a dierent scheduler. The existing definitions do not ensure that an accepted program behaves securely under the scheduler that is used to deploy the program. Therefore, this paper proposes a new formalization of scheduler-specic observational determinism. It accepts programs that are secure when executed under a specic scheduler. Moreover, it is less restrictive on harmless programs under a particular scheduling policy. We discuss the properties of our denition and argue why it better approximates the intuitive understanding of observational determinism. In addition, we discuss how compliance with our denition can be veried, using model checking. We use the idea of self-composition and we rephrase the observational determinism property for a single program $C$ as a temporal logic formula over the program $C$ executed in parallel with an independent copy of itself. Thus two states reachable during the execution of $C$ are combined into a reachable program state of the selfcomposed program. This allows to compare two program executions in a single temporal logic formula. The actual characterization is done in two steps. First we discuss how stuttering equivalence can be characterized as a temporal logic formula. Observational determinism is then expressed in terms of the stuttering equivalence characterization. This results in a conjunction of n LTL and a CTL formula, that are amenable to model checking.

KW - METIS-285035

KW - Confidentiality

KW - IR-79437

KW - Multi-threaded programs

KW - EWI-21337

KW - Security

KW - Observational determinism

KW - Temporal Logic

KW - noninterference

KW - Verification

U2 - 10.1007/978-3-642-31762-0_12

DO - 10.1007/978-3-642-31762-0_12

M3 - Conference contribution

SN - 978-3-642-31761-3

T3 - Lecture Notes in Computer Science

SP - 178

EP - 195

BT - 2nd International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2011), Revised Selected Papers

A2 - Beckert, B.

A2 - Damiani, F.

A2 - Gurov, D.

PB - Springer

CY - Berlin

ER -

Huisman M, Ngo MT. Scheduler-Specific Confidentiality for Multi-Threaded Programs and Its Logic-Based Verification. In Beckert B, Damiani F, Gurov D, editors, 2nd International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2011), Revised Selected Papers. Berlin: Springer. 2012. p. 178-195. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-31762-0_12