Trusted declassification:: high-level policy for a security-typed language

ABSTRACT

Security-typed languages promise to be a powerful tool with which provably secure software applications may be developed. Programs written in these languages enforce a strong, global policy of noninterferencewhich ensures that high-security data will not be observable on low-security channels. Because noninterference is typically too strong a property, most programs use some form of declassification to selectively leak high security information, e.g. when performing a password check or data encryption. Unfortunately, such a declassification is often expressed as an operation within a given program, rather than as part of a global policy, making reasoning about the security implications of a policy more difficult.In this paper, we propose a simple idea we call trusted declassification in which special declassifier functions are specified as part of the global policy. In particular, individual principals declaratively specify which declassifiers they trust so that all information flows implied by the policy can be reasoned about in absence of a particular program. We formalize our approach for a Java-like language and prove a modified form of noninterference which we call noninterference modulo trusted methods. We have implemented our approach as an extension to Jif and provide some of our experience using it to build a secure e-mail client.

REFERENCES

• 1: Askarov, A., and Sabelfeld, A Secure implementation of cryptographic protocols: A case study of mutual distrust. In Proceedings of the 10th European Symposium on Research in Computer Security (ESORICS '05) (Milan, Italy, September 2005), LNCS, Springer-Verlag.
• 2: Anindya Banerjee , David A. Naumann, Stack-based access control and secure information flow, Journal of Functional Programming, v.15 n.2, p.131-177, March 2005 [doi>10.1017/S0956796804005453]
• 3: Broberg, N., and Sands, D. Flow locks: Towards a core calculus for dynamic flow policies. In Proceedings of ESOP'06, European Symposium on Programming (Vienna, Austria, March 2006), LNCS, Springer-Verlag.
• 4: Stephen Chong , Andrew C. Myers, Security policies for downgrading, Proceedings of the 11th ACM conference on Computer and communications security, October 25-29, 2004, Washington DC, USA [doi>10.1145/1030083.1030110]
• 5: Chong, S., and Myers, A. C. Decentralized robustness. In Proceedings of the 19th IEEE Computer Security Foundations Workshop (CSFW) (Venice, July 2006). to appear.
• 6: Hicks, B., Ahmadizadeh, K., and McDaniel, P. From Languages to Systems: Understanding Practical Application Development in Security-typed Languages. Tech. Rep. NAS-TR-0035-2006, Network and Security Research Center, Department of Computer Science and Engineering, Pennsylvania State University, University Park, PA, USA, April 2006.
• 7: Hicks, B., King, D., McDaniel, P., and Hicks, M. Trusted declassification: High-level policy for a security-typed language. Tech. Rep. NAS-TR-0033-2006, Networking and Security Research Center, Department of Computer Science, Pennsylvania State University, March 2006.
• 8: Hicks, M., Tse, S., Hicks, B., and Zdancewic, S. Dynamic updating of information-flow policies. In Proceedings of the Foundations of Computer Security Workshop (FCS '05) (March 2005).
• 9: Atshushi Igarashi , Benjamin Pierce , Philip Wadler, Featherwieght Java: a minimal core calculus for Java and GJ, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.132-146, November 01-05, 1999, Denver, Colorado, United States
• 10: Peng Li , Steve Zdancewic, Downgrading policies and relaxed noninterference, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.158-170, January 12-14, 2005, Long Beach, California, USA
• 11: Mantel, H., and Sands, D. Controlled declassification based on intransitive noninterference. In Proceedings of the Asian Symposium on Programming Languages and Systems (Taipei, Taiwan, 2004), vol. 3302, Springer-Verlag, pp. 129--145.
• 12: Ana Almeida Matos , Gerard Boudol, On Declassification and the Non-Disclosure Policy, Proceedings of the 18th IEEE Computer Security Foundations Workshop (CSFW'05), p.226-240, June 20-22, 2005 [doi>10.1109/CSFW.2005.21]
• 13: A. Myers, Mostly-Static Decentralized Information Flow Control, Massachusetts Institute of Technology, Cambridge, MA, 1999
• 14: Myers, A. C., Nystrom, N., Zheng, L., and Zdancewic, S. Jif: Java + information flow. Software release. Located at http://www.cs.cornell.edu/jif, July 2001.
• 15: Andrew C. Myers , Andrei Sabelfeld , Steve Zdancewic, Enforcing robust declassification and qualified robustness, Journal of Computer Security, v.14 n.2, p.157-196, January 2006
• 16: François Pottier , Vincent Simonet, Information flow inference for ML, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.319-330, January 16-18, 2002, Portland, Oregon
• 17: Sabelfeld, A., and Myers, A. C. Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21, 1 January 2003, 5--19.
• 18: Andrei Sabelfeld , David Sands, Dimensions and Principles of Declassification, Proceedings of the 18th IEEE Computer Security Foundations Workshop (CSFW'05), p.255-269, June 20-22, 2005 [doi>10.1109/CSFW.2005.15]
• 19: Swamy, N., Hicks, M., Tse, S., and Zdancewic, S. Managing policy updates in security-typed languages, February 2006. Submitted for publication.
• 20: Tse, S., and Zdancewic, S. A design for a security-typed language with certificate-based declassification. In Proc. of the 10th European Symposium on Programming (2005), Lecture Notes in Computer Science.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Constraints

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Frameworks; Data types and structures

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Invariants; Specification techniques; Mechanical verification

  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.5 Security and Protection (D.4.6, K.4.2)

General Terms:
Design, Languages, Security, Theory

Keywords:
noninterference modolo trusted methods, FJifP, Jif, declassification, information-flow control, security policy, security-typed languages, trusted declassification