Using simplex method in verifying software safety
DOI:
https://doi.org/10.2298/YJOR0901133VKeywords:
Simplex method, software safety, buffer overflowsAbstract
In this paper we have discussed the application of the Simplex method in checking software safety - the application in automated detection of buffer overflows in C programs. This problem is important because buffer overflows are suitable targets for hackers' security attacks and sources of serious program misbehavior. We have also described our implementation, including a system for generating software correctness conditions and a Simplex based theorem prover that resolves these conditions.References
Ackerman, W., Solvable cases of the decision problem, Studies in Logic and the Foundations of Mathematics, 1954.
Bland, R., G., “New finite pivoting rules for the simplex method”, Mathematics of Operations Research, 2 (2) (1977) 104-107.
Cowan, C., Wagle, P., Pu, C., Beattie, S., and Walpole, J., “Buffer overflows: Attacks and defenses for the vulnerability of the decade”, Proceedings of the DARPA Information Survivability Conference and Expo, 2000.
Dantzig, G., B., Linear Programming and Extensions, Princeton University Press, Princeton, NJ, 1963.
Davis, M., Logemann, G., and Loveland, D., “A machine program for theorem-proving”, Commun. ACM, 5 (7) (1962) 394-397.
Dor, N., Rodeh, M., and Sagiv, M., “Towards a realistic tool for statically detecting all buffer overflows in C”. in: Proceedings of the ACM SIG-PLAN 2003 conference on Programming Language Design and Implementation, ACM Press, New York, NY, USA, 2003, 155-167.
Dutertre, B., and De Moura, L., “A fast linear-arithmetic solver for dpll(t)”. CAV 2006, of LNCS, Springer, 2006, 41-44.
Dutertre, B., and De Moura, L., “Integrating Simplex with DPLL(T)”, Technical Report SRI CSL-06-01, SRI International, 2006.
Forsgren, A., Gill, P., E., and Wright, M., H., “Interior methods for nonlinear optimization” SIAM Rev, 44 (2002) 525-597.
Holzmann, G., “Static source code checking for user-defined properties” in: Proceedings of 6th World Conference on Integrated Design and Process Technology, Pasadena, CA, June 2002.
Klee, V., Minty, G., J., and Shisha, O.,”How good is the simplex algorithm?”, Inequalities 3, (1972) 159-175.
Kratkiewicz, K., and Lippmann, R., “Using a diagnostic corpus of c programs to evaluate buffer overflow detection by static analysis tools”, in: Workshop on the Evaluation of Software Defect Detection Tools, Chicago, 2005.
Larochelle, D., and Evans, D., “Statically detecting likely buffer overflow vulnerabilities”, in: USENIX Security Symposium, Washington D.C., 2001.
Lassez, J., L., and Maher, M.,J., “On Fourier's algorithm for linear arithmetic constraints”, Journal of Automated Reasoning, 9 (1992) 373-379.
Lemke, C., E., “The dual method of solving the linear programming problem” Naval Research Logistics Quarterly, (1954) 36-47.
Nieuwenhuis, R., Oliveras, A., and Tinelli, C., “Solving SAT and SAT Modulo Theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T)”, Journal of the ACM, 53 (6) (2006) 937-977.
Nocedal, J., and Wright, S., J., Numerical Optimization Springer-Verlag, New York, 1999.
Ranise, S., and Tinelli, C., “The SMT-LIB format”, An Initial Proposal 2003 on-line at: http://goedel.cs.uiowa.edu/smt-lib/
Secure software solutions. Rats, the rough auditing tool for security September 2001. on-line at: http://www.securesw.com/rats/.
Viega, J., Bloch, J.,T., Kohno, Y., and McGraw, G., “A static vulnerability scanner for C and C++ code”, in: 16th Annual Computer Security Applications Conference (ACSAC'00), 2000.
Viega, J., and McGraw, G., Building Secure Software, Addison-Wesley, 2002.
Wagner, D., Foster, J., Brewer, E., and Aiken, A., “A first step towards automated detection of buffer overrun vulnerabilities”, in: Symposium on Network and Distributed System Security, San Diego, CA, February 2000, 3-17.
Wheeler, D., Flawfinder, A., May 2001. on-line at: http://www.dwheeler.com/flawfinder/.
Wilander, J., and Kamkar, M., “A comparison of publicly available tools for static intrusion prevention”, in: Proceedings of the 7th Nordic Workshop on Secure IT Systems (Nordsec 2002), Karlstad, Sweden, November, 2002, 68-84.
Xie, Y., Chou, A., and Engler, D., Archer: using symbolic, path-sensitive analysis to detect memory access errors, in: Proceedings of the 9th European software engineering conference held jointly with 10th ACM SIGSOFT international symposium on Foundations of software engineering, 2003, 327-336.
Yorsh, G., and Dor, N., The Design of CoreC. 2003. on-line at: http://www.cs.tau.ac.il/gretay/GFC.htm.
Zitser, M., Lippmann, R., and Leek, T., “Testing static analysis tools using exploitable buffer overflows from open source code”, in: Proceedings of the 12th ACM SIGSOFT international symposium on Foundations of software engineering table of contents, Newport Beach, CA, USA, ACM, 2004, 97-106.
Downloads
Published
Issue
Section
License
Copyright (c) 2009 YUJOR
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
