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