Breaking the Model: Finalisation and a Taxonomy of Security Attacks

John A. Clark; Susan Stepney; Howard Chivers

Breaking the Model: Finalisation and a Taxonomy of Security Attacks

John A. Clark, Susan Stepney, Howard Chivers

Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

It is well known that security properties are not preserved by refinement, and that refinement can introduce new, covert, channels, such as timing channels. The finalisation step in refinement can be analysed to identify some of these channels, as unwanted finalisations that can break the assumptions of the formal model. We introduce a taxonomy of such unwanted finalisations, and give examples of attacks that exploit them.

Original language	English
Pages (from-to)	225-242
Number of pages	18
Journal	Electronic Notes in Theoretical Computer Science
Volume	137
Issue number	2
Publication status	Published - Jul 2005

Bibliographical note

The above URL provides a link to the Elsevier site.

Keywords

Finalisation
observed system
security model assumptions

Access to Document

http://dx.doi.org/10.1016/j.entcs.2005.04.033

Cite this

@article{e1ea325f5ecb4dcdbbb1644b411d27ac,

title = "Breaking the Model: Finalisation and a Taxonomy of Security Attacks",

abstract = "It is well known that security properties are not preserved by refinement, and that refinement can introduce new, covert, channels, such as timing channels. The finalisation step in refinement can be analysed to identify some of these channels, as unwanted finalisations that can break the assumptions of the formal model. We introduce a taxonomy of such unwanted finalisations, and give examples of attacks that exploit them.",

keywords = "Finalisation, observed system, security model assumptions",

author = "Clark, {John A.} and Susan Stepney and Howard Chivers",

note = "The above URL provides a link to the Elsevier site.",

year = "2005",

month = jul,

language = "English",

volume = "137",

pages = "225--242",

journal = "Electronic Notes in Theoretical Computer Science",

publisher = "Elsevier",

number = "2",

}

TY - JOUR

T1 - Breaking the Model

T2 - Finalisation and a Taxonomy of Security Attacks

AU - Clark, John A.

AU - Stepney, Susan

AU - Chivers, Howard

N1 - The above URL provides a link to the Elsevier site.

PY - 2005/7

Y1 - 2005/7

N2 - It is well known that security properties are not preserved by refinement, and that refinement can introduce new, covert, channels, such as timing channels. The finalisation step in refinement can be analysed to identify some of these channels, as unwanted finalisations that can break the assumptions of the formal model. We introduce a taxonomy of such unwanted finalisations, and give examples of attacks that exploit them.

AB - It is well known that security properties are not preserved by refinement, and that refinement can introduce new, covert, channels, such as timing channels. The finalisation step in refinement can be analysed to identify some of these channels, as unwanted finalisations that can break the assumptions of the formal model. We introduce a taxonomy of such unwanted finalisations, and give examples of attacks that exploit them.

KW - Finalisation

KW - observed system

KW - security model assumptions

M3 - Article

VL - 137

SP - 225

EP - 242

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - 2

ER -