Efficient type inference for secure information flow

ABSTRACT

This paper describes the design, analysis, and implementation of an efficient algorithm for information flow analysis expressed using a type system. Given a program and an environment of security classes for information accessed by the program, the algorithm checks whether the program is well typed, i.e., there is no information of higher security classes flowing into places of lower security classes according to a lattice of security classes, by inferring the highest or lowest security class as appropriate for each program node. We express the analysis as a set of Datalog-like rules based on the typing and subtyping rules, and we use a systematic method to generate specialized algorithms and data structures directly from the Datalog-like rules. The generated implementation traverses the program multiple times and uses a combination of linked and indexed data structures to represent program nodes, environments, and types. The time complexity of the algorithm is linear in the size of the input program, times the height of the lattice of security classes, plus a small overhead for preprocessing the security classes. This complexity is confirmed through our prototype implementation and experimental evaluation on code generated from high-level specifications for real systems.

REFERENCES

• 1: Martín Abadi, Secrecy by Typing inSecurity Protocols, Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software, p.611-638, September 23-26, 1997
• 2: Serge Abiteboul , Richard Hull , Victor Vianu, Foundations of Databases: The Logical Level, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1995
• 3: Hassan Aït-Kaci , Robert Boyer , Patrick Lincoln , Roger Nasr, Efficient implementation of lattice operations, ACM Transactions on Programming Languages and Systems (TOPLAS), v.11 n.1, p.115-146, Jan. 1989 [doi>10.1145/59287.59293]
• 4: Marco Avvenuti , Cinzia Bernardeschi , Nicoletta De Francesco, Java bytecode verification for secure information flow, ACM SIGPLAN Notices, v.38 n.12, December 2003 [doi>10.1145/966051.966055]
• 5: Jean-Pierre Banâtre , Ciarán Bryce , Daniel Le Métayer, Compile-Time Detection of Information Flow in Sequential Programs, Proceedings of the Third European Symposium on Research in Computer Security, p.55-73, November 07-09, 1994
• 6: Roberto Barbuti , Cinzia Bernardeschi , Nicoletta De Francesco, Checking security of Java bytecode by abstract interpretation, Proceedings of the 2002 ACM symposium on Applied computing, March 11-14, 2002, Madrid, Spain [doi>10.1145/508791.508839]
• 7: J. Cai , R. Paige, Program derivation by fixed point computation, Science of Computer Programming, v.11 n.3, p.197-261, April 1989 [doi>10.1016/0167-6423(88)90033-0 ]
• 8: Stefano Ceri , Georg Gottlob , Letizia Tanca, Logic programming and databases, Springer-Verlag New York, Inc., New York, NY, 1990
• 9: Z. Deng and G. Smith. Type inference and informative error reporting for secure information flow. In Proceedings of ACMSE 2006: 44th ACM Southeast Conference, Melbourne, Florida, 2006.
• 10: 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]
• 11: 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]
• 12: Nicoletta De Francesco , Antonella Santone , Luca Tesei, Abstract interpretation and model checking for checking secure information flow in concurrent systems, Fundamenta Informaticae, v.54 n.2-3, p.195-211, February 2003
• 13: Roberto Giacobazzi , Isabella Mastroeni, Abstract non-interference: parameterizing non-interference by abstract interpretation, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.186-197, January 14-16, 2004, Venice, Italy
• 14: Constance Heitmeyer, Using the SCR* Toolset to Specify Software Requirements, Proceedings of the Second IEEE Workshop on Industrial Strength Formal Specification Techniques, p.12, October 20-23, 1998
• 15: Yanhong A. Liu , Scott D. Stoller, From datalog rules to efficient programs with time and space guarantees, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.172-183, August 27-29, 2003, Uppsala, Sweden [doi>10.1145/888251.888268]
• 16: 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]
• 17: R. Paige. Real-time simulation of a set machine on a RAM. In Proceedings of the International Conference on Computing and Information, volume 2, pages 68--73, 1989.
• 18: Robert Paige , Shaye Koenig, Finite Differencing of Computable Expressions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.402-454, July 1982 [doi>10.1145/357172.357177]
• 19: Jens Palsberg , Peter Ørbæk, Trust in the lambda-Calculus, Proceedings of the Second International Symposium on Static Analysis, p.314-329, September 25-27, 1995
• 20: 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
• 21: Tom Rothamel , Yanhong A. Liu , Constance L. Heitmeyer , Elizabeth I. Leonard, Generating optimized code from SCR specifications, Proceedings of the 2006 ACM SIGPLAN/SIGBED conference on Language, compilers and tool support for embedded systems, June 14-16, 2006, Ottawa, Ontario, Canada
• 22: A.Sabelfeld and A. C. Myers. Language-based information-flow security. IEEE Journal On Selected Areas in Communications, 21(1):5--19, January 2003.
• 23: V. Simonet. Flow CAML in a nutshell. In G. Hutton, editor, Proceedings of the first APPSEM-II workshop, pages 152--165, 2003.
• 24: 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]
• 25: Martin Sulzmann, A General Type Inference Framework for Hindley/Milner Style Systems, Proceedings of the 5th International Symposium on Functional and Logic Programming, p.248-263, March 07-09, 2001
• 26: Q. Sun, A. Banerjee, and D. A. Naumann. Modular and constraint-based information flow inference for an object-oriented language. In Proceedings of the 11th International Static Analysis Symposium, volume 3148 of Lecture Notes in Computer Science, pages 84--99, Aug. 2004.
• 27: 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
• 28: 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.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Code generation

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Constraint and logic languages
      D.3.4 Processors
          Subjects: Optimization
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Access controls; Information flow controls

  E. Data
  E.1 DATA STRUCTURES
      Subjects: Records; Arrays; Lists, stacks, and queues

  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Computations on discrete structures

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
          Subjects: Program transformation

General Terms:
Algorithms, Languages, Performance, Security

Keywords:
algorithm, information flow, security, time complexity, type inference