Model-checking Secure Information Flow for Multi-Threaded Programs

Marieke Huisman, Henri-Charles Blondeel

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

26 Downloads (Pure)

Abstract

This paper shows how secure information flow properties of multi-threaded programs can be verified by model checking in a precise and efficient way, by using the idea of self-composition. It discusses two properties that aim to capture secure information flow for multi-threaded programs, and it shows how these properties can be char- acterised in modal μ-calculus. For this characterisation, a self-composed model of the program is constructed. More precisely, this is a model that contains two copies of the labelled transition system induced by the program, so that the program is executed in parallel with itself. The self- composed model allows to compare two program executions in a single temporal formula that characterises a secure information flow property. Both the formula and model are translated into the input language for the Concurrency Workbench model checker. We discuss this encoding, and use it for some practical experiments on several simple examples.
Original languageUndefined
Title of host publicationProceedings of the Joint Workshop on Theory of Security and Applications, TOSCA 2011
EditorsS. Mödersheim, C. Palamadessi
Place of PublicationBerlin
PublisherSpringer
Pages148-165
Number of pages18
ISBN (Print)978-3-642-27374-2
DOIs
Publication statusPublished - Mar 2011

Publication series

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

Keywords

  • METIS-277679
  • EWI-20260
  • IR-77615

Cite this

Huisman, M., & Blondeel, H-C. (2011). Model-checking Secure Information Flow for Multi-Threaded Programs. In S. Mödersheim, & C. Palamadessi (Eds.), Proceedings of the Joint Workshop on Theory of Security and Applications, TOSCA 2011 (pp. 148-165). (Lecture Notes in Computer Science; Vol. 6993). Berlin: Springer. https://doi.org/10.1007/978-3-642-27375-9_9
Huisman, Marieke ; Blondeel, Henri-Charles. / Model-checking Secure Information Flow for Multi-Threaded Programs. Proceedings of the Joint Workshop on Theory of Security and Applications, TOSCA 2011. editor / S. Mödersheim ; C. Palamadessi. Berlin : Springer, 2011. pp. 148-165 (Lecture Notes in Computer Science).
@inproceedings{663beae7e9ad4cecba6e5401b112178b,
title = "Model-checking Secure Information Flow for Multi-Threaded Programs",
abstract = "This paper shows how secure information flow properties of multi-threaded programs can be verified by model checking in a precise and efficient way, by using the idea of self-composition. It discusses two properties that aim to capture secure information flow for multi-threaded programs, and it shows how these properties can be char- acterised in modal μ-calculus. For this characterisation, a self-composed model of the program is constructed. More precisely, this is a model that contains two copies of the labelled transition system induced by the program, so that the program is executed in parallel with itself. The self- composed model allows to compare two program executions in a single temporal formula that characterises a secure information flow property. Both the formula and model are translated into the input language for the Concurrency Workbench model checker. We discuss this encoding, and use it for some practical experiments on several simple examples.",
keywords = "METIS-277679, EWI-20260, IR-77615",
author = "Marieke Huisman and Henri-Charles Blondeel",
year = "2011",
month = "3",
doi = "10.1007/978-3-642-27375-9_9",
language = "Undefined",
isbn = "978-3-642-27374-2",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "148--165",
editor = "S. M{\"o}dersheim and C. Palamadessi",
booktitle = "Proceedings of the Joint Workshop on Theory of Security and Applications, TOSCA 2011",

}

Huisman, M & Blondeel, H-C 2011, Model-checking Secure Information Flow for Multi-Threaded Programs. in S Mödersheim & C Palamadessi (eds), Proceedings of the Joint Workshop on Theory of Security and Applications, TOSCA 2011. Lecture Notes in Computer Science, vol. 6993, Springer, Berlin, pp. 148-165. https://doi.org/10.1007/978-3-642-27375-9_9

Model-checking Secure Information Flow for Multi-Threaded Programs. / Huisman, Marieke; Blondeel, Henri-Charles.

Proceedings of the Joint Workshop on Theory of Security and Applications, TOSCA 2011. ed. / S. Mödersheim; C. Palamadessi. Berlin : Springer, 2011. p. 148-165 (Lecture Notes in Computer Science; Vol. 6993).

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

TY - GEN

T1 - Model-checking Secure Information Flow for Multi-Threaded Programs

AU - Huisman, Marieke

AU - Blondeel, Henri-Charles

PY - 2011/3

Y1 - 2011/3

N2 - This paper shows how secure information flow properties of multi-threaded programs can be verified by model checking in a precise and efficient way, by using the idea of self-composition. It discusses two properties that aim to capture secure information flow for multi-threaded programs, and it shows how these properties can be char- acterised in modal μ-calculus. For this characterisation, a self-composed model of the program is constructed. More precisely, this is a model that contains two copies of the labelled transition system induced by the program, so that the program is executed in parallel with itself. The self- composed model allows to compare two program executions in a single temporal formula that characterises a secure information flow property. Both the formula and model are translated into the input language for the Concurrency Workbench model checker. We discuss this encoding, and use it for some practical experiments on several simple examples.

AB - This paper shows how secure information flow properties of multi-threaded programs can be verified by model checking in a precise and efficient way, by using the idea of self-composition. It discusses two properties that aim to capture secure information flow for multi-threaded programs, and it shows how these properties can be char- acterised in modal μ-calculus. For this characterisation, a self-composed model of the program is constructed. More precisely, this is a model that contains two copies of the labelled transition system induced by the program, so that the program is executed in parallel with itself. The self- composed model allows to compare two program executions in a single temporal formula that characterises a secure information flow property. Both the formula and model are translated into the input language for the Concurrency Workbench model checker. We discuss this encoding, and use it for some practical experiments on several simple examples.

KW - METIS-277679

KW - EWI-20260

KW - IR-77615

U2 - 10.1007/978-3-642-27375-9_9

DO - 10.1007/978-3-642-27375-9_9

M3 - Conference contribution

SN - 978-3-642-27374-2

T3 - Lecture Notes in Computer Science

SP - 148

EP - 165

BT - Proceedings of the Joint Workshop on Theory of Security and Applications, TOSCA 2011

A2 - Mödersheim, S.

A2 - Palamadessi, C.

PB - Springer

CY - Berlin

ER -

Huisman M, Blondeel H-C. Model-checking Secure Information Flow for Multi-Threaded Programs. In Mödersheim S, Palamadessi C, editors, Proceedings of the Joint Workshop on Theory of Security and Applications, TOSCA 2011. Berlin: Springer. 2011. p. 148-165. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-27375-9_9