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

Informatik 2 - Lehrstuhl für Sprachen und Beschreibungsstrukturen in der Informatik

TUM - Lehrstuhl für Architekturinformatik, Prof. Dr.-Ing. Frank Petzold

Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

8 Zitate (Scopus)

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.

Originalsprache	Englisch
Titel	Proceedings - 2015 IEEE 28th Computer Security Foundations Symposium, CSF 2015
Redakteure/-innen	Patrick Kellenberger
Herausgeber (Verlag)	IEEE Computer Society
Seiten	380-393
Seitenumfang	14
ISBN (elektronisch)	9781467375382
DOIs	https://doi.org/10.1109/CSF.2015.33
Publikationsstatus	Veröffentlicht - 4 Sept. 2015
Veranstaltung	28th IEEE Computer Security Foundations Symposium, CSF 2015 - Verona, Italien Dauer: 13 Juli 2015 → 17 Juli 2015

Publikationsreihe

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

Konferenz

Konferenz	28th IEEE Computer Security Foundations Symposium, CSF 2015
Land/Gebiet	Italien
Ort	Verona
Zeitraum	13/07/15 → 17/07/15

Zugriff auf Dokument

10.1109/CSF.2015.33

Andere Dateien und Links

Verknüpfung zur Publikation in Scopus

Dieses zitieren

Müller, C., Kovács, M., & Seidl, H. (2015). An Analysis of Universal Information Flow Based on Self-Composition. in P. Kellenberger (Hrsg.), Proceedings - 2015 IEEE 28th Computer Security Foundations Symposium, CSF 2015 (S. 380-393). Artikel 7243746 (Proceedings of the Computer Security Foundations Workshop; Band 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 (Hrsg.), Proceedings - 2015 IEEE 28th Computer Security Foundations Symposium, CSF 2015., 7243746, Proceedings of the Computer Security Foundations Workshop, Bd. 2015-September, IEEE Computer Society, S. 380-393, 28th IEEE Computer Security Foundations Symposium, CSF 2015, Verona, Italien, 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. Hrsg. / Patrick Kellenberger. IEEE Computer Society, 2015. S. 380-393 7243746 (Proceedings of the Computer Security Foundations Workshop; Band 2015-September).

Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

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

Publikationsreihe

Konferenz

Zugriff auf Dokument

Andere Dateien und Links

Fingerprint

Dieses zitieren