Applying flow-sensitive CQUAL to verify MINIX authorization check placement

ABSTRACT

We present the first use of flow-sensitive CQUAL to verify the placement of operating system authorization checks. Our analysis of MINIX 3 system servers and discovery of a non-exploitable Time-Of-Check/Time-Of-Use bug demonstrate the effectiveness of flow sensitive CQUAL and its advantage over earlier flow-insensitive versions. We also identify and suggest alternatives to current CQUAL usability features that encourage analysts to make omissions that cause the otherwise sound tool to produce false-negative results.

REFERENCES

• 1: Ken Ashcraft , Dawson Engler, Using Programmer-Written Compiler Extensions to Catch Security Holes, Proceedings of the 2002 IEEE Symposium on Security and Privacy, p.143, May 12-15, 2002
• 2: Matt Bishop and Michael Dilger. Checking for Race Conditions in File Accesses. In USENIX Computing Systems, vol. 2, no. 2, 1996.
• 3: Common Criteria for Information Technology Security Evaluation v2.3 ISO/IEC 15408: 2005, August, 2005.
• 4: Maureen Harris Cheheyl , Morrie Gasser , George A. Huff , Jonathan K. Millen, Verifying Security, ACM Computing Surveys (CSUR), v.13 n.3, p.279-339, Sept. 1981 [doi>10.1145/356850.356853]
• 5: Jeffrey S. Foster , Manuel Fähndrich , Alexander Aiken, A theory of type qualifiers, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.192-203, May 01-04, 1999, Atlanta, Georgia, United States
• 6: Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 7: Ben Gras. In personal E-mail communication, 23 February 2006.
• 8: T. Jensen and D. Le Metayer and T. Thorn. Verification of control flow based security properties. In Proceedings of the 1999 IEEE Symposium on Security and Privacy, pages 89--103, 1999.
• 9: Rob Johnson and David Wagner. Finding User/Kernel Bugs With Type Inference. In Proceedings of the 13th Usenix Security Symposium, 2004.
• 10: National Computer Security Center. Department of Defense Trusted Computer System Evaluation Criteria. Dod 5200.28-STD, 1985.
• 11: Peter G. Neumann , Richard J. Feiertag , Karl N. Levitt , Lawrence Robinson, Software development and proofs of multi-level security, Proceedings of the 2nd international conference on Software engineering, p.421-428, October 13-15, 1976, San Francisco, California, United States
• 12: J. H. Saltzer and M. D. Schroder. The Protection of Information in Computer Systems. In Proceedings of the IEEE Vol. 63(9), 1975.
• 13: Benjamin Schwarz , Hao Chen , David Wagner , Jeremy Lin , Wei Tu , Geoff Morrison , Jacob West, Model Checking An Entire Linux Distribution for Security Violations, Proceedings of the 21st Annual Computer Security Applications Conference, p.13-22, December 05-09, 2005 [doi>10.1109/CSAC.2005.39]
• 14: Umesh Shankar and Kunal Talwar and Jeffrey S. Foster and David Wagner. Detecting Format String Vulnerabilities with Type Qualifiers. In Proceedings of the 10th USENIX Security Symposium, 2001.
• 15: The Open Group. Single UNIX Standard: System Interfaces Volume. The Open Group Base Specifications Issue 6, IEEE Std 1003.1, 2004.
• 16: Chris Wright , Crispin Cowan , Stephen Smalley , James Morris , Greg Kroah-Hartman, Linux Security Modules: General Security Support for the Linux Kernel, Proceedings of the 11th USENIX Security Symposium, p.17-31, August 05-09, 2002
• 17: Junfeng Yang , Ted Kremenek , Yichen Xie , Dawson Engler, MECA: an extensible, expressive system and language for statically checking security properties, Proceedings of the 10th ACM conference on Computer and communications security, October 27-30, 2003, Washington D.C., USA [doi>10.1145/948109.948153]
• 18: Xiaolan Zhang , Antony Edwards , Trent Jaeger, Using CQUAL for Static Analysis of Authorization Hook Placement, Proceedings of the 11th USENIX Security Symposium, p.33-48, August 05-09, 2002

INDEX TERMS

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

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

General Terms:
Security

Keywords:
CQUAL, MINIX, static analysis, type qualifiers