Hao Chen
ABSTRACT
We describe a formal approach for finding bugs in security-relevant software and verifying their absence. The idea is as follows: we identify rules of safe programming practice, encode them as safety properties, and verify whether these properties are obeyed. Because manual verification is too expensive, we have built a program analysis tool to automate this process. Our program analysis models the program to be verified as a pushdown automaton, represents the security property as a finite state automaton, and uses model checking techniques to identify whether any state violating the desired security goal is reachable in the program. The major advantages of this approach are that it is sound in verifying the absence of certain classes of vulnerabilities, that it is fully interprocedural, and that it is efficient and scalable. Experience suggests that this approach will be useful in finding a wide range of security vulnerabilities in large programs efficiently.
- K. Ashcraft and D. Engler. Using programmer-written compiler extensions to catch security holes. In Proceedings of IEEE Security and Privacy 2002, 2002. Google Scholar
Digital Library
- T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In SPIN 2001, Workshop on Model Checking of Software, 2001. Google ScholarDigital Library
- T. Ball and S. K. Rajamani. The SLAM project: Debugging system software via static analysis. In POPL 2002, 2002. Google ScholarDigital Library
- F. Besson, T. Jensen, D. L. Metayer, and T. Thorn. Model checking security properties of control flow graphs. Journal of Computer Security, 9:217--250, 2001. Google ScholarDigital Library
- M. Bishop and M. Dilger. Checking for race conditions in file access. Computing Systems, 9(2):131--152, 1996.Google Scholar
- CERT. CERT Advisory CA-1997-16: ftpd signal handling vulnerability. http://www.cert.org/advisories/CA-1997-16.html.Google Scholar
- H. Chen and D. Wagner. MOPS: an infrastructure for examining security properties of software. Technical Report UCB//CSD-02-1197, UC Berkeley, 2002. Google ScholarDigital Library
- H. Chen, D. Wagner, and D. Dean. Setuid demystified. In Proceedings of the Eleventh Usenix Security Symposium, San Francisco, CA, 2002. Google ScholarDigital Library
- D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In OSDI, 2000. Google ScholarDigital Library
- J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms for model checking pushdown systems. Technical report, Technische Universität München, 2000. Google ScholarDigital Library
- J. Foster, M. Fähndrich, and A. Aiken. A theory of type qualifiers. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'99), May 1999. Google ScholarDigital Library
- D. Greenman. Serious security bug in wu-ftpd v2.4. http://online.securityfocus.com/archive/1/6056/1997-01-04/1997-01-10/2.Google Scholar
- J. Hopcroft and J. Ullman. Introduction to automata theory, languages, and computation. Addison-Wesley, 1979. Google ScholarDigital Library
- T. Jensen, D. L. Metayer, and T. Thorn. Verification of control flow based security properties. In Proceedings of the 1999 IEEE Symposium on Security and Privacy, 1999.Google ScholarCross Ref
- L. Koved, M. Pistoia, and A. Kershenbaum. Access rights analysis for java. In Proceedings of the 17th Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2002. Google ScholarDigital Library
- Sendmail Inc. Sendmail workaround for linux capabilities bug. http://www.sendmail.org/sendmail.8.10.1.LINUX-SECURITY.txt.Google Scholar
- U. Shankar, K. Talwar, J. S. Foster, and D. Wagner. Detecting format string vulnerabilities with type qualifiers. In Proceedings of the 10th USENIX Security Symposium, 2001. Google ScholarDigital Library
- D. Wagner, J. Foster, E. Brewer, and A. Aiken. A first step towards automated detection of buffer overrun vulnerabilities. In Proceedings of NDSS 2000, 2000.Google Scholar
- M. Zalewski. Multiple local sendmail vulnerabilities. http://razor.bindview.com/publish/advisories/adv_sm812.html.Google Scholar
- X. Zhang, A. Edwards, and T. Jaeger. Using CQUAL for static analysis of authorization hook placement. In Proceedings of the Eleventh Usenix Security Symposium, August 2002. Google ScholarDigital Library
Index Terms
- MOPS: an infrastructure for examining security properties of software
Recommendations
Model Checking of Component Protocol Conformance -- Optimizations by Reducing False Negatives
In past years, a number of works considered behavioral protocols of components and discussed approaches for automatically checking of compatibality of protocols (protocol conformance) in component-based systems. The approaches are usually model-checking ...
Bounded model checking of high-integrity software
HILT '13: Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technologyModel checking [5] is an automated algorithmic technique for exhaustive verification of systems, described as finite state machines, against temporal logic [9] specifications. It has been used successfully to verify hardware at an industrial scale [6]. ...
Handling loops in bounded model checking of C programs via k-induction
The first attempts to apply the k-induction method to software verification are only recent. In this paper, we present a novel proof by induction algorithm, which is built on the top of a symbolic context-bounded model checker and uses an iterative ...
Comments