Transforming out timing leaks

ABSTRACT

One aspect of security in mobile code is privacy: private (or secret) data should not be leaked to unauthorised agents. Most of the work on secure information flow has until recently only been concerned with detecting direct and indirect flows. Secret information can however be leaked to the attacker also through covert channels. It is very reasonable to assume that the attacker, even as an external observer, can monitor the timing (including termination) behaviour of the program. Thus to claim a program secure, the security analysis must take also these into account. In this work we present a surprisingly simple solution to the problem of detecting timing leakages to external observers. Our system consists of a type system in which well-typed programs do not leak secret information directly, indirectly or through timing, and a transformation for removing timing leakages. For any program that is well typed according to Volpano and Smith [VS97a], our transformation generates a program that is also free of timing leaks.

REFERENCES

• BBL94: 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
• DD77: 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]
• Den76: 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]
• DFWB97: D. Dean, E. W. Felten, D.. Wallach, and D. Balfanz. Java security: Web browsers and beyond. Technical Report TR-566-97, Princeton University, Computer Science Department, February 1997.
• GM82: J. Goguen and J. Meseguer. Security policies and security models. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society Press, April 1982.
• Gor94: A. Gordon. A tutorial on co-induction and functional programming. In Glasgow functional programming workshop, pages 78-95. Springer Workshops in Computing, 1994.
• Heh84: Eric C. R. Hehner, Predicative programming Part I, Communications of the ACM, v.27 n.2, p.134-143, Feb. 1984 [doi>10.1145/69610.357988]
• HG92: Jingsha He , Virgil D. Gligor, Formal Methods and Automated Tool for Timing-Channel Identification in TCB Source Code, Proceedings of the Second European Symposium on Research in Computer Security, p.57-76, November 23-25, 1992
• HR98: 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]
• Koc96: Paul C. Kocher, Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems, Proceedings of the 16th Annual International Cryptology Conference on Advances in Cryptology, p.104-113, August 18-22, 1996
• McC87: D. McCullough. Specifications for multi-level security and hook-up property. In Proceedings of the IEEE Symposium on Security and Privacy, pages 161-166. IEEE Computer Society Press, 1987.
• Mog89: Torben Æ Mogensen, Separating binding times in language specifications, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.12-25, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99372]
• Mye99: 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]
• Nie84: H.R. Nielson. Hoare Logic's for Run-time Analysis of Programs. Ph.D. thesis, CST-30-84, Edinburgh University, 1984.
• RLJ98: K. Rustan M. Leino , Rajeev Joshi, A Semantic Approach to Secure Information Flow, Proceedings of the Mathematics of Program Construction, p.254-271, June 15-17, 1998
• RT96: Thomas W. Reps , Todd Turnidge, Program Specialization via Program Slicing, Selected Papers from the Internaltional Seminar on Partial Evaluation, p.409-429, February 12-16, 1996
• SS99: A. Sabelfeld and D. Sands. Probabilistic noninterference for multithreaded programs. Unpublished (ht t p://www, cs. chalmers.se/" dave/papers/probsabelfeld-sands.ps), June; Revised October 1999.
• SV98: 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]
• VS97a: Dennis Volpano , Geoffrey Smith, Eliminating Covert Flows with Minimum Typings, Proceedings of the 10th Computer Security Foundations Workshop (CSFW '97), p.156, June 10-12, 1997
• VS97b: 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
• VS98: D. Volpano , G. Smith, Probabilistic Noninterference in a Concurrent Language, Proceedings of the 11th IEEE Computer Security Foundations Workshop, p.34, June 09-11, 1998
• VSI96: 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

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.0 General
          Subjects: Security and protection (e.g., firewalls)

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES