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.