MECA: an extensible, expressive system and language for statically checking security properties

ABSTRACT

This paper describes a system and annotation language, MECA, for checking security rules. MECA is expressive and designed for checking real systems. It provides a variety of practical constructs to effectively annotate large bodies of code. For example, it allows programmers to write programmatic annotators that automatically annotate large bodies of source code. As another example, it lets programmers use general predicates to determine if an annotation is applied; we have used this ability to easily handle kernel backdoors and other false-positive inducing constructs. Once code is annotated, MECA propagates annotations aggressively, allowing a single manual annotation to derive many additional annotations (e.g., over one hundred in our experiments) freeing programmers from the heavy manual effort required by most past systems.MECA is effective. Our most thorough case study was a user-pointer checker that used 75 annotations to check thousands of declarations in millions of lines of code in the Linux system. It found over forty errors, many of which were serious, while only having eight false positives.

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: M. Bishop and M. Dilger. Checking for race conditions in file accesses. Computing systems, pages 131--152, Spring 1996.
• 3: Hao Chen , David Wagner, MOPS: an infrastructure for examining security properties of software, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA [doi>10.1145/586110.586142]
• 4: Andy Chow Chou , Dawson Engler, Static analysis for bug finding in systems software, 2003
• 5: Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
• 6: Nurit Dor , Michael Rodeh , Shmuel Sagiv, Cleanness Checking of String Manipulations in C Programs via Integer Analysis, Proceedings of the 8th International Symposium on Static Analysis, p.194-212, July 16-18, 2001
• 7: Antony Edwards , Trent Jaeger , Xiaolan Zhang, Runtime verification of authorization hook placement for the linux security modules framework, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA [doi>10.1145/586110.586141]
• 8: Dawson Engler , David Yu Chen , Seth Hallem , Andy Chou , Benjamin Chelf, Bugs as deviant behavior: a general approach to inferring errors in systems code, Proceedings of the eighteenth ACM symposium on Operating systems principles, October 21-24, 2001, Banff, Alberta, Canada
• 9: David Evans , David Larochelle, Improving Security Using Extensible Lightweight Static Analysis, IEEE Software, v.19 n.1, p.42-51, January 2002 [doi>10.1109/52.976940]
• 10: Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.219-232, June 18-21, 2000, Vancouver, British Columbia, Canada
• 11: Cormac Flanagan , K. Rustan M. Leino, Houdini, an Annotation Assistant for ESC/Java, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity, p.500-517, March 12-16, 2001
• 12: 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
• 13: D. Freedman, R. Pisani, and R. Purves. Statistics. W.W. Norton, third edition edition, 1998.
• 14: T. Kremenek and D. Engler. Z-ranking: Using statistical analysis to counter the impact of static analysis approximations. In 10th Annual International Static Analysis Symposium, 2003.
• 15: D. Larochelle and D. Evans. Statically detecting likely buffer overflow vulnerabilities. In USENIX Security Symposium, Washington, D. C., Aug. 2001.
• 16: K. R. M. Leino, G. Nelson, and J. Saxe. ESC/Java user's manual. Technical note 2000-002, Compaq Systems Research Center, Oct. 2001.
• 17: Andrew C. Myers , Barbara Liskov, A decentralized model for information flow control, Proceedings of the sixteenth ACM symposium on Operating systems principles, p.129-142, October 05-08, 1997, Saint Malo, France
• 18: J. Pincus. Personal communication. Developing a buffer overflow checker in PREfast (a version of of PREfix)., Oct. 2001.
• 19: S. M. Ross. Probability Models. Academic Press, London, UK, sixth edition, 1997.
• 20: J. Viega , J. T. Bloch , Y. Kohno , G. McGraw, ITS4: A static vulnerability scanner for C and C++ code, Proceedings of the 16th Annual Computer Security Applications Conference, p.257, December 11-15, 2000
• 21: David Wagner , Drew Dean, Intrusion Detection via Static Analysis, Proceedings of the 2001 IEEE Symposium on Security and Privacy, p.156, May 14-16, 2001
• 22: D. Wagner, J. Foster, E. Brewer, and A. Aiken. A first step towards automated detection of buffer overrun vulnerabilities. In The 2000 Network and Distributed Systems Security Conference. San Diego, CA, Feb. 2000.
• 23: 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.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection

General Terms:
Measurement, Reliability, Security

Keywords:
annotation language, static analysis