A type system for data-flow integrity on Windows Vista

ABSTRACT

The Windows Vista operating system implements an interesting model of multi-level integrity. We observe that in this model, trusted code must participate in any information-flow attack. Thus, it is possible to eliminate such attacks by statically restricting trusted code. We formalize this model by designing a type system that can efficiently enforce data-flow integrity on Windows Vista. Typechecking guarantees that objects whose contents are statically trusted never contain untrusted values, regardless of what untrusted code runs in the environment. Some of Windows Vista's runtime access checks are necessary for soundness; others are redundant and can be optimized away.

REFERENCES

• 1: Martín Abadi, Secrecy by typing in security protocols, Journal of the ACM (JACM), v.46 n.5, p.749-786, Sept. 1999 [doi>10.1145/324133.324266]
• 2: Martín Abadi , Anindya Banerjee , Nevin Heintze , Jon G. Riecke, A core calculus of dependency, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.147-160, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292555]
• 3: Martín Abadi , Bruno Blanchet, Analyzing security protocols with secrecy types and logic programs, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.33-44, January 16-18, 2002, Portland, Oregon
• 4: M. Abadi , L. Cardelli , P.-L. Curien , J.-J. Levy, Explicit substitutions, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.31-46, December 1989, San Francisco, California, United States [doi>10.1145/96709.96712]
• 5: Martín Abadi , Cédric Fournet, Mobile values, new names, and secure communication, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.104-115, January 2001, London, United Kingdom
• 6: Martín Abadi , Butler Lampson , Jean-Jacques Lévy, Analysis and caching of dependencies, Proceedings of the first ACM SIGPLAN international conference on Functional programming, p.83-91, May 24-26, 1996, Philadelphia, Pennsylvania, United States
• 7: B. Alpern and F. B. Schneider. Defining liveness. Information Processing Letters, 21(5):181--185, 1985.
• 8: A. Banerjee and D. Naumann. Using access control for secure information flow in a Java-like language. In CSFW'03: Computer Security Foundations Workshop, pages 155--169. IEEE, 2003.
• 9: K. J. Biba. Integrity considerations for secure computer systems. Technical Report TR-3153, MITRE Corporation, 1977.
• 10: Gérard Boudol , Ilaria Castellani, Noninterference for concurrent programs and thread systems, Theoretical Computer Science, v.281 n.1-2, p.109-130, June 3 2002 [doi>10.1016/S0304-3975(02)00010-5]
• 11: Luca Cardelli , Giorgio Ghelli , Andrew D. Gordon, Secrecy and group creation, Information and Computation, v.196 n.2, p.127-155, January 29, 2005 [doi>10.1016/j.ic.2004.08.003]
• 12: Miguel Castro , Manuel Costa , Tim Harris, Securing software by enforcing data-flow integrity, Proceedings of the 7th symposium on Operating systems design and implementation, November 06-08, 2006, Seattle, Washington
• 13: A. Chaudhuri. Dynamic access control in a concurrent object calculus. In CONCUR'06: Concurrency Theory, pages 263--278. Springer, 2006.
• 14: Avik Chaudhuri , Martin Abadi, Secrecy by Typing and File-Access Control, Proceedings of the 19th IEEE workshop on Computer Security Foundations, p.112-123, July 05-07, 2006 [doi>10.1109/CSFW.2006.28]
• 15: A. Chaudhuri, P. Naldurg, and S. Rajamani. A type system for data-flow integrity on Windows Vista. Technical Report TR-2007-86, Microsoft Research, 2007. Also available as an arXiv e-print at http://arxiv.org/abs/0803.3230.
• 16: D. D. Clark and D. R. Wilson. A comparison of commercial and military computer security policies. In SP'87: Symposium on Security and Privacy, pages 184--194. IEEE, 1987.
• 17: James Clause , Wanchun Li , Alessandro Orso, Dytan: a generic dynamic taint analysis framework, Proceedings of the 2007 international symposium on Software testing and analysis, July 09-12, 2007, London, United Kingdom [doi>10.1145/1273463.1273490]
• 18: M. Conover. Analysis of the Windows Vista security model. Available at www.symantec.com/avcenter/reference/Windows_Vista_Security_Model_Analysis.pdf.
• 19: 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]
• 20: Petros Efstathopoulos , Maxwell Krohn , Steve VanDeBogart , Cliff Frey , David Ziegler , Eddie Kohler , David Mazières , Frans Kaashoek , Robert Morris, Labels and event processes in the asbestos operating system, Proceedings of the twentieth ACM symposium on Operating systems principles, October 23-26, 2005, Brighton, United Kingdom
• 21: Mattias Felleisen, The theory and practice of first-class prompts, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.180-190, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73576]
• 22: Cormac Flanagan, Hybrid type checking, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.245-256, January 11-13, 2006, Charleston, South Carolina, USA
• 23: C. Fournet, A. D. Gordon, and S. Maffeis. A type discipline for authorization policies. In ESOP'05: European Symposium on Programming, pages 141--156. Springer, 2005.
• 24: J. A. Goguen and J. Meseguer. Security policies and security models. In SP'82: Symposium on Security and Privacy, pages 11--20. IEEE, 1982.
• 25: A. D. Gordon and P. D. Hankin. A concurrent object calculus: Reduction and typing. In HLCL'98: High-Level Concurrent Languages, pages 248--264. Elsevier, 1998.
• 26: Andrew D. Gordon , Alan Jeffrey, Typing correspondence assertions for communication protocols, Theoretical Computer Science, v.300 n.1-3, p.379-409, 07 May 2003 [doi>10.1016/S0304-3975(02)00333-X]
• 27: Andrew D. Gordon , Alan Jeffrey, Secrecy despite compromise: types, cryptography, and the pi-calculus, CONCUR 2005 - Concurrency Theory, Springer-Verlag, London, 2005 [doi>10.1007/11539452_17]
• 28: Matthew Hennessy , Julian Rathke , Nobuko Yoshida, safeDpi: a language for controlling mobile code, Acta Informatica, v.42 n.4, p.227-290, December 2005 [doi>10.1007/s00236-005-0178-y]
• 29: Matthew Hennessy , James Riely, Information flow vs. resource access in the asynchronous pi-calculus, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.5, p.566-591, September 2002 [doi>10.1145/570886.570890]
• 30: Kohei Honda , Nobuko Yoshida, A uniform type structure for secure information flow, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.81-92, January 16-18, 2002, Portland, Oregon
• 31: Daisuke Hoshina , Eijiro Sumii , Akinori Yonezawa, A Typed Process Calculus for Fine-Grained Resource Access Control in Distributed Computation, Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software, p.64-81, October 29-31, 2001
• 32: Michael Howard , David LeBlanc, Writing secure code for windows vista™, Microsoft Press, Redmond, WA, 2007
• 33: Naoki Kobayashi, Type-based information flow analysis for the π-calculus, Acta Informatica, v.42 n.4, p.291-347, December 2005 [doi>10.1007/s00236-005-0179-x]
• 34: L. Lamport, Proving the Correctness of Multiprocess Programs, IEEE Transactions on Software Engineering, v.3 n.2, p.125-143, March 1977 [doi>10.1109/TSE.1977.229904]
• 35: Butler W. Lampson, Protection, ACM SIGOPS Operating Systems Review, v.8 n.1, p.18-24, January 1974 [doi>10.1145/775265.775268]
• 36: J.-J. Lévy. Réductions correctes et optimales dans le lambdacalcul. PhD thesis, Université Paris 7, 1978.
• 37: Peng Li , Steve Zdancewic, Downgrading policies and relaxed noninterference, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.158-170, January 12-14, 2005, Long Beach, California, USA
• 38: Larry Wall , Randal L. Schwartz, Programming perl, O'Reilly & Associates, Inc., Sebastopol, CA, 1991
• 39: Andrew C. Myers , Andrei Sabelfeld , Steve Zdancewic, Enforcing Robust Declassification, Proceedings of the 17th IEEE workshop on Computer Security Foundations, p.172, June 28-30, 2004 [doi>10.1109/CSFW.2004.9]
• 40: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 41: Marco Pistoia , Anindya Banerjee , David A. Naumann, Beyond Stack Inspection: A Unified Access-Control and Information-Flow Security Model, Proceedings of the 2007 IEEE Symposium on Security and Privacy, p.149-163, May 20-23, 2007 [doi>10.1109/SP.2007.10]
• 42: François Pottier , Sylvain Conchon, Information flow inference for free, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.46-57, September 2000
• 43: François Pottier , Christian Skalka , Scott Smith, A systematic approach to static access control, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.2, p.344-382, March 2005 [doi>10.1145/1057387.1057392]
• 44: M. Russinovich. Inside Windows Vista User Access Control. Microsoft Technet Magazine, June 2007. Available at http://www.microsoft.com/technet/technetmag/issues/2007/06/UAC/.
• 45: A. Sabelfeld and A. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1), 2003.
• 46: Davide Sangiorgi , Naoki Kobayashi , Eijiro Sumii, Environmental Bisimulations for Higher-Order Languages, Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, p.293-302, July 10-14, 2007 [doi>10.1109/LICS.2007.17]
• 47: U. Shankar, T. Jaeger, and R. Sailer. Toward automated information-flow integrity verification for security-critical applications. In NDSS'06: Network and Distributed System Security Symposium. ISOC, 2006.
• 48: G. Edward Suh , Jae W. Lee , David Zhang , Srinivas Devadas, Secure program execution via dynamic information flow tracking, Proceedings of the 11th international conference on Architectural support for programming languages and operating systems, October 07-13, 2004, Boston, MA, USA
• 49: S. Tse and S. Zdancewic. Run-time principals in information-flow type systems. In SP'04: Symposium on Security and Privacy, pages 179--193. IEEE, 2004.
• 50: P. Vogt, F. Nentwich, N. Jovanovic, C. Kruegel, E. Kirda, and G. Vigna. Cross site scripting prevention with dynamic data tainting and static analysis. In NDSS'07: Network and Distributed System Security Symposium. ISOC, 2007.
• 51: 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
• 52: P. Wadler and R. B. Findler. Well-typed programs can't be blamed. In Scheme'07: Workshop on Scheme and Functional Programming, 2007.
• 53: Windows Vista TechCenter. Understanding and configuring User Account Control in Windows Vista. Available at http://technet.microsoft.com/en-us/windowsvista/aa905117.aspx.
• 54: Heng Yin , Dawn Song , Manuel Egele , Christopher Kruegel , Engin Kirda, Panorama: capturing system-wide information flow for malware detection and analysis, Proceedings of the 14th ACM conference on Computer and communications security, October 28-31, 2007, Alexandria, Virginia, USA [doi>10.1145/1315245.1315261]
• 55: Nobuko Yoshida, Channel dependent types for higher-order mobile processes, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.147-160, January 14-16, 2004, Venice, Italy
• 56: Steve Zdancewic , Andrew C. Myers, Robust Declassification, Proceedings of the 14th IEEE workshop on Computer Security Foundations, p.5, June 11-13, 2001
• 57: Steve Zdancewic , Andrew C. Myers, Secure Information Flow via Linear Continuations, Higher-Order and Symbolic Computation, v.15 n.2-3, p.209-234, September 2002 [doi>10.1023/A:1020843229247]
• 58: S. Zdancewic and A. C. Myers. Observational determinism for concurrent program security. In CSFW'03: Computer Security Foundations Workshop, pages 29--43. IEEE, 2003.
• 59: Nickolai Zeldovich , Silas Boyd-Wickizer , Eddie Kohler , David Mazières, Making information flow explicit in HiStar, Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation, p.19-19, November 06-08, 2006, Seattle, WA
• 60: L. Zheng. Personal communication, July 2007.
• 61: L. Zheng and A. Myers. Dynamic security labels and noninterference. In FAST'04: Formal Aspects in Security and Trust, pages 27--40. Springer, 2004.

INDEX TERMS

Primary Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Access controls

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques; Mechanical verification; Invariants

General Terms:
Languages, Security, Theory, Verification

Keywords:
data-flow integrity, dynamic access control, explicit substitution, hybrid type system