Luísa Lourenço
ABSTRACT
In this paper, we develop a novel notion of dependent information flow types. Dependent information flow types fit within the standard framework of dependent type theory, but, unlike usual dependent types, crucially allow the security level of a type, rather than just the structural data type itself, to depend on runtime values.
Our dependent function and dependent sum information flow types provide a direct, natural and elegant way to express and enforce fine grained security policies on programs, including programs that manipulate structured data types in which the security level of a structure field may depend on values dynamically stored in other fields, still considered a challenge to security enforcement in software systems such as data-centric web-based applications.
We base our development on the very general setting of a minimal lambda-calculus with references and collections. We illustrate its expressiveness, showing how secure operations on relevant scenarios can be modelled and analysed using our dependent information flow type system, which is also shown to be amenable to algorithmic type checking. Our main results include type-safety and non-interference theorems ensuring that well-typed programs do not violate prescribed security policies.
Supplemental Material
- M. Abadi, A. Banerjee, N. Heintze, and J. G. Riecke:. A Core Calculus of Dependency. In POPL 1999. Google Scholar
Digital Library
- O. Arden, M. D. George, J. Liu, K. Vikram, A. Askarov, and A. C. Myers. Sharing mobile code securely with information flow control. In IEEE SSP 2012. Google ScholarDigital Library
- G. M. Bierman, A. D. Gordon, C. Hritcu, and D. E. Langworthy. Semantic Subtyping with an SMT Solver. J. Funct. Program., 2012. Google ScholarDigital Library
- A. Chlipala. Static Checking of Dynamically-Varying Security Policies in Database-Backed Applications. In USENIX OSDI 2010. Google ScholarDigital Library
- B. J. Corcoran, N. Swamy, and M. W. Hicks. Cross-tier, Label-based Security Enforcement for Web Applications. In ACM SIGMOD Int. Conf. on Management of Data, 2009. Google ScholarDigital Library
- B. Davis and H. Chen. DBTaint: Cross-Application Information Flow Tracking via Databases. In USENIX WebApps 2010. Google ScholarDigital Library
- L. M. de Moura and N. Bjørner. Z3: An efficient smt solver. In TACAS 2008. Google ScholarDigital Library
- D. E. Denning and P. J. Denning. Certification of Programs for Secure Information Flow. Comm. of the ACM, 1977. Google ScholarDigital Library
- W. Enck, P. Gilbert, B. Chun, L. P. Cox, J. Jung, P. M., and A. Sheth. TaintDroid: An Information-Flow Tracking System for Realtime Privacy Monitoring on Smartphones. In USENIX OSDI 2010. Google ScholarDigital Library
- J. A. Goguen and J. Meseguer. Security Policies and Security Models. In IEEE SSP 1982.Google Scholar
- D. Hedin and A. Sabelfeld. Information-Flow Security for a Core of JavaScript. In IEEE CSF 2012. Google ScholarDigital Library
- N. Heintze and J. G. Riecke. The SLam Calculus: Programming with Secrecy and Integrity. In POPL 1998. Google ScholarDigital Library
- K. Honda, V. T. Vasconcelos, and N. Yoshida. Secure information flow as typed process behaviour. In ESOP 2000, LNCS. Google ScholarDigital Library
- C. Hritcu, M. Greenberg, B. Karel, B. C. Pierce, and G. Morrisett. All your ifcexception are belong to us. In IEEE SSP 2013. Google ScholarDigital Library
- P. Li and S. Zdancewic. Practical information-flow control in web-based information systems. In IEEE CSFW 2005. Google ScholarDigital Library
- J. Liu, M. D. George, K. Vikram, X. Qi, L. Waye, and A. C. Myers. Fabric: a platform for secure distributed computation and storage. In ACM SOSP 2009. Google ScholarDigital Library
- L. Lourenço and L. Caires. Information Flow Analysis for Valued-Indexed Data Security Compartments. In TGC 2013.Google Scholar
- A. C. Myers. JFlow: Practical Mostly-Static Information Flow Control. In POPL 1999. Google ScholarDigital Library
- A. C. Myers and B. Liskov. A Decentralized Model for Information Flow Control. In ACM SOSP 1997. Google ScholarDigital Library
- A. Nanevski, A. Banerjee, and D. Garg. Verification of Information Flow and Access Control Policies with Dependent Types. In IEEE SSP 2011. Google ScholarDigital Library
- F. Pottier and V. Simonet. Information flow inference for ML. In POPL 2002. Google ScholarDigital Library
- A. Sabelfeld and A. C. Myers. Language-Based Information-Flow Security. IEEE JSAC, 21(1):5--19, Jan. 2003. Google ScholarDigital Library
- A. Sabelfeld and D. Sands. A Per Model of Secure Information Flow in Sequential Programs. Higher-Order and Symbolic Computation, 2001. Google ScholarDigital Library
- N. Swamy, B. J. Corcoran, and M. Hicks. Fable: A language for enforcing user-defined security policies. In IEEE SSP 2008. Google ScholarDigital Library
- N. Swamy, J. Chen, and R. Chugh. Enforcing Stateful Authorization and Information Flow Policies in Fine. In ESOP 2010. Google ScholarDigital Library
- N. Swamy, J. Chen, C. Fournet, P. Strub, K. Bhargavan, and J. Yang. Secure Distributed Programming with Value-dependent Types. In ICFP 2011. Google ScholarDigital Library
- S. Tse and S. Zdancewic. Run-time Principals in Information-flow Type Systems. ACM Trans. Program. Lang. Syst., 2007. Google ScholarDigital Library
- D. M. Volpano, C. E. Irvine, and G. Smith. A Sound Type System for Secure Flow Analysis. Journal of Computer Security, 1996. Google ScholarDigital Library
- H. Xi and F. Pfenning. Dependent Types in Practical Programming. In POPL 1999. Google ScholarDigital Library
- S. Zdancewic and A. C. Myers. Observational determinism for concurrent program security. In IEEE CSFW 2003.Google ScholarCross Ref
- N. Zeldovich, S. Boyd-Wickizer, and D. Mazières. Securing Distributed Systems with Information Flow Control. In USENIX NSDI 2008. Google ScholarDigital Library
- L. Zheng and A. C. Myers. Dynamic Security Labels and Static Information Flow Control. Int. J. Inf. Sec., 2007. Google ScholarDigital Library
- G. Barthe, C. Fournet, B. Grégoire, P. Strub, N. Swamy and S. Z. Béguelin. Probabilistic relational verification for cryptographic implementations. In POPL 2014. Google ScholarDigital Library
- L. Lourenço and L. Caires. Dependent Information Flow Types. Technical report, UNL, 2014.Google Scholar
- DIFT Prototype. http://ctp.di.fct.unl.pt/DIFTprototype.Google Scholar
Index Terms
- Dependent Information Flow Types
Recommendations
Verification of Information Flow and Access Control Policies with Dependent Types
SP '11: Proceedings of the 2011 IEEE Symposium on Security and PrivacyWe present Relational Hoare Type Theory (RHTT), a novel language and verification system capable of expressing and verifying rich information flow and access control policies via dependent types. We show that a number of security policies which have ...
Composing polymorphic information flow systems with reference immutability
FTfJP '13: Proceedings of the 15th Workshop on Formal Techniques for Java-like ProgramsInformation flow type systems, such as EnerJ (a type system for energy efficiency), and integrity and confidentiality, are unsound if subtyping for references is allowed because of the presence of mutable references. The standard approach is to disallow ...
Martin-Löf à la Coq
CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and ProofsWe present an extensive mechanization of the metatheory of Martin-Löf Type Theory (MLTT) in the Coq proof assistant. Our development builds on pre-existing work in Agda to show not only the decidability of conversion, but also the decidability of type ...
Comments