Document Open Access Logo

LJGS: Gradual Security Types for Object-Oriented Languages

Authors Luminous Fennell, Peter Thiemann

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2016.9.pdf
  • Filesize: 0.76 MB
  • 26 pages

Document Identifiers

Author Details

Luminous Fennell
Peter Thiemann

Cite AsGet BibTex

Luminous Fennell and Peter Thiemann. LJGS: Gradual Security Types for Object-Oriented Languages. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 56, pp. 9:1-9:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.ECOOP.2016.9

Abstract

LJGS is a lightweight Java core calculus with a gradual security type system. The calculus guarantees secure information flow for sequential, class-based, typed object-oriented programming with mutable objects and virtual method calls. An LJGS program is composed of fragments that are checked either statically or dynamically. Statically checked fragments adhere to a security type system so that they incur no run-time penalty whereas dynamically checked fragments rely on run-time security labels. The programmer marks the boundaries between static and dynamic checking with casts so that it is always clear whether a program fragment requires run-time checks. LJGS requires security annotations on fields and methods. A field annotation either specifies a fixed static security level or it prescribes dynamic checking. A method annotation specifies a constrained polymorphic security signature. The types of local variables in method bodies are analyzed flow-sensitively and require no annotation. The dynamic checking of fields relies on a static points-to analysis to approximate implicit flows. We prove type soundness and non-interference for LJGS.
Keywords
  • gradual typing
  • security typing
  • Java
  • hybrid information flow control

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Amal Ahmed, Robert Bruce Findler, Jacob Matthews, and Philip Wadler. Blame for all. In Proceedings of the 1st Workshop on Script to Program Evolution, pages 1-13, Genova, Italy, 2009. ACM. Google Scholar
  2. Aslan Askarov, Sebastian Hunt, Andrei Sabelfeld, and David Sands. Termination-insensitive noninterference leaks more than just a bit. In Proceedings of the 13th European Symposium on Research in Computer Security: Computer Security, ESORICS '08, pages 333-348, Berlin, Heidelberg, 2008. Springer-Verlag. Google Scholar
  3. Thomas H. Austin and Cormac Flanagan. Efficient purely-dynamic information flow analysis. In Stephen Chong and David A. Naumann, editors, PLAS, pages 113-124, Dublin, Ireland, June 2009. ACM. Google Scholar
  4. Thomas H. Austin and Cormac Flanagan. Permissive dynamic information flow analysis. In Proceedings of the 5th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, PLAS '10, pages 3:1-3:12, New York, NY, USA, 2010. ACM. Google Scholar
  5. Thomas H. Austin and Cormac Flanagan. Multiple facets for dynamic information flow. In John Field and Michael Hicks, editors, Proc. 39th ACM Symp. POPL, pages 165-178, Philadelphia, USA, January 2012. ACM Press. Google Scholar
  6. Anindya Banerjee and David A. Naumann. Secure information flow and pointer confinement in a Java-like language. In CSFW, pages 253-, Cape Breton, Nova Scotia, Canada, June 2002. IEEE Computer Society. Google Scholar
  7. Gilles Barthe, David Pichardie, and Tamara Rezk. A certified lightweight non-interference Java bytecode verifier. Mathematical Structures in Computer Science, 23(5):1032-1081, 2013. Google Scholar
  8. Andrew Bedford, Josée Desharnais, Théophane G. Godonou, and Nadia Tawbi. Enforcing information flow by combining static and dynamic analysis. In Jean Luc Danger, Mourad Debbabi, Jean-Yves Marion, Joaquín García-Alfaro, and A. Nur Zincir-Heywood, editors, Foundations and Practice of Security - 6th International Symposium, FPS 2013, La Rochelle, France, October 21-22, 2013, Revised Selected Papers, volume 8352 of LNCS, pages 83-101, La Rochelle, France, October 2013. Springer. Google Scholar
  9. Deepak Chandra and Michael Franz. Fine-grained information flow analysis and enforcement in a Java virtual machine. In 23rd Annual Computer Security Applications Conference (ACSAC 2007), pages 463-475, Miami Beach, Florida, USA, December 2007. IEEE Computer Society. Google Scholar
  10. Dorothy Denning. A lattice model of secure information flow. Comm. ACM, 19(5):236-242, 1976. Google Scholar
  11. Dorothy Denning and Peter Denning. Certification of programs for secure information flow. Comm. ACM, 20(7):504-513, 1977. Google Scholar
  12. Tim Disney and Cormac Flanagan. Gradual information flow typing. In STOP, 2011. Google Scholar
  13. Luminous Fennell and Peter Thiemann. Gradual security typing with references. In Véronique Cortier and Anupam Datta, editors, CSF, pages 224-239, New Orleans, LA, USA, 2013. IEEE. Google Scholar
  14. Luminous Fennell and Peter Thiemann. Gradual typing for annotated type systems. In Zhong Shao, editor, ESOP'14, volume 8410 of Lecture Notes in Computer Science, pages 47-66, Grenoble, France, April 2014. Springer. Google Scholar
  15. Manuel Geffken and Peter Thiemann. Side effect monitoring for Java using bytecode rewriting. In Joanna Kolodziej and Bruce R. Childers, editors, PPPJ '14, pages 87-98, Cracow, Poland, September 2014. ACM. Google Scholar
  16. Daniel Hedin and Andrei Sabelfeld. A perspective on information-flow control. In 2011 Marktoberdorf Summer School. IOS Press, 2011. Google Scholar
  17. Sebastian Hunt and David Sands. On flow-sensitive security types. In Simon Peyton Jones, editor, Proc. 33rd ACM Symp. POPL, pages 79-90, Charleston, South Carolina, USA, January 2006. ACM Press. Google Scholar
  18. Uday P. Khedker, Amitabha Sanyal, and Amey Karkare. Heap reference analysis using access graphs. ACM TOPLAS, 30(1), 2007. Google Scholar
  19. Jacob Matthews and Robert Bruce Findler. Operational semantics for multi-language programs. In Matthias Felleisen, editor, Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, pages 3-10, Nice, France, January 2007. ACM Press. Google Scholar
  20. Scott Moore and Stephen Chong. Static analysis for efficient hybrid information-flow control. In CSF 2011, pages 146-160, Cernay-la-Ville, France, June 2011. IEEE Computer Society. Google Scholar
  21. Andrew C. Myers. JFlow: Practical mostly-static information flow control. In Alexander Aiken, editor, Proc. 26th ACM Symp. POPL, pages 228-241, San Antonio, Texas, USA, January 1999. ACM Press. Google Scholar
  22. François Pottier and Vincent Simonet. Information flow inference for ML. ACM TOPLAS, 25(1):117-158, January 2003. Google Scholar
  23. Alejandro Russo and Andrei Sabelfeld. Dynamic vs. static flow-sensitive security analysis. In CSF, pages 186-199. IEEE Computer Society, 2010. Google Scholar
  24. Andrei Sabelfeld and Andrew C. Myers. Language-based information-flow security. IEEE J. Selected Areas in Communications, 21(1):5-19, January 2003. Google Scholar
  25. Ilya Sergey and Dave Clarke. Gradual ownership types. In 21th European Symposium on Programming (ESOP 2012), Tallinn, Estonia, April 2012. Springer. Google Scholar
  26. Jeremy Siek and Walid Taha. Gradual typing for objects. In Erik Ernst, editor, 21st ECOOP, volume 4609 of LNCS, pages 2-27, Berlin, Germany, July 2007. Springer. Google Scholar
  27. Jeremy G. Siek and Walid Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, September 2006. Google Scholar
  28. Yannis Smaragdakis and George Balatsouras. Pointer analysis. Foundations and Trends in Programming Languages, 2(1):1-69, 2015. Google Scholar
  29. Rok Strnisa and Matthew J. Parkinson. Lightweight Java. Archive of Formal Proofs, 2011, 2011. Google Scholar
  30. Qi Sun, Anindya Banerjee, and David A. Naumann. Modular and constraint-based information flow inference for an object-oriented language. In Roberto Giacobazzi, editor, SAS 2004, volume 3148 of LNCS, pages 84-99, Verona, Italy, August 2004. Springer. Google Scholar
  31. Peter Thiemann. Gradual typing for session types. In Emilio Tuosto and Matteo Maffeis, editors, TGC, volume 8902 of LNCS, pages 144-158, Rome, Italy, September 2014. Springer. Google Scholar
  32. Sam Tobin-Hochstadt and Matthias Felleisen. Interlanguage migration: From scripts to programs. In Dynamic Languages Symposium, DLS 2006, pages 964-974, Portland, Oregon, USA, 2006. ACM. Google Scholar
  33. Sam Tobin-Hochstadt and Matthias Felleisen. The design and implementation of typed scheme. In Phil Wadler, editor, Proc. 35th ACM Symp. POPL, pages 395-406, San Francisco, CA, USA, January 2008. ACM Press. Google Scholar
  34. Philip Wadler and Robert Bruce Findler. Well-typed programs can't be blamed. In Proc. 18th ESOP, volume 5502 of LNCS, pages 1-16, York, UK, March 2009. Springer. Google Scholar
  35. Roger Wolff, Ronald Garcia, Éric Tanter, and Jonathan Aldrich. Gradual typestate. In ECOOP, volume 6813 of LNCS, pages 459-483, Lancaster, UK, 2011. Springer. Google Scholar
  36. Stephan Arthur Zdancewic. Programming Languages for Information Security. PhD thesis, Cornell, Ithaca, NY, USA, 2002. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact