Review form for CSEM-reviews 2003 ================================= Paper #6, "CSSV: Towards a Realistic Tool for Statically Detecting All Buffer Overflows in C" by Nurit Dor, Michael Rodeh and Mooly Sagiv. Reviewer: Andrzej Bednarski Short summary ------------- The authors describe C String Static Verifier (CSSV) tool capable of detecting all buffer overflows in C programs. The tool is capable of analyzing large programs, since it operates on procedure/function level independently. The analysis is not totally automatic (if accuracy is required): the user requires to specify precondition, postcondition as well as side effects (so called contracts). Contracts can be generated for each procedure automatically, but it results in more false-errors. Then, the tool performs static pointer analysis which is followed by a transformation of the C program into an integer program. CSSV performs abstract interpretation to detect and reports string buffer overflows. The main contributions ---------------------- Solve the problem of all buffer overflows in C. The tool make use of static detection of string errors in C programs. CSSV is an existing tool capable of finding string errors in real life applications. Merits and weaknesses --------------------- Merits: + CSSV tool is a static analysis tool. + Reliability: it detects all string manipulation errors that are subject to buffer overflows. + The tool handles pointer arithmetics for the analysis and error detection. + Also, the tool handles the whole C language. + The tool helps the user to fine-tune contracts by giving hints as error messages. Weaknesses: - There is no proof of completeness of the tool, that show all errors are detected. - Manual specification of the contracts to obtain valuable results. The automatically generated contracts produces many false alarms. - CSSV do not consider inter-procedural analysis. - The automatically generated pre/post conditions results in numerous false errors. Numerical rating ---------------- * Significance: 8 * Originality: 5 * Interest to a journal on programming languages and compiler technology: 3 * Quality of experimental evaluation: 7 * Overall organization: 6 * Presentation (language and style): 9 * Length appropriate: 4 * References appropriate: 8 * Overall evaluation: 7 * Recommendation: Accept * Your confidence in your review: 2 Comments to the authors ----------------------- The paper is well organized and follows the flow of the CSSV tool. However, a large part is dedicated to various definitions that do not help in understanding the algorithm/tool, but obfuscates the paper and makes it more difficult to read. Is it possible to prof that CSSV will not miss any buffer overflow of C applications? Minor remark: section 3.1, *PtrEndText = '\n'; should be *PtrEndLoc = '\n'; It is actually easy to verify *PtrEndText = '\n'. Suggestions for improvement --------------------------- The paper describes systematically the steps in CSSV. The theoretical part is quite heavy and difficult to follow - mainly for the numerous definitions and missing algorithms (pseudo code). The reader needs to refer to previous work and other mentioned techniques. This is not an easy task for a non-expert in this domain (this is my case). In my opinion CSSV paper is more suitable for a journal on computer security and reliability rather than programming languages and compiler technology.