Simple Noninterference by Normalization
Pages 61 - 72
Abstract
Information-flow control (IFC) languages ensure programs preserve the confidentiality of sensitive data. Noninterference, the desired security property of such languages, states that public outputs of programs must not depend on sensitive inputs. In this paper, we show that noninterference can be proved using normalization. Unlike arbitrary terms, normal forms of programs are well-principled and obey useful syntactic properties-hence enabling a simpler proof of noninterference. Since our proof is syntax-directed, it offers an appealing alternative to traditional semantic based techniques to prove noninterference.
In particular, we prove noninterference for a static IFC calculus, based on Haskell's seclib library, using normalization. Our proof follows by straightforward induction on the structure of normal forms. We implement normalization using normalization by evaluation and prove that the generated normal forms preserve semantics. Our results have been verified in the Agda proof assistant.
References
[1]
Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon G Riecke. 1999. A core calculus of dependency. In Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, 147--160.
[2]
Andreas Abel and Christian Sattler. 2019. Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus. arXiv preprint arXiv:1902.06097 (2019).
[3]
Maximilian Algehed and Jean-Philippe Bernardy. 2019. Simple Noninterference from Parametricity. (2019).
[4]
Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. 1995. Categorical reconstruction of a reduction free normalization proof. In International Conference on Category Theory and Computer Science. Springer, 182--199.
[5]
Vincent Balat, Roberto Di Cosmo, and Marcelo Fiore. 2004. Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. In POPL, Vol. 4. 49.
[6]
Ulrich Berger, Matthias Eberl, and Helmut Schwichtenberg. 1998. Normalization by evaluation. In Prospects for Hardware Foundations. Springer, 117--137.
[7]
William J Bowman and Amal Ahmed. 2015. Noninterference for free. ACM SIGPLAN Notices, Vol. 50, 9 (2015), 101--113.
[8]
Catarina Coquand. 1993. From semantics to rules: A machine assisted analysis. In International Workshop on Computer Science Logic. Springer, 91--105.
[9]
Olivier Danvy. 1998. Type-directed partial evaluation. In DIKU International Summer School. Springer, 367--411.
[10]
Olivier Danvy, Morten Rhiger, and Kristoffer H Rose. 2001. Normalization by evaluation with typed abstract syntax. Journal of Functional Programming, Vol. 11, 6 (2001), 673--680.
[11]
Dorothy E Denning. 1976. A lattice model of secure information flow. Commun. ACM, Vol. 19, 5 (1976), 236--243.
[12]
Andrzej Filinski. 2001. Normalization by evaluation for the computational lambda-calculus. In International Conference on Typed Lambda Calculi and Applications. Springer, 151--165.
[13]
GA Kavvos. 2019. Modalities, cohesion, and information flow. Proceedings of the ACM on Programming Languages, Vol. 3, POPL (2019), 20.
[14]
Peng Li and Steve Zdancewic. 2010. Arrows for secure information flow. Theoretical computer science, Vol. 411, 19 (2010), 1974--1994.
[15]
Sam Lindley. 2005. Normalisation by evaluation in the compilation of typed functional programming languages. (2005).
[16]
Conor McBride. 2018. Everybody's got to be somewhere. Electronic Proceedings in Theoretical Computer Science, Vol. 275 (2018), 53--69.
[17]
Kenji Miyamoto and Atsushi Igarashi. 2004. A modal foundation for secure information flow. In Workshop on Foundations of Computer Security. 187--203.
[18]
Eugenio Moggi. 1989. Computational lambda-calculus and monads. In [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science. IEEE, 14--23.
[19]
Eugenio Moggi. 1991. Notions of computation and monads. Information and computation, Vol. 93, 1 (1991), 55--92.
[20]
Dominic A Orchard and Tomas Petricek. 2014. Embedding effect systems in Haskell. (2014).
[21]
Benjamin C Pierce. 2002. Types and programming languages.MIT press.
[22]
Gordon Plotkin. 1973. Lambda-definability and logical relations.Edinburgh University.
[23]
Alejandro Russo, Koen Claessen, and John Hughes. 2009. A library for light-weight information-flow security in Haskell. ACM Sigplan Notices, Vol. 44, 2 (2009), 13--24.
[24]
Deian Stefan, Alejandro Russo, John C Mitchell, and David Mazières. 2011. Flexible dynamic information flow control in Haskell. In ACM Sigplan Notices, Vol. 46. ACM, 95--106.
[25]
David Terei, Simon Marlow, Simon Peyton Jones, and David Mazières. 2012. Safe haskell. In ACM SIGPLAN Notices, Vol. 47. ACM, 137--148.
[26]
Anne Sjerp Troelstra and Helmut Schwichtenberg. 2000. Basic proof theory. Number 43. Cambridge University Press.
[27]
Stephen Tse and Steve Zdancewic. 2004. Translating dependency into parametricity. In ACM SIGPLAN Notices, Vol. 39. ACM, 115--125.
[28]
Nachiappan Valliappan and Alejandro Russo. 2019. Exponential Elimination for Bicartesian Closed Categorical Combinators. (2019).
[29]
Marco Vassena and Alejandro Russo. 2016. On formalizing information-flow control libraries. In Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security. ACM, 15--28.
[30]
Marco Vassena, Alejandro Russo, Pablo Buiras, and Lucas Waye. 2018. Mac a verified static information-flow control library. Journal of logical and algebraic methods in programming, Vol. 95 (2018), 148--180.
[31]
Philip Wadler. 1998. The marriage of effects and monads. In ACM SIGPLAN Notices, Vol. 34. ACM, 63--74.
Recommendations
Normalization for fitch-style modal calculi
Fitch-style modal lambda calculi enable programming with necessity modalities in a typed lambda calculus by extending the typing context with a delimiting operator that is denoted by a lock. The addition of locks simplifies the formulation of typing ...
Mechanized logical relations for termination-insensitive noninterference
We present an expressive information-flow control type system with recursive types, existential types, label polymorphism, and impredicative type polymorphism for a higher-order programming language with higher-order state. We give a novel semantic model ...
Simple noninterference from parametricity
In this paper we revisit the connection between parametricity and noninterference. Our primary contribution is a proof of noninterference for a polyvariant variation of the Dependency Core Calculus of in the Calculus of Constructions. The proof is ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2019 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 15 November 2019
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
- Swedish Foundation for Strategic Research (SSF)
Conference
CCS '19
Sponsor:
CCS '19: 2019 ACM SIGSAC Conference on Computer and Communications Security
November 15, 2019
London, United Kingdom
Acceptance Rates
Overall Acceptance Rate 43 of 77 submissions, 56%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 119Total Downloads
- Downloads (Last 12 months)10
- Downloads (Last 6 weeks)1
Reflects downloads up to 11 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in