These are files to allow you to reproduce the results in "SATE V
Ockham Sound Analysis Criteria" NIST-IT 8113, available at
http://dx.doi.org/10.6028/NIST.IR.8113

These are available on-line at https://s3.amazonaws.com/nist-ockham-criteria-sate-v-data/ockhamCriteriaSATEVdata.tar.xz

    This is an experimental system. NIST assumes no responsibility
    whatsoever for its use by other parties and makes no guaranties,
    expressed or implied, about its quality, reliability, or any other
    characteristic.

    Certain commercial equipment or materials are identified in this
    article to specify the experimental procedure adequately. Such
    identification is not intended to imply recommendation or
    endorsement by NIST, nor is it intended to imply that the
    materials or equipment identified are necessarily the best
    available for the purpose.

    The files submissionComments, frama_c_report.allocfail.xml, and
    frama_c_report.succalloc.xml came from Frama-C.  All other
    software, data, and files were developed at the National Institute
    of Standards and Technology by employees of the Federal Government
    in the course of their official duties.  Pursuant to title 17
    Section 105 of the United States Code they are not subject to
    copyright protection and are in the public domain.

During the original analysis, we changed many files and scripts.  The
file names, directory structures, and other names were not always
consistent.  In addition, different people kept different pieces.  In
other words, this is more like what the analysis would have been if we
had known what to do in the beginning and made fewer mistakes.

In May 2017 we discovered two systematic bugs. The first bug was that
sites with post-increment (e.g., i++) were not extracted for integer
overflow.  This does not change the ultimate result, since Juliet does
not have any buggy cases of integer overflow in post-increments.  The
bug fix increased the reported number of sites and the reported number
of findings, but had no other effect.  The code changes are in
int_overflow.py and int_underflow.py.

The second bug was that four functions were counted as reading from a
buffer, like strcpy() or strncat() do, but they do not read from a
buffer.  These functions were:
    memset()
    wmemset() 
    snprintf()
    fgets()
This does not change the ultimate result, since Juliet does not
(cannot!) have buggy cases of read outside buffer with these
functions.  The bug fix decreased the reported number of sites and the
reported number of findings, but had no other effect.  The code
changes are in buffer_read.py.

CONTENTS OF MAIN DIRECTORY

frama_c_report.allocfail.xml and frama_c_report.succalloc.xml are the
warnings from Frama-C.  The first, allocfail, models every allocation
as failure.  The second models every allocation as success.  The union
of the two is all warnings from Frama-C.

Frama-C sent comments about their submission.  It explains some of the
behavior and decisions about Frama-C. The file is submissionComments.

*ExtractSites
  The scripts, program, and support material to extract sites from the
  Juliet test cases.
  *selected_Juliet_tests
    The .c test files for the selected CWEs.  This constitutes the
    test material for SATE V Ockham Criteria.  Because of human error,
    no files under CWE191 were processed, so CWE191 is not included.
    We also excluded some test cases that had erroneous behavior.

*ExtractWarnings
  The only significant content is the program to extract warnings from
  the two Frama-C files, mentioned above, and assign them to classes.
  It is named extract_warnings.  The output is in frama_c_warnings.csv

*Class_*
  One subdirectory for each class of warning. 


GENERAL RUN ARCHITECTURE

There are two major inputs: the warnings from Frama-C and the Juliet
test case programs, more specifically, the sites from the Juliet cases.

One program, extract_warnings, extracts and reformats all warnings from
Frama-C.  In contrast, one program for each class extracts sites from
the Juliet cases.  There are a few reasons why.
    One program, and one output file, for warnings allows us to be
sure that every Frama-C warning is considered, and that no warning is
put in more than one class.  The output file is in a comma-separated-
value (CSV) format, making it easy to use grep to select the warnings
for each class.
    Sites are different.  A single statement may have many sites for
different classes.  More importantly, the sites files are huge, 10 to
15 megabytes, and the extraction takes half an hour for each class of
sites.  In addition, the output is in XML, which is harder to separate
by class.



SOFTWARE

This analysis was run on Ubuntu 14.04 LTS.  The reanalysis in 2017 was
run on Ubuntu 16.04 LTS.  The major software packages used for this
analysis are:
    Python
    Perl
    make
We also used the following Unix utilities:
    grep
    comm
    sort
    echo
    mv
    test
    wc
    rm
Caution: these make extensive use of sorting and comparing, which
depends on the LC_COLLATE shell environment variable.  A later run may
have an error about a file out of order if runs are done with
different settings.


About discrimination
Vadim Okun suggested that we compute Frama-C's discrimination.
Briefly, a tool gets one point if it warns about a buggy site and does
not warn about the parallel good site.  We will concentrate on those
test cases that are made for that weakness class, e.g., only read
outside buffer findings in cases beginning with CWE126_Buffer_ or
CWE127_Buffer_ .

Since we showed that every buggy site has a warning (since no finding
matches a buggy site), all we have to do is consider good sites
without warnings.

The maximum number of points is the number of test cases with a
finding, since a finding is a (good) site without a finding.  The
problem is that some test cases are constructed with more than one
buggy site or more than one parallel good site.

The minimum number of points is the number of test cases with exactly
one warning - any more than one might be a warning on a good site.

Divide the minimum or maximum points by the number of test cases meant
for that CWE gives the minimum or maximum discrimination.

end of README
