William J. Bowman
Amal Ahmed
ABSTRACT
The dependency core calculus (DCC) is a framework for studying a variety of dependency analyses (e.g., secure information flow). The key property provided by DCC is noninterference, which guarantees that a low-level observer (attacker) cannot distinguish high-level (protected) computations. The proof of noninterference for DCC suggests a connection to parametricity in System F, which suggests that it should be possible to implement dependency analyses in languages with parametric polymorphism. We present a translation from DCC into Fω and prove that the translation preserves noninterference. To express noninterference in Fω, we define a notion of observer-sensitive equivalence that makes essential use of both first-order and higher-order polymorphism. Our translation provides insights into DCC's type system and shows how DCC can be implemented in a polymorphic language without loss of the noninterference (security) guarantees available in DCC. Our contributions include proof techniques that should be valuable when proving other secure compilation or full abstraction results.
- M. Abadi. Protection in programming-language translations. In ICALP 1998. Google Scholar
Digital Library
- M. Abadi, A. Banerjee, N. Heintze, and J. G. Riecke. A core calculus of dependency. In POPL 1999. Google ScholarDigital Library
- A. Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In ESOP 2006. Google ScholarDigital Library
- A. Ahmed and M. Blume. Typed closure conversion preserves observational equivalence. In ICFP 2008. Google ScholarDigital Library
- A. Ahmed and M. Blume. An equivalence-preserving CPS translation via multi-language semantics. In ICFP 2011. Google ScholarDigital Library
- J. Berdine, P. O’Hearn, U. Reddy, and H. Thielecke. Linear continuation-passing. Higher Order Symbol. Comput., 15(2-3):181– 208, 2002. Google ScholarDigital Library
- W. J. Bowman and A. Ahmed. Noninterference for free (technical appendix). June 2015. URL https://perma.cc/RJ9N-B5ZQ.Google Scholar
- A. Chlipala. A certified type-preserving compiler from lambda calculus to assembly language. In PLDI 2007 Google ScholarDigital Library
- C. Fournet, N. Swamy, J. Chen, P.-E. Dagand, P.-Y. Strub, and B. Livshits. Fully abstract compilation to JavaScript. In POPL 2013. Google ScholarDigital Library
- N. C. Heintze and J. G. Riecke. The SLam Calculus: Programming with secrecy and integrity. In POPL 1998. Google ScholarDigital Library
- A. Kennedy. Securing the .NET programming model. In APPSEM II Workshop, Industrial Applications Session, Sept. 2005.Google Scholar
- J. Matthews and R. B. Findler. Operational semantics for multilanguage programs. In POPL 2007. Google ScholarDigital Library
- E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92, 1991. Google ScholarDigital Library
- J. T. Perconti and A. Ahmed. Verifying an open compiler using multilanguage semantics. In ESOP 2014.Google Scholar
- B. C. Pierce. Types and Programming Languages, chapter 30: Higher-Order Polymorphism. MIT Press, 2002. Google ScholarDigital Library
- J. C. Reynolds. Types, abstraction, and parametric polymorphism. Information Processing, pages 513–523, 1983.Google Scholar
- N. Shikuma and A. Igarashi. Proving noninterference by a fully complete translation to the simply typed lambda-calculus. In 11th Asian conference on advances in computer science, 2007. Google ScholarDigital Library
- N. Shikuma and A. Igarashi. Proving noninterference by a fully complete translation to the simply typed lambda-calculus. Logical Methods in Computer Science, 4(3:10):1–31, 2008.Google Scholar
- S. Tse and S. Zdancewic. Translating dependency into parametricity. In ICFP 2004. Google ScholarDigital Library
- D. Vytiniotis and S. Weirich. Parametricity, type equality, and higherorder polymorphism. J. Funct. Programming, 20(2):175–210, Mar. 2010. Google ScholarDigital Library
- P. Wadler. Theorems for free! In ACM Symp. on Functional Programming Languages and Computer Architecture (FPCA), Sept. 1989. Google ScholarDigital Library
- J. Zhao, Q. Zhang, and S. Zdancewic. Relational parametricity for a polymorphic linear lambda calculus. In APLAS 2010. Google ScholarDigital Library
Index Terms
- Noninterference for free
Recommendations
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 ...
Translating dependency into parametricity
ICFP '04Abadi et al. introduced the dependency core calculus (DCC) as a unifying framework to study many important program analyses such as binding time, information flow, slicing, and function call tracking. DCC uses a lattice of monads and a nonstandard ...
Noninterference for free
ICFP '15The dependency core calculus (DCC) is a framework for studying a variety of dependency analyses (e.g., secure information flow). The key property provided by DCC is noninterference, which guarantees that a low-level observer (attacker) cannot ...
Comments