A Language-based Approach to Analysing Flow Security Properties in Virtualised Computing Systems

Chunyan Mu

doi:10.1109/TASE49443.2020.00033

A Language-based Approach to Analysing Flow Security Properties in Virtualised Computing Systems

Chunyan Mu

Teesside University

Research output: Chapter in Book/Report/Conference proceeding › Published conference contribution

4 Downloads (Pure)

Abstract

This paper studies the problem of reasoning about flow security properties in virtualised computing networks with mobility from perspective of formal language. We propose a distributed process algebra CSP4v with security labelled processes for the purpose of formal modelling of virtualised computing systems. Specifically, information leakage can come from observations on process executions, communications and from cache side channels in the virtualised environment. We describe a cache flow policy to identify such flows. A type system of the language is presented to enforce the flow policy.

Original language	English
Title of host publication	2020 International Symposium on Theoretical Aspects of Software Engineering (TASE)
Publisher	IEEE Explore
Pages	185-192
Number of pages	8
ISBN (Electronic)	978-1-7281-4086-5
DOIs	https://doi.org/10.1109/TASE49443.2020.00033
Publication status	Published - 11 Dec 2020
Event	International Symposium on Theoretical Aspects of Software Engineering - Hangzhou, China, Hangzhou, China Duration: 11 Dec 2020 → 13 Dec 2020

Conference

Conference	International Symposium on Theoretical Aspects of Software Engineering
Abbreviated title	TASE
Country/Territory	China
City	Hangzhou
Period	11/12/20 → 13/12/20

Access to Document

10.1109/TASE49443.2020.00033Licence: Unspecified

flow-vmAccepted author manuscript, 183 KBLicence: Unspecified

Cite this

@inproceedings{3acb54327ffb44f4bbc75419c2cf0bf9,

title = "A Language-based Approach to Analysing Flow Security Properties in Virtualised Computing Systems",

abstract = "This paper studies the problem of reasoning about flow security properties in virtualised computing networks with mobility from perspective of formal language. We propose a distributed process algebra CSP4v with security labelled processes for the purpose of formal modelling of virtualised computing systems. Specifically, information leakage can come from observations on process executions, communications and from cache side channels in the virtualised environment. We describe a cache flow policy to identify such flows. A type system of the language is presented to enforce the flow policy.",

author = "Chunyan Mu",

year = "2020",

month = dec,

day = "11",

doi = "10.1109/TASE49443.2020.00033",

language = "English",

pages = "185--192",

booktitle = "2020 International Symposium on Theoretical Aspects of Software Engineering (TASE)",

publisher = "IEEE Explore",

note = "International Symposium on Theoretical Aspects of Software Engineering , TASE ; Conference date: 11-12-2020 Through 13-12-2020",

}

TY - GEN

T1 - A Language-based Approach to Analysing Flow Security Properties in Virtualised Computing Systems

AU - Mu, Chunyan

PY - 2020/12/11

Y1 - 2020/12/11

N2 - This paper studies the problem of reasoning about flow security properties in virtualised computing networks with mobility from perspective of formal language. We propose a distributed process algebra CSP4v with security labelled processes for the purpose of formal modelling of virtualised computing systems. Specifically, information leakage can come from observations on process executions, communications and from cache side channels in the virtualised environment. We describe a cache flow policy to identify such flows. A type system of the language is presented to enforce the flow policy.

AB - This paper studies the problem of reasoning about flow security properties in virtualised computing networks with mobility from perspective of formal language. We propose a distributed process algebra CSP4v with security labelled processes for the purpose of formal modelling of virtualised computing systems. Specifically, information leakage can come from observations on process executions, communications and from cache side channels in the virtualised environment. We describe a cache flow policy to identify such flows. A type system of the language is presented to enforce the flow policy.

U2 - 10.1109/TASE49443.2020.00033

DO - 10.1109/TASE49443.2020.00033

M3 - Published conference contribution

SP - 185

EP - 192

BT - 2020 International Symposium on Theoretical Aspects of Software Engineering (TASE)

PB - IEEE Explore

T2 - International Symposium on Theoretical Aspects of Software Engineering

Y2 - 11 December 2020 through 13 December 2020

ER -

A Language-based Approach to Analysing Flow Security Properties in Virtualised Computing Systems

Abstract

Conference

Access to Document

Fingerprint

Cite this