A security domain model to assess software for exploitable covert channels

ABSTRACT

Covert channels can result in unauthorized information flows when exploited by malicious software. To address this problem, we present a precise, formal definition for covert channels, which relies on control flow dependency tracing through program execution, and extends Dennings' and subsequent classic work in secure information flow [9][40][30]. A formal security Domain Model (DM) for conducting static analysis of programs to identify covert channel vulnerabilities is described. The DM is comprised of an Invariant Model, which defines the generic concepts of program state, information flow, and covert channel rules; and an Implementation Model, which specifies the behavior of a target program. The DM is compiled from a representation of the program, written in a domain-specific Implementation Modeling Language (IML), and a specification of the security policy written in Alloy. The Alloy Analyzer tool is used to perform static analysis of the DM to automatically detect potential covert channel vulnerabilities and security policy violations in the target program.

REFERENCES

• 1: The Alloy Analyzer website. (2000). Retrieved January 11, 2008, from http://alloy.mit.edu/.
• 2: Bell, D., & LaPadula, L. (1973). Secure Computer Systems: Mathematical Foundations and Model, MITRE Report. The MITRE Corp.
• 3: Serdar Cabuk , Carla E. Brodley , Clay Shields, IP covert timing channels: design and detection, Proceedings of the 11th ACM conference on Computer and communications security, October 25-29, 2004, Washington DC, USA [doi>10.1145/1030083.1030108]
• 4: Chen, C., Grisham, P., Khurshid, S., & Perry, D. (2006). Design and validation of a general security model with the alloy analyzer. Proceedings of the ACM SIGSOFT First Alloy Workshop (pp. 38--47).
• 5: Common Criteria for Information Technology Security Evaluation, Part 1: Introduction and General Model, version 3.1. Document number CCMB-2006-09-001. September 2006.
• 6: Department of Defense Trusted Computer Security Evaluation Criteria, DOD 5200.28-STD, National Computer Security Center, December 1985.
• 7: 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]
• 8: 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]
• 9: 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]
• 10: Steven Gianvecchio , Haining Wang, Detecting covert timing channels: an entropy-based approach, Proceedings of the 14th ACM conference on Computer and communications security, October 28-31, 2007, Alexandria, Virginia, USA [doi>10.1145/1315245.1315284]
• 11: Gligor, V. (1993). A guide to understanding covert channel analysis of trusted systems. Technical Rep. NCSC-TG-030, National Computer Security Center, Ft. Meade, MD, USA.
• 12: Graham-Cumming, J., & Sanders, J.W. (1991). On the refinement of non-interference. Proceedings of the Computer Security Foundations Workshop IV (pp.35--42).
• 13: Goguen, J., & Meseguer, J. (1984). Unwinding and inference control. Proceedings of the IEEE Symposium on Security and Privacy (pp. 75--86). IEEE Computer Society Press.
• 14: Goguen, J., & Meseguer, J. (1982). Security policies and security models. Proceedings of the IEEE Symposium on Security and Privacy (pp. 11--20). IEEE Computer Society Press.
• 15: J. Thomas Haigh , William D. Young, Extending the Noninterference Version of MLS for SAT, IEEE Transactions on Software Engineering, v.13 n.2, p.141-150, February 1987 [doi>10.1109/TSE.1987.226478]
• 16: Daniel Jackson, Software Abstractions: Logic, Language, and Analysis, The MIT Press, 2006
• 17: Richard A. Kemmerer, Shared resource matrix methodology: an approach to identifying storage and timing channels, ACM Transactions on Computer Systems (TOCS), v.1 n.3, p.256-277, August 1983 [doi>10.1145/357369.357374]
• 18: Bogdan Korel , Jurgen Rilling, Dynamic Program Slicing in Understanding of Program Execution, Proceedings of the 5th International Workshop on Program Comprehension (WPC '97), p.80, May 28-30, 1997
• 19: Kruger, L., Wang, H., & Jha, S. (2004). Towards discovering and containing privacy violations in software (Technical Report No. 1515). Madison, WI, USA: University of Wisconsin-Madison.
• 20: Butler W. Lampson, A note on the confinement problem, Communications of the ACM, v.16 n.10, p.613-615, Oct. 1973 [doi>10.1145/362375.362389]
• 21: Laud, P. (2003). Handling encryption in analyses for secure information flow. Proceedings 12 th European Symposium on Programming, ESOP (pp. 159--173).
• 22: Levin, T., & Clark, P. (2004). A note regarding covert channels. Proceedings of the 6th Workshop on Education in Computer Security (pp. 11--15). Monterey, CA, USA.
• 23: Levin, T., Irvine, C., & Spyropoulou, E. (2006). Quality of security service: Adaptive security. Handbook of Information Security (H. Bidgoli, ed.), vol. 3, pp. 1016--1025, Hoboken, NJ: John Wiley and Sons.
• 24: McLean, J. (1990). Security models and information flow. Proceedings of the IEEE Symposium on Security and Privacy (pp. 180--189). IEEE Computer Society Press.
• 25: John McLean, A General Theory of Composition for a Class of "Possibilistic" Properties, IEEE Transactions on Software Engineering, v.22 n.1, p.53-67, January 1996 [doi>10.1109/32.481534]
• 26: National Security Agency IA Directorate. (2004). Global Information Grid Information Assurance Reference Capability/Technology Roadmap, Version 1.0.
• 27: National Security Agency. (2007). U.S. Government Protection Profile for Separation Kernels in Environments Requiring High Robustness, Version 1.03.
• 28: Padlipsky, M., Snow, D., & Karger, P. (1978). Limitations of end-to-end encryption in secure computer networks. MITRE Technical Report, MTR-3592, Vol. I, May 1978 (ESD TR 78-158, DTIC AD A059221).
• 29: A. W. Roscoe, CSP and determinism in security modelling, Proceedings of the 1995 IEEE Symposium on Security and Privacy, p.114, May 08-10, 1995
• 30: Sabelfeld, A., & Myers. A. (2003). Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1), 5--19. IEEE Press.
• 31: Andrei Sabelfeld , David Sands, Probabilistic Noninterference for Multi-Threaded Programs, Proceedings of the 13th IEEE workshop on Computer Security Foundations, p.200, July 03-05, 2000
• 32: Marvin Schaefer , Barry Gold , Richard Linde , John Scheid, Program confinement in KVM/370, Proceedings of the 1977 annual conference, p.404-410, January 1977 [doi>10.1145/800179.1124633]
• 33: Shaffer, A., Auguston, M., Irvine, C. and Levin, T. (2007). Toward a security domain model for static analysis and verification of information systems. Proceedings of the 7th OOPSLA Workshop on Domain-Specific Modeling (pp. 160--171). Montreal, Canada.
• 34: Simonet, V. (2003). Type inference with structural subtyping: A faithful formalization of an efficient constraint solver. Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS'03), vol 2895 (pp. 283--302). Beijing, China: Springer-Verlag.
• 35: Geoffrey Smith, Secure information flow with random assignment and encryption, Proceedings of the fourth ACM workshop on Formal methods in security, p.33-44, November 03-03, 2006, Alexandria, Virginia, USA [doi>10.1145/1180337.1180341]
• 36: Geoffrey Smith, Improved typings for probabilistic noninterference in a multi-threaded language, Journal of Computer Security, v.14 n.6, p.591-623, November 2006
• 37: Scott F. Smith , Mark Thober, Improving usability of information flow security in java, Proceedings of the 2007 workshop on Programming languages and analysis for security, June 14-14, 2007, San Diego, California, USA [doi>10.1145/1255329.1255332]
• 38: Chii-Ren Tsai , Virgil D. Gligor , C. S. Shandersekaran, On the Identification of Covert Storage Channels in Secure Systems, IEEE Transactions on Software Engineering, v.16 n.6, p.569-580, June 1990 [doi>10.1109/32.55086]
• 39: Dennis Volpano , Geoffrey Smith, Probabilistic noninterference in a concurrent language, Journal of Computer Security, v.7 n.2-3, p.231-253, Jan. 1999
• 40: 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
• 41: von Oheimb, D. (2004). Information flow control revisited: Noninfluence = noninterference + nonleakage. Proceedings of the 9th European Symposium on Research Computer Security (pp. 225--243). Sophia Antipolis, France.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Assertion checkers

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Syntax; Semantics
      D.3.4 Processors
          Subjects: Compilers
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Access controls; Information flow controls

General Terms:
Design, Languages, Security, Verification

Keywords:
automated program verification, covert channel, dynamic slicing, security domain model, specification language, static analysis