Breaking the Model: finalisation and a taxonomy of security attack

Susan Stepney; John Andrew Clark; Howard Chivers

Breaking the Model: finalisation and a taxonomy of security attack

Susan Stepney, John Andrew Clark, Howard Chivers

Computer Science

Research output: Book/Report › Other report

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
Publisher	Department of Computer Science, University of York
Number of pages	20
Publication status	Published - 2004

Publication series

Name	York Computer Science Technical Report
Publisher	Department of Computer Science, University of York
No.	YCS-2004-371
Volume	YCS

Bibliographical note

Freely available.

Keywords

Finalisation
Observed system
Security model assumptions

Access to Document

YCS 2004 371
Freely available
Final published version, 156 KB

Cite this

@book{b9279cccce1d4b7ba28e488a2a4eca34,

title = "Breaking the Model: finalisation and a taxonomy of security attack",

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 = "Susan Stepney and Clark, {John Andrew} and Howard Chivers",

note = "Freely available.",

year = "2004",

language = "English",

series = "York Computer Science Technical Report",

publisher = "Department of Computer Science, University of York",

number = "YCS-2004-371",

}

TY - BOOK

T1 - Breaking the Model

T2 - finalisation and a taxonomy of security attack

AU - Stepney, Susan

AU - Clark, John Andrew

AU - Chivers, Howard

N1 - Freely available.

PY - 2004

Y1 - 2004

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 - Other report

T3 - York Computer Science Technical Report

BT - Breaking the Model

PB - Department of Computer Science, University of York

ER -