Type-Driven Gradual Security with References

Abstract

In security-typed programming languages, types statically enforce noninterference between potentially conspiring values, such as the arguments and results of functions. But to adopt static security types, like other advanced type disciplines, programmers face a steep wholesale transition, often forcing them to refactor working code just to satisfy their type checker. To provide a gentler path to security typing that supports safe and stylish but hard-to-verify programming idioms, researchers have designed languages that blend static and dynamic checking of security types. Unfortunately, most of the resulting languages only support static, type-based reasoning about noninterference if a program is entirely statically secured. This limitation substantially weakens the benefits that dynamic enforcement brings to static security typing. Additionally, current proposals are focused on languages with explicit casts and therefore do not fulfill the vision of gradual typing, according to which the boundaries between static and dynamic checking only arise from the (im)precision of type annotations and are transparently mediated by implicit checks.

In this article, we present GSL_Ref, a gradual security-typed higher-order language with references. As a gradual language, GSL_Ref supports the range of static-to-dynamic security checking exclusively driven by type annotations, without resorting to explicit casts. Additionally, GSL_Ref lets programmers use types to reason statically about termination-insensitive noninterference in all programs, even those that enforce security dynamically. We prove that GSL_Ref satisfies all but one of Siek et al.’s criteria for gradually-typed languages, which ensure that programs can seamlessly transition between simple typing and security typing. A notable exception regards the dynamic gradual guarantee, which some specific programs must violate if they are to satisfy noninterference; it remains an open question whether such a language could fully satisfy the dynamic gradual guarantee. To realize this design, we were led to draw a sharp distinction between syntactic type safety and semantic type soundness, each of which constrains the design of the gradual language.

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 (POPL’99). ACM, New York, NY, 147--160.
2. Amal Ahmed. 2004. Semantics of Types for Mutable State. Ph.D. Dissertation. Princeton University.
3. Amal Ahmed, Robert Bruce Findler, Jeremy Siek, and Philip Wadler. 2011. Blame for all. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’11). ACM Press, Austin, Texas, 201--214.
4. Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler. 2017. Theorems for free for free: Parametricity, with and without types. In Proceedings of the 22th ACM SIGPLAN Conference on Functional Programming (ICFP’17). ACM Press, Oxford, UK, 39:1--39:28.
5. Thomas H. Austin and Cormac Flanagan. 2009. Efficient purely dynamic information flow analysis. In Proceedings of the 2009 Workshop on Programming Languages and Analysis for Security (PLAS’09). 113--124.
6. Thomas H. Austin and Cormac Flanagan. 2010. Permissive dynamic information flow analysis. In Proceedings of the 2010 Workshop on Programming Languages and Analysis for Security (PLAS’10). 3:1--3:12.
7. Thomas H. Austin and Cormac Flanagan. 2012. Multiple facets for dynamic information flow. ACM SIGPLAN Notices 47, 1 (Jan. 2012), 165--178.
8. Thomas H. Austin, Tommy Schmitz, and Cormac Flanagan. 2017. Multiple facets for dynamic information flow with exceptions. ACM Trans. Program. Lang. Syst. 39, 3 (July 2017), 10:1--10:56.
9. Felipe Bañados Schwerter, Ronald Garcia, and Éric Tanter. 2014. A theory of gradual effect systems. In Proceedings of the 19th ACM SIGPLAN Conference on Functional Programming (ICFP’14). ACM Press, Gothenburg, Sweden, 283--295.
10. Felipe Bañados Schwerter, Ronald Garcia, and Éric Tanter. 2016. Gradual type-and-effect systems. J. Funct. Program. 26 (Sept. 2016), 19:1--19:69.
11. Kenneth J. Biba. 1977. Integrity Considerations for Secure Computer Systems. Technical Report ESD-TR-76-372. USAF Electronic Systems Division, Bedford, MA.
12. Pablo Buiras, Dimitrios Vytiniotis, and Alejandro Russo. 2015. HLIO: Mixing static and dynamic typing for information-flow control in Haskell. In Proceedings of the 20th ACM SIGPLAN Conference on Functional Programming (ICFP’15). ACM Press, Vancouver, Canada, 289--301.
13. Giuseppe Castagna and Victor Lanvin. 2017. Gradual typing with union and intersection types. In Proceedings of the 22th ACM SIGPLAN Conference on Functional Programming (ICFP’17). ACM Press, Oxford, United Kingdom, 41:1--41:28.
14. D. Chandra and M. Franz. 2007. Fine-grained information flow analysis and enforcement in a Java virtual machine. In Proceedings of the 23rd Annual Computer Security Applications Conference (ACSAC’07). 463--475.
15. Alonzo Church. 1940. A formulation of the simple theory of types. J. Symbol. Logic 5, 2 (06 1940), 56--68.
16. Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM Symposium on Principles of Programming Languages (POPL’77). ACM Press, Los Angeles, CA, 238--252.
17. Dorothy E. Denning. 1976. A lattice model of secure information flow. Commun. ACM 19, 5 (May 1976), 236--243.
18. Tim Disney and Cormac Flanagan. 2011. Gradual information flow typing. In Proceedings of the International Workshop on Scripts to Programs.
19. Luminous Fennell and Peter Thiemann. 2013. Gradual security typing with references. In Proceedings of the Computer Security Foundations Symposium. 224--239.
20. Luminous Fennell and Peter Thiemann. 2016. LJGS: Gradual security types for object-oriented languages. In Proceedings of the 30th European Conference on Object-oriented Programming (ECOOP’16) (LNCS). Springer-Verlag, Rome, Italy.
21. Ronald Garcia and Matteo Cimini. 2015. Principal type schemes for gradual programs. In Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’15). ACM Press, 303--315.
22. Ronald Garcia, Alison M. Clark, and Éric Tanter. 2016. Abstracting gradual typing. In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’16). ACM Press, St Petersburg, FL, 429--442.
23. Ronald Garcia and Éric Tanter. 2015. Deriving a Simple Gradual Security Language. Retrieved from http://arxiv.org/abs/1511.01399.
24. Ronald Garcia, Éric Tanter, Roger Wolff, and Jonathan Aldrich. 2014. Foundations of typestate-oriented programming. ACM Trans. Program. Lang. Syst. 36, 4, Article 12 (Oct. 2014), 12:1--12:44 pages.
25. David K. Gifford and John M. Lucassen. 1986. Integrating functional and imperative programming. In Proceedings of the 1986 ACM Conference on Lisp and Functional Programming. ACM Press, Cambridge, MA, 28--38.
26. Joseph A. Goguen and José Meseguer. 1982. Security policies and security models. In Proceedings of the 1982 IEEE Symposium on Security and Privacy. 11--20.
27. Daniel Hedin and Andrei Sabelfeld. 2012a. Information-flow security for a core of JavaScript. In Proceedings of the 25th IEEE Computer Security Foundations Symposium (CSF’12). 3--18.
28. Daniel Hedin and Andrei Sabelfeld. 2012b. A perspective on information-flow control. In NATO Science for Peace and Security Series D: Information and Communication Security. IOS Press, 319--347.
29. Nevin Heintze and Jon G. Riecke. 1998. The SLam calculus: Programming with secrecy and integrity. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’98). ACM, New York, NY, 365--377.
30. William A. Howard. 1980. The formulae-as-types notion of construction. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, J. P. Seldin and J. R. Hindley (Eds.). Academic Press, New York, 479--490. Reprint of 1969 article.
31. Sebastian Hunt and David Sands. 2006. On flow-sensitive security types. In Proceedings of the 33th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’06). ACM Press, Charleston, SC, 79--90.
32. Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi. 2017. On polymorphic gradual typing. In Proceedings of the 22th ACM SIGPLAN Conference on Functional Programming (ICFP’17). ACM Press, Oxford, UK, 40:1--40:29.
33. Khurram A. Jafery and Joshua Dunfield. 2017. Sums of uncertainty: Refinements go gradual. In Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’17). ACM Press, Paris, France, 804--817.
34. Kenneth Knowles and Cormac Flanagan. 2010. Hybrid type checking. ACM Trans. Program. Lang. Syst. 32, 2 (2010).
35. Nico Lehmann and Éric Tanter. 2017. Gradual refinement types. In Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’17). ACM Press, Paris, France, 775--788.
36. Scott Moore and Stephen Chong. 2011. Static analysis for efficient hybrid information-flow control. In Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF’11). Cernay-la-Ville, France, 146--160.
37. Andrew C. Myers. 1999. JFlow: Practical mostly static information flow control. In Proceedings of the 26th ACM Symposium on Principles of Programming Languages (POPL’99). ACM Press, San Antonio, TX, 228--241.
38. Andrew C. Myers and Barbara Liskov. 1997. A decentralized model for information flow control. In Proceedings of the 16th ACM Symposium on Operating System Principles (SOSP’97). 129--142.
39. Andrew C. Myers and Barbara Liskov. 2000. Protecting privacy using the decentralized label model. ACM Trans. Softw. Eng. Methodol. 9 (Oct. 2000), 410--442. Issue 4.
40. François Pottier and Vincent Simonet. 2003. Information flow inference for ML. ACM Trans. Program. Lang. Syst. 25, 1 (Jan. 2003), 117--158.
41. John C. Reynolds. 1983. Types, abstraction and parametric polymorphism. In Proceedings of the IFIP Congress. 513--523.
42. Alejandro Russo and Andrei Sabelfeld. 2010. Dynamic vs. static flow-sensitive security analysis. In Proceedings of the 2010 23rd IEEE Computer Security Foundations Symposium (CSF’10). IEEE Computer Society, Washington, DC, 186--199.
43. Andrei Sabelfeld and Andrew C. Myers. 2003. Language-based information-flow security. IEEE J. Select. Areas Commun. 21, 1 (Jan. 2003).
44. Andrei Sabelfeld and David Sands. 2009. Declassification: Dimensions and principles. J. Comput. Secur. 17, 5 (2009), 517--548.
45. Ilya Sergey and Dave Clarke. 2012. Gradual ownership types. In Proceedings of the 21st European Symposium on Programming Languages and Systems (ESOP’12) (LNCS), Helmut Seidl (Ed.), Vol. 7211. Springer-Verlag, Tallinn, Estonia, 579--599.
46. Paritosh Shroff, Scott Smith, and Mark Thober. 2007. Dynamic dependency monitoring to secure information flow. In Proceedings of the 20th IEEE Computer Security Foundations Symposium (CSF’07). IEEE Computer Society, Washington, DC, 203--217.
47. Jeremy Siek and Walid Taha. 2007. Gradual typing for objects. In Proceedings of the 21st European Conference on Object-oriented Programming (ECOOP’07) (LNCS), Erik Ernst (Ed.). Springer-Verlag, Berlin, 2--27.
48. Jeremy Siek and Philip Wadler. 2010. Threesomes, with and without blame. In Proceedings of the 37th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’10). ACM Press, 365--376.
49. Jeremy G. Siek and Walid Taha. 2006. Gradual typing for functional languages. In Proceedings of the Scheme and Functional Programming Workshop. 81--92.
50. Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015. Refined criteria for gradual typing. In Proceedings of the 1st Summit on Advances in Programming Languages (SNAPL’15). 274--293.
51. Deian Stefan, David Mazières, John C. Mitchell, and Alejandro Russo. 2017. Flexible dynamic information flow control in the presence of exceptions. J. Funct. Program. 27 (2017).
52. Peter Thiemann and Luminous Fennell. 2014. Gradual typing for annotated type systems. In Proceedings of the 23rd European Symposium on Programming Languages and Systems (ESOP’14) (LNCS), Zhong Shao (Ed.), Vol. 8410. Springer-Verlag, Grenoble, France, 47--66.
53. Matías Toro, Ronald Garcia, and Éric Tanter. 2018. Type-Driven Gradual Security with References: Complete Definitions and Proofs. Technical Report TR/DCC-2018-4. University of Chile.
54. Matías Toro and Éric Tanter. 2015. Customizable gradual polymorphic effects for Scala. In Proceedings of the 30th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA’15). ACM Press, Pittsburgh, PA, 935--953.
55. Matías Toro and Éric Tanter. 2017. A gradual interpretation of union types. In Proceedings of the 24th Static Analysis Symposium (SAS’17) (Lecture Notes in Computer Science), Vol. 10422. Springer-Verlag, New York City, NY, 382--404.
56. Dennis Volpano, Cynthia Irvine, and Geoffrey Smith. 1996. A sound type system for secure flow analysis. J. Comput. Secur. 4, 2--3 (Jan. 1996), 167--187.
57. Philip Wadler. 1989. Theorems for free! In Proceedings of the 4th International Conference on Functional Programming Languages and Computer Architecture (FPCA’89). ACM, New York, NY, 347--359.
58. Roger Wolff, Ronald Garcia, Éric Tanter, and Jonathan Aldrich. 2011. Gradual typestate. In Proceedings of the 25th European Conference on Object-oriented Programming (ECOOP’11) (LNCS), Mira Mezini (Ed.), Vol. 6813. Springer-Verlag, Lancaster, UK, 459--483.
59. Steve Zdancewic. 2002. Programming Languages for Information Security. Ph.D. Dissertation. Cornell University.
60. Steve Zdancewic and Andrew C. Myers. 2001. Secure information flow and CPS. In Proceedings of the 10th European Symposium on Programming, Vol. 2028. 46--61.
61. Lantian Zheng and Andrew C. Myers. 2007. Dynamic security labels and noninterference. Int. J. Info. Secur. 6, 2 (Mar. 2007), 67--84.

Index Terms

• Security and privacy

  • Systems security

    • Information flow control

• Theory of computation

  • Semantics and reasoning

    • Program constructs

      • Type structures

    • Program semantics