An algebraic approach for reasoning about information flow

Arthur Américo, Mário S. Alvim, Annabelle McIver

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionResearchpeer-review

Abstract

This paper concerns the analysis of information leaks in security systems. We address the problem of specifying and analyzing large systems in the (standard) channel model used in quantitative information flow (QIF). We propose several operators which match typical interactions between system components. We explore their algebraic properties with respect to the security-preserving refinement relation defined by Alvim et al. and McIver et al. [1, 2]. We show how the algebra can be used to simplify large system specifications in order to facilitate the computation of information leakage bounds. We demonstrate our results on the specification and analysis of the Crowds Protocol. Finally, we use the algebra to justify a new algorithm to compute leakage bounds for this protocol.

LanguageEnglish
Title of host publicationFormal Methods
Subtitle of host publication22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
EditorsKlaus Havelund, Jan Peleska, Bill Roscoe, Erik de Vink
Place of PublicationCham
PublisherSpringer, Springer Nature
Pages55-72
Number of pages18
ISBN (Electronic)9783319955827
ISBN (Print)9783319955810
DOIs
Publication statusPublished - 1 Jan 2018
Event22nd International Symposium on Formal Methods, FM 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, United Kingdom
Duration: 15 Jul 201817 Jul 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10951 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference22nd International Symposium on Formal Methods, FM 2018 Held as Part of the Federated Logic Conference, FloC 2018
CountryUnited Kingdom
CityOxford
Period15/07/1817/07/18

Fingerprint

Algebraic Approach
Information Flow
Algebra
Reasoning
Specifications
Security systems
Leakage
Specification
Channel Model
Justify
Standard Model
Simplify
Refinement
Operator
Interaction
Demonstrate

Cite this

Américo, A., Alvim, M. S., & McIver, A. (2018). An algebraic approach for reasoning about information flow. In K. Havelund, J. Peleska, B. Roscoe, & E. de Vink (Eds.), Formal Methods: 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings (pp. 55-72). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10951 LNCS). Cham: Springer, Springer Nature. https://doi.org/10.1007/978-3-319-95582-7_4
Américo, Arthur ; Alvim, Mário S. ; McIver, Annabelle. / An algebraic approach for reasoning about information flow. Formal Methods: 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. editor / Klaus Havelund ; Jan Peleska ; Bill Roscoe ; Erik de Vink. Cham : Springer, Springer Nature, 2018. pp. 55-72 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{7cd9d1808fa34f47bab7a4541078ddda,
title = "An algebraic approach for reasoning about information flow",
abstract = "This paper concerns the analysis of information leaks in security systems. We address the problem of specifying and analyzing large systems in the (standard) channel model used in quantitative information flow (QIF). We propose several operators which match typical interactions between system components. We explore their algebraic properties with respect to the security-preserving refinement relation defined by Alvim et al. and McIver et al. [1, 2]. We show how the algebra can be used to simplify large system specifications in order to facilitate the computation of information leakage bounds. We demonstrate our results on the specification and analysis of the Crowds Protocol. Finally, we use the algebra to justify a new algorithm to compute leakage bounds for this protocol.",
author = "Arthur Am{\'e}rico and Alvim, {M{\'a}rio S.} and Annabelle McIver",
year = "2018",
month = "1",
day = "1",
doi = "10.1007/978-3-319-95582-7_4",
language = "English",
isbn = "9783319955810",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer, Springer Nature",
pages = "55--72",
editor = "Klaus Havelund and Jan Peleska and Bill Roscoe and {de Vink}, Erik",
booktitle = "Formal Methods",
address = "United States",

}

Américo, A, Alvim, MS & McIver, A 2018, An algebraic approach for reasoning about information flow. in K Havelund, J Peleska, B Roscoe & E de Vink (eds), Formal Methods: 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10951 LNCS, Springer, Springer Nature, Cham, pp. 55-72, 22nd International Symposium on Formal Methods, FM 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, United Kingdom, 15/07/18. https://doi.org/10.1007/978-3-319-95582-7_4

An algebraic approach for reasoning about information flow. / Américo, Arthur; Alvim, Mário S.; McIver, Annabelle.

Formal Methods: 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. ed. / Klaus Havelund; Jan Peleska; Bill Roscoe; Erik de Vink. Cham : Springer, Springer Nature, 2018. p. 55-72 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10951 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionResearchpeer-review

TY - GEN

T1 - An algebraic approach for reasoning about information flow

AU - Américo,Arthur

AU - Alvim,Mário S.

AU - McIver,Annabelle

PY - 2018/1/1

Y1 - 2018/1/1

N2 - This paper concerns the analysis of information leaks in security systems. We address the problem of specifying and analyzing large systems in the (standard) channel model used in quantitative information flow (QIF). We propose several operators which match typical interactions between system components. We explore their algebraic properties with respect to the security-preserving refinement relation defined by Alvim et al. and McIver et al. [1, 2]. We show how the algebra can be used to simplify large system specifications in order to facilitate the computation of information leakage bounds. We demonstrate our results on the specification and analysis of the Crowds Protocol. Finally, we use the algebra to justify a new algorithm to compute leakage bounds for this protocol.

AB - This paper concerns the analysis of information leaks in security systems. We address the problem of specifying and analyzing large systems in the (standard) channel model used in quantitative information flow (QIF). We propose several operators which match typical interactions between system components. We explore their algebraic properties with respect to the security-preserving refinement relation defined by Alvim et al. and McIver et al. [1, 2]. We show how the algebra can be used to simplify large system specifications in order to facilitate the computation of information leakage bounds. We demonstrate our results on the specification and analysis of the Crowds Protocol. Finally, we use the algebra to justify a new algorithm to compute leakage bounds for this protocol.

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

U2 - 10.1007/978-3-319-95582-7_4

DO - 10.1007/978-3-319-95582-7_4

M3 - Conference proceeding contribution

SN - 9783319955810

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 55

EP - 72

BT - Formal Methods

PB - Springer, Springer Nature

CY - Cham

ER -

Américo A, Alvim MS, McIver A. An algebraic approach for reasoning about information flow. In Havelund K, Peleska J, Roscoe B, de Vink E, editors, Formal Methods: 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Cham: Springer, Springer Nature. 2018. p. 55-72. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-95582-7_4