"Improving Computer Security using Extended Static Checking"
             by Brian V. Chess
    	 IEEE S&P 2002
    
    Summary:
    
    This paper presents a way of finding security flaws in source code by way of 
static analysis. It allows the user to specify concrete security properties 
    as annotations to the source code, then further constructs a verification 
condition that can be analyzed by an automated theorem prover. A prototype 
implementation called Eau Claire has been created, which represents the first 
Extended Static Checking application specifically for identifying security 
vulnerabilities.
    
    Eau Claire deals with C code. Security properties for a function can be 
specified as preconditions, modifiable variables, and postconditions. These 
specifications along with the C code together are translated into a variation 
    of Dijkstra's Guarded Commands. For simplicity, this translation maintains 
    only a subset of C's semantics. The guarded commands can be faithfully 
    converted to a verification condition, which is fed into an automated theorem 
    proover to analyze.
    
    With regard to effectiveness, the author shows that Eau Clair is able to 
catch two real world security vulnerability cases: the RSAREF buffer overflow 
    and the Redhat  lpr race condition. Performance-wise, Eau Claire makes the 
    compile speed 25 times slower, which is practically non-usable at the develop 
    stage, but may well fit into the release process. 
    
    Discussion
    
    Pros:
    
    *This solution utilizes existing techniques such as guarded commands,  
verification condition construction, and theorem proving, combine them together 
     to provide a workable solution part of a very practical problem: finding 
security  flaws.
    
    *This is a static approach, which adds no runtime cost and is favorable as  
far as  performance is concerned. 
    
    *Eau Claire can be automated to check against growing source code on a  
regular  basis to catch some non-sophisticated yet common errors and  works as a 
heads up  for developers. It can also serve as a defense line  in the release 
process.
    
    *By using pre-existing specification libraries, some common  vulnerabilities 
can be caught without much extra work.
    
    *In terms of writing, the author does a good job describing the Guarded  
Commands, and gives a good summary of related work.
    
    
    Cons:
    
    * Eau Claire gives up soundness in favor of ease. Semantics modification
    such as   not handling function pointers or bit operators may hurt the
    practical usability   of this tool.
    
    * Given the over-simplification of the loop semantics and such, it would be 
interesting to show some results about the false positive rates.
    
    * Generating the specifications can be burdensome and programmers may not  be 
willing to do it.
    
    * The paper suffers because the author only provides two examples of
      his software finding security vulnerabilities in real-world applications,
      and these vulnerabilities were already well-known.  A much stronger
      approach would be for the author to pass a significantly-large set of
      source code (e.g. the source code for the GNU libc or the Linux operating
      system) through Eau Claire for analysis.
    
    * The author indicates that a majority of security vulnerabilities fall
      into the categories of array bounds errors and race conditions. In terms
      of finding array bounds errors, it seem that simple lexical analysis may
      be all that is necessary and that extended static checking is somewhat
      overkill.  In terms of finding race conditions, on the other hand, it
      seems that even extended static checking may be unable to all but the
      most straightforward of race conditions such as the lpr vulnerability
      cited by the author (which is actually of a class of race conditions
      known as Time Of Check To Time Of Use flaws).
    
    * Some programmers may misunderstand the results of Eau Claire.  For
      example, a given piece of software may not have any vulnerabilities
      within it, but may link to libraries that are vulnerable.
    
    * Static analysis seems to be constrained to finding only a specific
      subset of security vulnerabilities due to issues of undecidability, etc.
      Given these constraints, it seems that simpler methods such as simple
      lexical analysis of a source code might be just as good as extended
      static checking.
    
    * Since it's dealing with high level source code instead of binaries as
      Proof-carrying Code does, wouldn't it be easier to choose a type safe 
      language in the first place?
    
    
    Vote Results
    
      Strong Accept - 0
      Weak Accept - 8
      Weak Reject - 3
      Strong Reject - 0