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

Marieke Huisman, Minh Tri Ngo

Research output: Book/ReportReportProfessional

31 Downloads (Pure)

Abstract

Observational determinism has been proposed in the literature as a way to ensure confidentiality 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 definitions 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 definitions. A program that is secure under one kind of scheduler might not be secure when executed with a different 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-specific observational determinism. It accepts programs that are secure when executed under a specific scheduler. Moreover, it is less restrictive on harmless programs under a particular scheduling policy. In addition, we discuss how compliance with our definition can be verified, 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 self-composed 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 an LTL and a CTL formula, that are amenable to model checking.
Original languageUndefined
Place of PublicationEnschede
PublisherCentre for Telematics and Information Technology (CTIT)
Number of pages21
Publication statusPublished - 6 Oct 2011

Publication series

NameCTIT Technical Report Series
PublisherUniversity of Twente, Centre for Telematics and Information Technology
No.TR-CTIT-11-22
ISSN (Print)1381-3625

Keywords

  • IR-78119
  • Confidentiality
  • Model Checking
  • Multi-threaded programs
  • METIS-278805
  • Observational determinism
  • Verification
  • EWI-20534
  • logic-based
  • observational determinismscheduler-specificlogic-basedverificationmodel checkingconfidentialitymulti-threaded programs
  • Scheduler-specific

Cite this

Huisman, M., & Ngo, M. T. (2011). Scheduler-specific Confidentiality for Multi-Threaded Programs and Its Logic-Based Verification. (CTIT Technical Report Series; No. TR-CTIT-11-22). Enschede: Centre for Telematics and Information Technology (CTIT).
Huisman, Marieke ; Ngo, Minh Tri. / Scheduler-specific Confidentiality for Multi-Threaded Programs and Its Logic-Based Verification. Enschede : Centre for Telematics and Information Technology (CTIT), 2011. 21 p. (CTIT Technical Report Series; TR-CTIT-11-22).
@book{046353defdef40ffa10552043c15d1eb,
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 confidentiality 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 definitions 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 definitions. A program that is secure under one kind of scheduler might not be secure when executed with a different 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-specific observational determinism. It accepts programs that are secure when executed under a specific scheduler. Moreover, it is less restrictive on harmless programs under a particular scheduling policy. In addition, we discuss how compliance with our definition can be verified, 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 self-composed 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 an LTL and a CTL formula, that are amenable to model checking.",
keywords = "IR-78119, Confidentiality, Model Checking, Multi-threaded programs, METIS-278805, Observational determinism, Verification, EWI-20534, logic-based, observational determinismscheduler-specificlogic-basedverificationmodel checkingconfidentialitymulti-threaded programs, Scheduler-specific",
author = "Marieke Huisman and Ngo, {Minh Tri}",
note = "This is a long version of the paper submitted to FoVeOOS 2011. Part of this paper was presented at SecCo 2011, Aachen, Germany.",
year = "2011",
month = "10",
day = "6",
language = "Undefined",
series = "CTIT Technical Report Series",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "TR-CTIT-11-22",
address = "Netherlands",

}

Huisman, M & Ngo, MT 2011, Scheduler-specific Confidentiality for Multi-Threaded Programs and Its Logic-Based Verification. CTIT Technical Report Series, no. TR-CTIT-11-22, Centre for Telematics and Information Technology (CTIT), Enschede.

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

Enschede : Centre for Telematics and Information Technology (CTIT), 2011. 21 p. (CTIT Technical Report Series; No. TR-CTIT-11-22).

Research output: Book/ReportReportProfessional

TY - BOOK

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

AU - Huisman, Marieke

AU - Ngo, Minh Tri

N1 - This is a long version of the paper submitted to FoVeOOS 2011. Part of this paper was presented at SecCo 2011, Aachen, Germany.

PY - 2011/10/6

Y1 - 2011/10/6

N2 - Observational determinism has been proposed in the literature as a way to ensure confidentiality 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 definitions 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 definitions. A program that is secure under one kind of scheduler might not be secure when executed with a different 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-specific observational determinism. It accepts programs that are secure when executed under a specific scheduler. Moreover, it is less restrictive on harmless programs under a particular scheduling policy. In addition, we discuss how compliance with our definition can be verified, 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 self-composed 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 an 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 confidentiality 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 definitions 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 definitions. A program that is secure under one kind of scheduler might not be secure when executed with a different 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-specific observational determinism. It accepts programs that are secure when executed under a specific scheduler. Moreover, it is less restrictive on harmless programs under a particular scheduling policy. In addition, we discuss how compliance with our definition can be verified, 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 self-composed 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 an LTL and a CTL formula, that are amenable to model checking.

KW - IR-78119

KW - Confidentiality

KW - Model Checking

KW - Multi-threaded programs

KW - METIS-278805

KW - Observational determinism

KW - Verification

KW - EWI-20534

KW - logic-based

KW - observational determinismscheduler-specificlogic-basedverificationmodel checkingconfidentialitymulti-threaded programs

KW - Scheduler-specific

M3 - Report

T3 - CTIT Technical Report Series

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

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -

Huisman M, Ngo MT. Scheduler-specific Confidentiality for Multi-Threaded Programs and Its Logic-Based Verification. Enschede: Centre for Telematics and Information Technology (CTIT), 2011. 21 p. (CTIT Technical Report Series; TR-CTIT-11-22).