Quantitative information flow as network flow capacity

ABSTRACT

We present a new technique for determining how much information about a program's secret inputs is revealed by its public outputs. In contrast to previous techniques based on reachability from secret inputs (tainting), it achieves a more precise quantitative result by computing a maximum flow of information between the inputs and outputs. The technique uses static control-flow regions to soundly account for implicit flows via branches and pointer operations, but operates dynamically by observing one or more program executions and giving numeric flow bounds specific to them (e.g., "17 bits"). The maximum flow in a network also gives a minimum cut (a set of edges that separate the secret input from the output), which can be used to efficiently check that the same policy is satisfied on future executions. We performed case studies on 5 real C, C++, and Objective C programs, 3 of which had more than 250K lines of code. The tool checked multiple security policies, including one that was violated by a previously unknown bug.

References

1. R. Ahlswede, N. Cai, S.-Y. R. Li, and R. W. Yeung. Network information flow. IEEE Transactions on Information Theory, 46(4):1204--1216, 2000.]]
2. A. Askarov and A. Sabelfeld. Security-typed languages for implementation of cryptographic protocols: A case study. In Proceedings of the 10th European Symposium On Research In Computer Security (LNCS 3679), pages 197--221, Milan, Italy, September 12-14, 2005.]]
3. G. D. Battista and R. Tamassia. Incremental planarity testing. In 30th Annual Symposium on Foundations of Computer Science, pages 436--441, Research Triangle Park, NC, USA, October 30-November 1, 1989.]]
4. M. D. Bond and K. S. McKinley. Probabilistic calling context. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2007), pages 97--112, Montreal, Canada, October 23--25, 2007.]]
5. M. Budiu, M. Sakr, K. Walker, and S. C. Goldstein. BitValue inference: Detecting and exploiting narrow bitwidth computations. In European Conference on Parallel Processing, pages 969--979, Munich, Germany, August 29-September 1, 2000.]]
6. D. Chandra and M. Franz. Fine-grained information flow analysis and enforcement in a Java virtual machine. In 23rd Annual Computer Security Applications Conference, pages 463--475, Miami Beach, FL, USA, December 10-14, 2007.]]
7. J.-D. Choi, M. Burke, and P. Carini. Efficient flow-sensitive interprocedural computation of pointer-induced aliases and side effects. In Proceedings of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 232--245, Charleston, SC, January 1993.]]
8. J. Chow, B. Pfaff, T. Garfinkel, K. Christopher, and M. Rosenblum. Understanding data lifetime via whole system simulation. In 13th USENIX Security Symposium, pages 321--336, San Diego, CA, USA, August 11-13, 2004.]]
9. D. Clark, S. Hunt, and P. Malacaria. Quantified interference for a while language. In Proceedings of the 2nd Workshop on Quantitative Aspects of Programming Languages (ENTCS 112), pages 149--159, Barcelona, Spain, March 27-28, 2004.]]
10. J. Clause, W. Li, and A. Orso. Dytan: A generic dynamic taint analysis framework. In ISSTA 2007, Proceedings of the 2007 International Symposium on Software Testing and Analysis, pages 196--206, London, UK, July 10-12, 2007.]]
11. T. H. Cormen, C. E. Leiserson, and R. L. Rivest. Introduction to Algorithms. MIT Electrical Engineering and Computer Science Series. MIT Press and McGraw-Hill, Cambridge, Massachusetts and New York, New York, 1990.]]
12. T.M. Cover and J. A. Thomas. Elements of Information Theory. John Wiley, 1991.]]
13. D. E. Denning. A lattice model of secure information flow. Communications of the ACM, 19(5):236--243, May 1976.]]
14. D. E. R. Denning. Secure Information Flow in Computer Systems. PhD thesis, Purdue University, May 1975.]]
15. Department of Defense Computer Security Center. Trusted Computer System Evaluation Criteria, August 1983. CSC-STD-001-83.]]
16. A. Di Pierro, C. Hankin, and H. Wiklicky. Approximate noninterference. In 15th IEEE Computer Security Foundations Workshop, pages 3--17, Cape Breton, Nova Scotia, Canada, June 24-26, 2002.]]
17. W. Drewry and T. Ormandy. Flayer: Exposing application internals. In First USENIX Workshop on Offensive Technologies, Boston, MA, USA, August 6, 2007.]]
18. P. Efstathopoulos, M. Krohn, S. VanDeBogart, C. Frey, D. Ziegler, E. Kohler, D. Mazieres, F. Kaashoek, and R. Morris. Labels and event processes in the Asbestos operating system. In Proceedings of the 20th ACM Symposium on Operating Systems Principles, pages 17--30, Brighton, UK, October 32-26, 2005.]]
19. J. S. Fenton. Memoryless subsytems. The Computer Journal, 17(2):143--147, May 1974.]]
20. E. Ferrari, P. Samarati, E. Bertino, and S. Jajodia. Providing flexibility in information flow control for object-oriented systems. In 1997 IEEE Symposium on Security and Privacy, pages 130--140, Oakland, CA, USA, May 4-7, 1997.]]
21. I. Gat and H. J. Saal. Memoryless execution: A programmer's viewpoint. Software: Practice and Experience, 6(4):463--471, 1976.]]
22. J. A. Goguen and J. Meseguer. Security policies and security models. In 1982 IEEE Symposium on Security and Privacy, pages 11--20, Oakland, CA, USA, April 26-28, 1982.]]
23. J. W. Gray III. Toward a mathematical foundation for information flow security. In 1991 IEEE Symposium on Research in Security and Privacy, pages 21--34, Oakland, CA, USA, May 20-22, 1991.]]
24. M. Herrb. X.org security advisory: multiple integer overflows in DBE and Render extensions, January 2007. http://lists.freedesktop.org/archives/xorg-announce/2007-January/000235.html.]]
25. B. Hicks, K. Ahmadizadeh, and P. McDaniel. From languages to systems: Understanding practical application development in security-typed languages. In Proceedings of the 2006 Annual Computer Security Applications Conference, pages 153--164, Miami Beach, FL, USA, December 11-15, 2006.]]
26. V. Kiriansky, D. Bruening, and S. Amarasinghe. Secure execution via program shepherding. In 11th USENIX Security Symposium, pages 191--206, San Francisco, CA, USA, August 7-9, 2002.]]
27. P. Li and S. Zdancewic. Encoding information flow in Haskell. In 19th IEEE Computer Security Foundations Workshop, pages 16--27, Venice, Italy, July 5-6, 2006.]]
28. G. Lowe. Quantifiying information flow. In 15th IEEE Computer Security Foundations Workshop, pages 18--31, Cape Breton, Nova Scotia, Canada, June 24-26, 2002.]]
29. P. Malacaria. Assessing security threats of looping constructs. In Proceedings of the 34rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 225--235, Nice, France, January 17-19, 2007.]]
30. W. Masri, A. Podgurski, and D. Leon. Detecting and debugging insecure information flows. In Fifteenth International Symposium on Software Reliability Engineering, pages 198--209, Saint-Malo, France, November 3-5, 2004.]]
31. S. McCamant. Quantitative Information-Flow Tracking for Real Systems. PhD thesis, MIT Department of Electrical Engineering and Computer Science, Cambridge, MA, June 2008.]]
32. S. McCamant and M. D. Ernst. Quantitative information-flow tracking for C and related languages. Technical Report MIT-CSAILTR- 2006-076, MIT Computer Science and Artificial Intelligence Laboratory, Cambridge, MA, November 17, 2006.]]
33. S. McCamant and M. D. Ernst. Quantitative information flow as network flow capacity. Technical Report MIT-CSAIL-TR-2007-057, MIT Computer Science and Artificial Intelligence Laboratory, Cambridge, MA, December 10, 2007.]]
34. S. McCamant and M. D. Ernst. A simulation-based proof technique for dynamic information flow. In PLAS 2007: ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, pages 41--46, San Diego, California, USA, June 14, 2007.]]
35. A. C. Myers. JFlow: Practical mostly-static information flow control. In Proceedings of the 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 228--241, San Antonio, TX, January 20-22, 1999.]]
36. A. C. Myers and B. Liskov. A decentralized model for information flow control. In Proceedings of the 16th ACM Symposium on Operating Systems Principles, pages 129--142, St. Malo, France, October 5-8, 1997.]]
37. S. K. Nair, P. N. Simpson, B. Crispo, and A. S. Tannenbaum. A virtual machine based information flow control system for policy enforcement. In The First International Workshop on Run Time Enforcement for Mobile and Distributed Systems, pages 3--16, Dresden, Germany, September 27, 2007.]]
38. G. C. Necula, S. McPeak, S. Rahul, and W. Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs. In Compiler Construction: 11th International Conference, CC 2002, pages 213--228, Grenoble, France, April 8-12, 2002.]]
39. N. Nethercote and A. Mycroft. Redux: A dynamic dataflow tracer. In Proceedings of the Third Workshop on Runtime Verification, Boulder, CO, USA, July 13, 2003.]]
40. N. Nethercote and J. Seward. Valgrind: A framework for heavyweight dynamic binary insrumentation. In Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, pages 89--100, San Diego, CA, USA, June 11-13, 2007.]]
41. J. Newsome and D. Song. Dynamic taint analysis: Automatic detection, analysis, and signature generation of exploit attacks on commodity software. In Annual Symposium on Network and Distributed System Security, San Diego, CA, USA, February 3-4, 2005.]]
42. J. Newsome and D. Song. Influence: A quantitative approach for data integrity. Technical Report CMU-CyLab-08-005, Carnegie Mellon University CyLab, February 2008.]]
43. A. Nguyen-Tuong, S. Guarnieri, D. Greene, J. Shirley, and D. Evans. Automatically hardening web applications using precise tainting. In 20th IFIP International Information Security Conference, pages 295--307, Chiba, Japan, May 30-June 1, 2005.]]
44. J. Qian, B. Xu, and H. Min. Interstatement must aliases for data dependence analysis of heap locations. In ACM SIGPLAN/SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 2007), pages 17--23, San Diego, CA, USA, June 13-14, 2007.]]
45. F. Qin, C. Wang, Z. Li, H.-S. Kim, Y. Zhou, and Y. Wu. LIFT: A low-overhead practical information flow tracking system for detecting general security attacks. In Proceedings of the 39th Annual IEEE/ACM International Symposium on Microarchitecture, pages 135--148, Orlando, FL, USA, December 9-13, 2006.]]
46. A. Salcianu and M. C. Rinard. Purity and side-effect analysis for Java programs. In VMCAI'05, Sixth International Conference on Verification, Model Checking and Abstract Interpretation, pages 199--215, Paris, France, January 17-19, 2005.]]
47. J. Seward and N. Nethercote. Using Valgrind to detect undefined value errors with bit-precision. In Proceedings of the 2005 USENIX Annual Technical Conference, pages 17--30, Anaheim, CA, USA, April 10-15, 2005.]]
48. V. Simonet. Flow Caml in a nutshell. In First Applied Semantics II (APPSEM-II) Workshop, pages 152--165, Nottingham, UK, May 26-28, 2003.]]
49. S. Smith and M. Thober. Refactoring programs to secure information flows. In PLAS 2006: ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, pages 75--84, Ottawa, Canada, June 10, 2006.]]
50. G. E. Suh, J. W. Lee, D. Zhang, and S. Devadas. Secure program execution via dynamic information flow tracking. In Proceedings of the 11th International Conference on Architectural Support for Programming Languages and Operating Systems, pages 85--96, Boston, Massachusetts, USA, October 7-13, 2004.]]
51. G. T. Sullivan, D. L. Bruening, I. Baron, T. Garnett, and S. Amarasinghe. Dynamic native optimization of interpreters. In ACM SIGPLAN 2003 Workshop on Interpreters, Virtual Machines and Emulators, pages 50--57, San Diego, California, USA, June 12, 2003.]]
52. N. Vachharajani, M. J. Bridges, J. Chang, R. Rangan, G. Ottoni, J. A. Blome, G. A. Reis, M. Vachharajani, and D. I. August. RIFLE: An architectural framework for user-centric information-flow security. In Proceedings of the 37th Annual IEEE/ACM International Symposium on Microarchitecture, pages 243--254, Portland, OR, USA, December 4-8, 2004.]]
53. D. Volpano, G. Smith, and C. Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(3):167--187, December 1996.]]
54. L. Wall and R. L. Schwartz. Programming Perl. O'Reilly & Associates, 1991.]]
55. D. P. Wiggins. Security Extension Specification. X Consortium, Inc., November 1996.]]
56. W. Xu, S. Bhatkar, and R. Sekar. Taint-enhanced policy enforcement: A practical approach to defeat a wide range of attacks. In 15th USENIX Security Symposium, pages 121--136, Vancouver, BC, Canada, August 2-4, 2006.]]
57. A. R. Yumerfendi, B. Mickle, and L. P. Cox. TightLip: Keeping applications from spilling the beans. In 4th USENIX Symposium on Networked Systems Design and Implementation, pages 159--172, Cambridge, MA, USA, April 11-13, 2007.]]
58. N. Zeldovich, S. Boyd-Wickizer, E. Kohler, and D. Mazieres. Making information flow explicit in HiStar. In USENIX 7th Symposium on OS Design and Implementation, pages 263--278, Seattle, WA, USA, November 6-8, 2006.]]

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Mathematics of computing

  • Discrete mathematics

    • Graph theory

  • Information theory

    • Coding theory

• Security and privacy

  • Cryptography

    • Mathematical foundations of cryptography

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

      • Software defect analysis

        • Software testing and debugging

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification