Globally reasoning about localised security policies in distributed systems

Publication: ResearchReport – Annual report year: 2012

Standard

Globally reasoning about localised security policies in distributed systems. / Hernandez, Alejandro Mario.

Kgs. Lyngby : Technical University of Denmark, 2012. 45 p. (IMM-Technical Report-2012; No. 11).

Publication: ResearchReport – Annual report year: 2012

Harvard

Hernandez, AM 2012, Globally reasoning about localised security policies in distributed systems. Technical University of Denmark, Kgs. Lyngby. IMM-Technical Report-2012, no. 11

APA

Hernandez, A. M. (2012). Globally reasoning about localised security policies in distributed systems. Kgs. Lyngby: Technical University of Denmark. (IMM-Technical Report-2012; No. 11).

CBE

Hernandez AM 2012. Globally reasoning about localised security policies in distributed systems. Kgs. Lyngby: Technical University of Denmark. 45 p. (IMM-Technical Report-2012; No. 11).

MLA

Hernandez, Alejandro Mario Globally reasoning about localised security policies in distributed systems Kgs. Lyngby: Technical University of Denmark. 2012. (IMM-Technical Report-2012; Journal number 11).

Vancouver

Hernandez AM. Globally reasoning about localised security policies in distributed systems. Kgs. Lyngby: Technical University of Denmark, 2012. 45 p. (IMM-Technical Report-2012; No. 11).

Author

Hernandez, Alejandro Mario / Globally reasoning about localised security policies in distributed systems.

Kgs. Lyngby : Technical University of Denmark, 2012. 45 p. (IMM-Technical Report-2012; No. 11).

Publication: ResearchReport – Annual report year: 2012

Bibtex

@book{9d0d4321d0b94da0a6e3b835df0a77fe,
title = "Globally reasoning about localised security policies in distributed systems",
publisher = "Technical University of Denmark",
author = "Hernandez, {Alejandro Mario}",
year = "2012",
series = "IMM-Technical Report-2012",

}

RIS

TY - RPRT

T1 - Globally reasoning about localised security policies in distributed systems

A1 - Hernandez,Alejandro Mario

AU - Hernandez,Alejandro Mario

PB - Technical University of Denmark

PY - 2012

Y1 - 2012

N2 - In this report, we aim at establishing proper ways for model checking the global security of distributed systems, which are designed consisting of set of localised security policies that enforce specific issues about the security expected.<br/>The systems are formally specified following a syntax, defined in detail in this report, and their behaviour is clearly established by the Semantics, also defined in detail in this report. The systems include the formal attachment of security policies into their locations, whose intended interactions are trapped by the policies, aiming at taking access control decisions of the system, and the Semantics also takes care of this.<br/>Using the Semantics, a Labelled Transition System (LTS) can be induced for every particular system, and over this LTS some model checking tasks could be done. We identify how this LTS is indeed obtained, and propose an alternative way of model checking the not-yet-induced LTS, by using the system design directly. This may lead to over-approximation thereby producing imprecise, though safe, results. We restrict ourselves to finite systems, in the sake of being certain about the decidability of the proposed method.<br/>To illustrate the usefulness and validity of our proposal, we present 2 small case-study-like examples, where we show how the system can be specified, which policies could be added to it, and how to decide if the desired global security property is met.<br/>Finally, an Appendix is given for digging deeply into how a tool for automatically performing this task is being built, including some implementation issues. The tool takes advantage of the proposed method, and given some system and some desired global security property, it safely (i.e. without false positives) ensures satisfaction of it.

AB - In this report, we aim at establishing proper ways for model checking the global security of distributed systems, which are designed consisting of set of localised security policies that enforce specific issues about the security expected.<br/>The systems are formally specified following a syntax, defined in detail in this report, and their behaviour is clearly established by the Semantics, also defined in detail in this report. The systems include the formal attachment of security policies into their locations, whose intended interactions are trapped by the policies, aiming at taking access control decisions of the system, and the Semantics also takes care of this.<br/>Using the Semantics, a Labelled Transition System (LTS) can be induced for every particular system, and over this LTS some model checking tasks could be done. We identify how this LTS is indeed obtained, and propose an alternative way of model checking the not-yet-induced LTS, by using the system design directly. This may lead to over-approximation thereby producing imprecise, though safe, results. We restrict ourselves to finite systems, in the sake of being certain about the decidability of the proposed method.<br/>To illustrate the usefulness and validity of our proposal, we present 2 small case-study-like examples, where we show how the system can be specified, which policies could be added to it, and how to decide if the desired global security property is met.<br/>Finally, an Appendix is given for digging deeply into how a tool for automatically performing this task is being built, including some implementation issues. The tool takes advantage of the proposed method, and given some system and some desired global security property, it safely (i.e. without false positives) ensures satisfaction of it.

BT - Globally reasoning about localised security policies in distributed systems

T3 - IMM-Technical Report-2012

T3 - en_GB

ER -