Combining type-based analysis and model checking for finding counterexamples against non-interference

ABSTRACT

Type systems for secure information flow are useful for efficiently checking that programs have secure information flow. They are, however, conservative, so that they often reject safe programs as ill-typed. Accordingly, users have to check whether the rejected programs indeed have insecure flows. To remedy this problem, we propose a method for automatically finding a counterexample of secure information flow (input states that actually lead to leakage of secret information). Our method is a novel combination of type-based analysis and model checking; Suspicious execution paths (that may cause insecure information flow) are first found by using the result of a type-based information flow analysis, and then a model checker is used to check whether the paths are indeed unsafe. We have formalized and implemented the method. The result of preliminary experiments shows that our method can often find counterexamples faster than a method using a model checker alone.

REFERENCES

• 1: Gilles Barthe , Pedro R. D'Argenio , Tamara Rezk, Secure Information Flow by Self-Composition, Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW'04), p.100, June 28-30, 2004 [doi>10.1109/CSFW.2004.17]
• 2: Jeremy Condit , Matthew Harren , Scott McPeak , George C. Necula , Westley Weimer, CCured in the real world, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 3: J. A. Goguen and J. Meseguer. Security policies and security models. In IEEE Symposium on Security and Privacy, pages 11--20, 1982.
• 4: Nevin Heintze , Jon G. Riecke, The SLam calculus: programming with secrecy and integrity, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.365-377, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268976]
• 5: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 6: Kohei Honda , Nobuko Yoshida, A uniform type structure for secure information flow, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.81-92, January 16-18, 2002, Portland, Oregon
• 7: Naoki Kobayashi, Type-based information flow analysis for the π-calculus, Acta Informatica, v.42 n.4, p.291-347, December 2005 [doi>10.1007/s00236-005-0179-x]
• 8: Peng Li , Steve Zdancewic, Practical Information-flow Control in Web-Based Information Systems, Proceedings of the 18th IEEE Computer Security Foundations Workshop (CSFW'05), p.2-15, June 20-22, 2005 [doi>10.1109/CSFW.2005.23]
• 9: Andrew C. Myers, JFlow: practical mostly-static information flow control, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.228-241, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292561]
• 10: A. C. Myers, N. Nystrom, L. Zheng, and S. Zdancewic. Jif: Java information flow. http://www.cs.cornell.edu/jif, July 2001.
• 11: George C. Necula , Scott McPeak , Shree Prakash Rahul , Westley Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, Proceedings of the 11th International Conference on Compiler Construction, p.213-228, April 08-12, 2002
• 12: George C. Necula , Scott McPeak , Westley Weimer, CCured: type-safe retrofitting of legacy code, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.128-139, January 16-18, 2002, Portland, Oregon
• 13: Y. Oiwa, S. Tatsurou, S. Eijiro, and Y. Akinori. Fail-safe ANSI-C compiler: An approach to making C programs secure: Progress report. In In International Symposium on Software Security, number 2609 in LNCS, pages 133--153. Springer-Verlag, 2002.
• 14: François Pottier , Sylvain Conchon, Information flow inference for free, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.46-57, September 2000
• 15: 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
• 16: V. Simonet. Flow Caml in a nutshell. In G. Hutton, editor, Proceedings of the first APPSEM-II workshop, pages 152--165, Nottingham, United Kingdom, March 2003.
• 17: Geoffrey Smith , Dennis Volpano, Secure information flow in a multi-threaded imperative language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.355-364, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268975]
• 18: T. Terauchi and A. Aiken. Secure information flow as a safety problem. In In Proceedings of the 12th International Static Analysis Symposium, September 2005.
• 19: H. Unno, N. Kobayashi, and A. Yonezawa. Combining type-based analysis and model checking for finding counterexamples against non-interference Full version, February 2006. Available from http://web.yl.is.s.u-tokyo.ac.jp/~uhiro/.
• 20: Dennis Volpano , Cynthia Irvine , Geoffrey Smith, A sound type system for secure flow analysis, Journal of Computer Security, v.4 n.2-3, p.167-187, Jan. 1996
• 21: Dennis M. Volpano , Geoffrey Smith, A Type-Based Approach to Program Security, Proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.607-621, April 14-18, 1997

INDEX TERMS

Primary Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Information flow controls

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Security, Theory, Verification

Keywords:
model checking, non-interference, type system