Effective blame for information-flow violations

ABSTRACT

Programs trusted with secure information should not release that information in ways contrary to system policy. However, when a program contains an illegal flow of information, current information-flow reporting techniques are inadequate for determining the cause of the error. Reasoning about information-flow errors can be difficult, as the flows involved can be quite subtle. We present a general model for information-flow blame that can explain the source of such security errors in code. This model is implemented by changing the information-flow verification procedure to: (1) generate supplementary information to reveal otherwise hidden program dependencies; (2) modify the constraint solver to construct a blame dependency graph; and (3) develop an explanation procedure that returns a complete and minimal error report. Our experiments show that information-flow errors can generally be explained and resolved by viewing only a small fraction of the total code.

REFERENCES

• 1: T.J. Watson Libraries for Analysis. http://wala.sourceforge.net.
• 2: Askarov, A., and Sabelfeld, A. Secure implementation of cryptographic protocols: A case study of mutual distrust. In ESORICS '05.
• 3: Thomas Ball , Mayur Naik , Sriram K. Rajamani, From symptom to cause: localizing errors in counterexample traces, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.97-105, January 15-17, 2003, New Orleans, Louisiana, USA
• 4: Pierre Bieber , Jacques Cazin , A. El Marouani , Pierre Girard , Jean Louis Lanet , Virginie Wiels , Guy Zanon, The PACAP Prototype: A Tool for Detecting Java Card Illegal Flow, Revised Papers from the First International Workshop on Java on Smart Cards: Programming and Security, p.25-37, September 14, 2000
• 5: Bruno Blanchet , Patrick Cousot , Radhia Cousot , Jérome Feret , Laurent Mauborgne , Antoine Miné , David Monniaux , Xavier Rival, A static analyzer for large safety-critical software, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 6: Stephen Chong , K. Vikram , Andrew C. Myers, SIF: enforcing confidentiality and integrity in web applications, Proceedings of 16th USENIX Security Symposium on USENIX Security Symposium, p.1-16, August 06-10, 2007, Boston, MA
• 7: Ron Cytron , Jeanne Ferrante , Barry K. Rosen , Mark N. Wegman , F. Kenneth Zadeck, Efficiently computing static single assignment form and the control dependence graph, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.4, p.451-490, Oct. 1991 [doi>10.1145/115372.115320]
• 8: Zhenyue Deng , Geoffrey Smith, Type inference and informative error reporting for secure information flow, Proceedings of the 44th annual Southeast regional conference, March 10-12, 2006, Melbourne, Florida [doi>10.1145/1185448.1185567]
• 9: Dorothy E. Denning, A lattice model of secure information flow, Communications of the ACM, v.19 n.5, p.236-243, May 1976 [doi>10.1145/360051.360056]
• 10: Dorothy E. Denning , Peter J. Denning, Certification of programs for secure information flow, Communications of the ACM, v.20 n.7, p.504-513, July 1977 [doi>10.1145/359636.359712]
• 11: E. M. Clarke , O. Grumberg , K. L. McMillan , X. Zhao, Efficient generation of counterexamples and witnesses in symbolic model checking, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.427-432, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217565]
• 12: Jeffrey S. Foster , Manuel Fähndrich , Alexander Aiken, A theory of type qualifiers, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.192-203, May 01-04, 1999, Atlanta, Georgia, United States
• 13: Christian Hammer , Martin Grimme , Jens Krinke, Dynamic path conditions in dependence graphs, Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 09-10, 2006, Charleston, South Carolina [doi>10.1145/1111542.1111552]
• 14: Sudheendra Hangal , Monica S. Lam, Tracking down software bugs using automatic anomaly detection, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581377]
• 15: Boniface Hicks , Kiyan Ahmadizadeh , Patrick McDaniel, From Languages to Systems: Understanding Practical Application Development in Security-typed Languages, Proceedings of the 22nd Annual Computer Security Applications Conference on Annual Computer Security Applications Conference, p.153-164, December 11-15, 2006 [doi>10.1109/ACSAC.2006.30]
• 16: Susan Horwitz , Thomas Reps , David Binkley, Interprocedural slicing using dependence graphs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.1, p.26-60, Jan. 1990 [doi>10.1145/77606.77608]
• 17: Rob Johnson , David Wagner, Finding user/kernel pointer bugs with type inference, Proceedings of the 13th conference on USENIX Security Symposium, p.9-9, August 09-13, 2004, San Diego, CA
• 18: King, D., Jaeger, T., Jha, S., and Seshia, S. A. Effective blame for information flow violations. Tech. Rep. NAS-TR-0069-2007 (Updated March 2008), The Pennsylvania State University, 2008.
• 19: 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]
• 20: Myers, A. C., Nystrom, N., Zheng, L., and Zdancewic, S. Jif: Java + Information Flow. http://www.cs.cornell.edu/jif.
• 21: 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
• 22: Jakob Rehof , Torben Ægidius Mogensen, Tractable constraints in finite semilattices, Science of Computer Programming, v.35 n.2-3, p.191-221, Nov.1.1999 [doi>10.1016/S0167-6423(99)00011-8]
• 23: Renieris, M., and Reiss, S. P. Fault localization with nearest neighbor queries. In ASE (2003).
• 24: Torsten Robschink , Gregor Snelting, Efficient path conditions in dependence graphs, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581398]
• 25: Sharir, M., and Pnueli, A. Two approaches to interprocedural dataflow analysis. In Program Flow Analysis: Theory and Applications (1981), Prentice Hall, pp. 189--234.
• 26: Scott F. Smith , Mark Thober, Refactoring programs to secure information flows, Proceedings of the 2006 workshop on Programming languages and analysis for security, June 10-10, 2006, Ottawa, Ontario, Canada [doi>10.1145/1134744.1134758]
• 27: Tip, F. A survey of program slicing techniques. Journal of programming languages 3 (1995), 121--189.
• 28: Mitchell Wand, Finding the source of type errors, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.38-43, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512648]
• 29: Mark Weiser, Program slicing, Proceedings of the 5th international conference on Software engineering, p.439-449, March 09-12, 1981, San Diego, California, United States
• 30: Xiaolan Zhang , Antony Edwards , Trent Jaeger, Using CQUAL for Static Analysis of Authorization Hook Placement, Proceedings of the 11th USENIX Security Symposium, p.33-48, August 05-09, 2002

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods