Dynamic IFC Theorems for Free
作者： Jean-Philippe Bernardy , Maximilian Algehed , Catalin Hritcu
DOI:
关键词: Programming language 、 Parametricity 、 Cover (topology) 、 Soundness 、 Agda 、 Abstraction (linguistics) 、 Computer science 、 Type (model theory) 、 Proof assistant 、 Mathematical proof
摘要: We show that noninterference and transparency, the key soundness theorems for dynamic IFC libraries, can be obtained "for free", as direct consequences of more general parametricity theorem type abstraction. This allows us to give very short proofs libraries such faceted values LIO. Our stay even when fully mechanized in Agda proof assistant. Moreover, our cover actual implementations not just an abstract model.
arxiv.org
harvard.edu参考文章(43)
John C. Reynolds, Types, Abstraction and Parametric Polymorphism. ifip congress. pp. 513- 523 ,(1983)
Pablo Buiras, Amit Levy, Deian Stefan, Alejandro Russo, David Mazières, A Library for Removing Cache-Based Attacks in Concurrent Information Flow Systems trustworthy global computing. ,vol. 8358, pp. 199- 216 ,(2013) , 10.1007/978-3-319-05119-2_12
Conor McBride, Turing-completeness totally free mathematics of program construction. pp. 257- 275 ,(2015) , 10.1007/978-3-319-19797-5_13
Ana Bove, Peter Dybjer, Ulf Norell, A Brief Overview of Agda --- A Functional Language with Dependent Types theorem proving in higher order logics. ,vol. 5674, pp. 73- 78 ,(2009) , 10.1007/978-3-642-03359-9_6
JEAN-PHILIPPE BERNARDY, PATRIK JANSSON, ROSS PATERSON, Proofs for free: Parametricity for dependent types Journal of Functional Programming. ,vol. 22, pp. 107- 152 ,(2012) , 10.1017/S0956796812000056
Pablo Buiras, Alejandro Russo, Lazy Programs Leak Secrets Secure IT Systems. ,vol. 8208, pp. 116- 122 ,(2013) , 10.1007/978-3-642-41488-6_8
William J. Bowman, Amal Ahmed, Noninterference for free international conference on functional programming. ,vol. 50, pp. 101- 113 ,(2015) , 10.1145/2784731.2784733
Eugenio Moggi, Notions of computation and monads Information & Computation. ,vol. 93, pp. 55- 92 ,(1991) , 10.1016/0890-5401(91)90052-4
Deian Stefan, Alejandro Russo, John C. Mitchell, David Mazières, Flexible dynamic information flow control in Haskell Proceedings of the 4th ACM symposium on Haskell - Haskell '11. ,vol. 46, pp. 95- 106 ,(2011) , 10.1145/2034675.2034688
Luca Cardelli, Peter Wegner, On understanding types, data abstraction, and polymorphism ACM Computing Surveys. ,vol. 17, pp. 471- 523 ,(1985) , 10.1145/6041.6042