An Analysis of Universal Information Flow Based on Self-Composition

Christian Müller; Máté Kovács; Helmut Seidl

doi:10.1109/CSF.2015.33

An Analysis of Universal Information Flow Based on Self-Composition

Christian Müller, Máté Kovács, Helmut Seidl

Informatics 2 - Chair of Formal Languages, Compiler Construction, Software Construction

Technical University of Munich

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

9 Scopus citations

Abstract

We introduce a novel way of proving information flow properties of a program based on its self-composition. Similarly to the universal information flow type system of Hunt and Sands, our analysis explicitly computes the dependencies of variables in the final state on variables in the initial state. Accordingly, the analysis result is independent of specific information flow lattices, and allows to derive information flow w.r.t. any of these. While our analysis runs in polynomial time, we prove that it never loses precision against the type system of Hunt and Sands, and may gain extra precision by taking similarities between different branches of conditionals into account. Also, we indicate how it can be smoothly generalized to an interprocedural analysis.

Original language	English
Title of host publication	Proceedings - 2015 IEEE 28th Computer Security Foundations Symposium, CSF 2015
Editors	Patrick Kellenberger
Publisher	IEEE Computer Society
Pages	380-393
Number of pages	14
ISBN (Electronic)	9781467375382
DOIs	https://doi.org/10.1109/CSF.2015.33
State	Published - 4 Sep 2015
Event	28th IEEE Computer Security Foundations Symposium, CSF 2015 - Verona, Italy Duration: 13 Jul 2015 → 17 Jul 2015

Publication series

Name	Proceedings of the Computer Security Foundations Workshop
Volume	2015-September
ISSN (Print)	1063-6900

Conference

Conference	28th IEEE Computer Security Foundations Symposium, CSF 2015
Country/Territory	Italy
City	Verona
Period	13/07/15 → 17/07/15

Keywords

hypersafety property
information flow control
interprocedural analysis
noninterference
weakest precondition

Access to Document

10.1109/CSF.2015.33

Cite this

Müller, C., Kovács, M., & Seidl, H. (2015). An Analysis of Universal Information Flow Based on Self-Composition. In P. Kellenberger (Ed.), Proceedings - 2015 IEEE 28th Computer Security Foundations Symposium, CSF 2015 (pp. 380-393). Article 7243746 (Proceedings of the Computer Security Foundations Workshop; Vol. 2015-September). IEEE Computer Society. https://doi.org/10.1109/CSF.2015.33

@inproceedings{cde72ffc18c740eb9263d667ab4a6c64,

title = "An Analysis of Universal Information Flow Based on Self-Composition",

abstract = "We introduce a novel way of proving information flow properties of a program based on its self-composition. Similarly to the universal information flow type system of Hunt and Sands, our analysis explicitly computes the dependencies of variables in the final state on variables in the initial state. Accordingly, the analysis result is independent of specific information flow lattices, and allows to derive information flow w.r.t. any of these. While our analysis runs in polynomial time, we prove that it never loses precision against the type system of Hunt and Sands, and may gain extra precision by taking similarities between different branches of conditionals into account. Also, we indicate how it can be smoothly generalized to an interprocedural analysis.",

keywords = "hypersafety property, information flow control, interprocedural analysis, noninterference, weakest precondition",

author = "Christian M{\"u}ller and M{\'a}t{\'e} Kov{\'a}cs and Helmut Seidl",

note = "Publisher Copyright: {\textcopyright} 2015 IEEE.; 28th IEEE Computer Security Foundations Symposium, CSF 2015 ; Conference date: 13-07-2015 Through 17-07-2015",

year = "2015",

month = sep,

day = "4",

doi = "10.1109/CSF.2015.33",

language = "English",

series = "Proceedings of the Computer Security Foundations Workshop",

publisher = "IEEE Computer Society",

pages = "380--393",

editor = "Patrick Kellenberger",

booktitle = "Proceedings - 2015 IEEE 28th Computer Security Foundations Symposium, CSF 2015",

}

Müller, C, Kovács, M & Seidl, H 2015, An Analysis of Universal Information Flow Based on Self-Composition. in P Kellenberger (ed.), Proceedings - 2015 IEEE 28th Computer Security Foundations Symposium, CSF 2015., 7243746, Proceedings of the Computer Security Foundations Workshop, vol. 2015-September, IEEE Computer Society, pp. 380-393, 28th IEEE Computer Security Foundations Symposium, CSF 2015, Verona, Italy, 13/07/15. https://doi.org/10.1109/CSF.2015.33

An Analysis of Universal Information Flow Based on Self-Composition. / Müller, Christian; Kovács, Máté; Seidl, Helmut.
Proceedings - 2015 IEEE 28th Computer Security Foundations Symposium, CSF 2015. ed. / Patrick Kellenberger. IEEE Computer Society, 2015. p. 380-393 7243746 (Proceedings of the Computer Security Foundations Workshop; Vol. 2015-September).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - An Analysis of Universal Information Flow Based on Self-Composition

AU - Müller, Christian

AU - Kovács, Máté

AU - Seidl, Helmut

PY - 2015/9/4

Y1 - 2015/9/4

N2 - We introduce a novel way of proving information flow properties of a program based on its self-composition. Similarly to the universal information flow type system of Hunt and Sands, our analysis explicitly computes the dependencies of variables in the final state on variables in the initial state. Accordingly, the analysis result is independent of specific information flow lattices, and allows to derive information flow w.r.t. any of these. While our analysis runs in polynomial time, we prove that it never loses precision against the type system of Hunt and Sands, and may gain extra precision by taking similarities between different branches of conditionals into account. Also, we indicate how it can be smoothly generalized to an interprocedural analysis.

AB - We introduce a novel way of proving information flow properties of a program based on its self-composition. Similarly to the universal information flow type system of Hunt and Sands, our analysis explicitly computes the dependencies of variables in the final state on variables in the initial state. Accordingly, the analysis result is independent of specific information flow lattices, and allows to derive information flow w.r.t. any of these. While our analysis runs in polynomial time, we prove that it never loses precision against the type system of Hunt and Sands, and may gain extra precision by taking similarities between different branches of conditionals into account. Also, we indicate how it can be smoothly generalized to an interprocedural analysis.

KW - hypersafety property

KW - information flow control

KW - interprocedural analysis

KW - noninterference

KW - weakest precondition

UR - http://www.scopus.com/inward/record.url?scp=84961368281&partnerID=8YFLogxK

U2 - 10.1109/CSF.2015.33

DO - 10.1109/CSF.2015.33

M3 - Conference contribution

AN - SCOPUS:84961368281

T3 - Proceedings of the Computer Security Foundations Workshop

SP - 380

EP - 393

BT - Proceedings - 2015 IEEE 28th Computer Security Foundations Symposium, CSF 2015

A2 - Kellenberger, Patrick

PB - IEEE Computer Society

T2 - 28th IEEE Computer Security Foundations Symposium, CSF 2015

Y2 - 13 July 2015 through 17 July 2015

ER -

An Analysis of Universal Information Flow Based on Self-Composition

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this