False Negative when using Polyspace Code Prover

Hello.

I am a beginner who is interested in Polyspace tool.

On page 63 of the Polyspace® Code Prover ™ Getting Started Guide, Code Prover says there are no false negatives.

However, as a result of static analysis of a part of NIST Juliet Test Suite for C / C ++ using Polyspace Code Prover, false negatives existed in the following CWE ID.

1. CWE 126 (Buffer Over-read)
2. CWE 561 (Dead Code)
3. CWE 674 (Uncontrolled Recursion)
4. CWE 835 (Loop with Unreachable Exit Condition ('Infinite Loop'))

I've analyzed the code, but I'm asking because I can't figure out why false negatives are occurring.

- Example of CWE 561 True Positive(Code Prover detects it.)

void CWE561_Dead_Code__return_before_code_01_bad ()

{

     return;

     / * FLAW: code after the 'return' * /

     printLine ("Hello");

}

- Example of CWE 561 False Negative(Code Prover cannot be detected)

static void helperBad ()

{

     printLine ("helperBad ()");

}

There is no call to helperBad function anywhere.

[Matt Rhodes]

Hi Hongjun,

Dead code is a very ambiguous term. You can have logically unreacheable code (which is the primary check for Code Prover) and uncalled functions (functions in your code base that are not called by anything). Code prover will find both, without false negatives, within the scope of the assumptions provided for the proof.

In this second example case, what you have might be an uncalled function, if it is called nowhere else in the code base. And, this instance could point to an incorrect behavior, but all the code presented is actually logically reachable.

For this kind of issue, if it is important to you, you are better off with a heuristic search to find all of the cases of function calls in string literals. The difficult aspect of this is that, without knowing your requirements, it is impossible to know whether it is intentional to just have a string literal refering to a function, or to have a value returned to be included in the string. The context might provide some clues too. In this contrived example, I would question the validity of any proving tool that claimed it found this to be dead code.

Answer 1

[Anirban]

Hi Hongjun,

For the two specific examples you give, you have to turn on the checks Function not called and Function not reachable. Often users are not interested in these two checks, for instance, because they are running Code Prover on units and some functions might be uncalled within an unit but eventually will get called from another unit. So these two checks are disabled by default. To enable them, use this option.

For all options related to tuning Code Prover checks, see the sections Check Behavior and Verification Assumptions.

[HONGJUN CHOI]

Hi Anirban,

Thanks for the explanation. The default value is none, so I changed it to ALL and performed code prover. However, the result was the same. Why does False Negative exist?

[HONGJUN CHOI]

Is it possible to check for flase negative from other CWEs?

The original Juliet file and necessary headers are here.

https://samate.nist.gov/SARD/testsuites/juliet/Juliet_Test_Suite_v1.3_for_C_Cpp.zip

• CWE 126 (Buffer Over-read)

/* TEMPLATE GENERATED TESTCASE FILE
Filename: CWE126_Buffer_Overread__char_declare_memcpy_32.c
Label Definition File: CWE126_Buffer_Overread.stack.label.xml
Template File: sources-sink-32.tmpl.c
*/
/*
 * @description
 * CWE: 126 Buffer Over-read
 * BadSource:  Set data pointer to a small buffer
 * GoodSource: Set data pointer to a large buffer
 * Sink: memcpy
 *    BadSink : Copy data to string using memcpy
 * Flow Variant: 32 Data flow using two pointers to the same value within the same function
 *
 * */

#include "std_testcase.h"

#include <wchar.h>

#ifndef OMITBAD

void CWE126_Buffer_Overread__char_declare_memcpy_32_bad()
{
    char * data;
    char * *dataPtr1 = &data;
    char * *dataPtr2 = &data;
    char dataBadBuffer[50];
    char dataGoodBuffer[100];
    memset(dataBadBuffer, 'A', 50-1); /* fill with 'A's */
    dataBadBuffer[50-1] = '\0'; /* null terminate */
    memset(dataGoodBuffer, 'A', 100-1); /* fill with 'A's */
    dataGoodBuffer[100-1] = '\0'; /* null terminate */
    {
        char * data = *dataPtr1;
        /* FLAW: Set data pointer to a small buffer */
        data = dataBadBuffer;
        *dataPtr1 = data;
    }
    {
        char * data = *dataPtr2;
        {
            char dest[100];
            memset(dest, 'C', 100-1);
            dest[100-1] = '\0'; /* null terminate */
            /* POTENTIAL FLAW: using memcpy with the length of the dest where data
             * could be smaller than dest causing buffer overread */
            memcpy(dest, data, strlen(dest)*sizeof(char));
            dest[100-1] = '\0';
            printLine(dest);
        }
    }
}

#endif /* OMITBAD */

#ifndef OMITGOOD

/* goodG2B() uses the GoodSource with the BadSink */
static void goodG2B()
{
    char * data;
    char * *dataPtr1 = &data;
    char * *dataPtr2 = &data;
    char dataBadBuffer[50];
    char dataGoodBuffer[100];
    memset(dataBadBuffer, 'A', 50-1); /* fill with 'A's */
    dataBadBuffer[50-1] = '\0'; /* null terminate */
    memset(dataGoodBuffer, 'A', 100-1); /* fill with 'A's */
    dataGoodBuffer[100-1] = '\0'; /* null terminate */
    {
        char * data = *dataPtr1;
        /* FIX: Set data pointer to a large buffer */
        data = dataGoodBuffer;
        *dataPtr1 = data;
    }
    {
        char * data = *dataPtr2;
        {
            char dest[100];
            memset(dest, 'C', 100-1);
            dest[100-1] = '\0'; /* null terminate */
            /* POTENTIAL FLAW: using memcpy with the length of the dest where data
             * could be smaller than dest causing buffer overread */
            memcpy(dest, data, strlen(dest)*sizeof(char));
            dest[100-1] = '\0';
            printLine(dest);
        }
    }
}

void CWE126_Buffer_Overread__char_declare_memcpy_32_good()
{
    goodG2B();
}

#endif /* OMITGOOD */

/* Below is the main(). It is only used when building this testcase on
 * its own for testing or for building a binary to use in testing binary
 * analysis tools. It is not used when compiling all the testcases as one
 * application, which is how source code analysis tools are tested.
 */
#ifdef INCLUDEMAIN

int main(int argc, char * argv[])
{
    /* seed randomness */
    srand( (unsigned)time(NULL) );
#ifndef OMITGOOD
    printLine("Calling good()...");
    CWE126_Buffer_Overread__char_declare_memcpy_32_good();
    printLine("Finished good()");
#endif /* OMITGOOD */
#ifndef OMITBAD
    printLine("Calling bad()...");
    CWE126_Buffer_Overread__char_declare_memcpy_32_bad();
    printLine("Finished bad()");
#endif /* OMITBAD */
    return 0;
}

#endif

• CWE 674 (Uncontrolled Recursion)

/*
 * @description Uncontrolled Recursion
 *
 * */

#include "std_testcase.h"

#ifndef OMITBAD

static void helperBad(unsigned level)
{
    /* FLAW: Although this cannot cause "infinite" recursion, it is essentially limited to UINT_MAX
     * which is rather large on most systems */
    if (level == 0) 
    {
        return;
    }

    helperBad(level - 1);
}

void CWE674_Uncontrolled_Recursion__unbounded_recursive_call_01_bad()
{
    helperBad(UINT_MAX);
}

#endif /* OMITBAD */

#ifndef OMITGOOD

#define MAX_RECURSION 10

static void helperGood(unsigned level)
{
    /* FIX: limit recursion to a sane level */
    if (level > MAX_RECURSION) 
    {
        printLine("ERROR IN RECURSION");
        return;
    }

    if (level == 0) 
    {
        return;
    }

    helperGood(level - 1);
}

static void good1()
{
    helperGood(UINT_MAX);
}

void CWE674_Uncontrolled_Recursion__unbounded_recursive_call_01_good()
{
    good1();
}

#endif /* OMITGOOD */

/* Below is the main(). It is only used when building this testcase on
 * its own for testing or for building a binary to use in testing binary
 * analysis tools. It is not used when compiling all the testcases as one
 * application, which is how source code analysis tools are tested. 
 */

#ifdef INCLUDEMAIN

int main(int argc, char * argv[])
{
    /* seed randomness */
    srand( (unsigned)time(NULL) );
#ifndef OMITGOOD
    printLine("Calling good()...");
    CWE674_Uncontrolled_Recursion__unbounded_recursive_call_01_good();
    printLine("Finished good()");
#endif /* OMITGOOD */
#ifndef OMITBAD
    printLine("Calling bad()...");
    CWE674_Uncontrolled_Recursion__unbounded_recursive_call_01_bad();
    printLine("Finished bad()");
#endif /* OMITBAD */
    return 0;
}

#endif

• CWE 835 (Loop with Unreachable Exit Condition ('Infinite Loop'))

/*
 * @description Infinite Loop - do..while()
 * 
 * */

#include "std_testcase.h"

#ifndef OMITBAD

void CWE835_Infinite_Loop__do_true_01_bad() 
{
    int i = 0;
    
    /* FLAW: Infinite Loop - do..while(true) with no break point */
    do
    {
        printIntLine(i);
        i++;
    } while(1);
}

#endif /* OMITBAD */


#ifndef OMITGOOD

static void good1() 
{
    int i = 0;

    do 
    {
        /* FIX: Add a break point for the loop if i = 10 */
        if (i == 10) 
        { 
            break; 
        }
        printIntLine(i);
        i++;
    } while(1);
}

void CWE835_Infinite_Loop__do_true_01_good() 
{
    good1();
}

#endif /* OMITGOOD */

/* Below is the main(). It is only used when building this testcase on 
 * its own for testing or for building a binary to use in testing binary 
 * analysis tools. It is not used when compiling all the testcases as one 
 * application, which is how source code analysis tools are tested. 
 */

#ifdef INCLUDEMAIN

int main(int argc, char * argv[]) 
{
    /* seed randomness */
    srand( (unsigned)time(NULL) );

#ifndef OMITGOOD
    printLine("Calling good()...");
    CWE835_Infinite_Loop__do_true_01_good();
    printLine("Finished good()");
#endif /* OMITGOOD */

#ifndef OMITBAD
    printLine("Calling bad()...");
    CWE835_Infinite_Loop__do_true_01_bad();
    printLine("Finished bad()");
#endif /* OMITBAD */

    return 0;
} 

#endif

[Anirban]

Hi Hongjun,

Sorry for the incompleteness of my previous answer. Code Prover does require a little bit of setup, so just those code snippets by themselves will not trigger the results you expect. Before I explain why, let me give another suggestion.

Since you have Code Prover, you also have Bug Finder. So, if you run Bug Finder simply after enabling all checkers using the option Find defects (-checkers), you should see the issues you expect to see. No other setup should be needed. Bug Finder is the tool recommended for CWE, partly because of its simplicity. See more details in CWE Coding Standard and Polyspace Results.

Code Prover will also detect the issues. Because Code Prover is more exhaustive, it is likely to have no false negatives in much more complicated scenarios (not just the simple ones in the tests). But the caveat is Code Prover will require some initial setup effort on your part.

For the two specific examples in your original question, if you want to use Code Prover, besides enabling the option to detect uncalled and unreachable functions, you also have to tune what are called the main-generator options, specifically the option -main-generator-calls. To achieve exhaustive proof for a complete application, a Code Prover analysis starts from main and then goes down the call tree. If you do not have a complete application and hence do not have a main, Code Prover generates one. By default, the generated main calls all functions that are not called anywhere in the code provided to Polyspace. Because the generated main calls helperBad, it is not considered as uncalled. To work around this issue, you have to explicitly specify during setup how the generated main is created (or provide a main yourself). I did the following. On this code:

void CWE561_Dead_Code__return_before_code_01_bad ()
{
     return;
     // FLAW: code after the 'return' 
     printLine ("Hello");
}

void printLine(char* str) {
    
}

static void helperBad ()
{
     printLine ("helperBad ()");
}

I ran Code Prover using these options:

-main-generator -main-generator-calls custom=CWE561_Dead_Code__return_before_code_01_bad -uncalled-function-checks all

I see the expected results. If you are using the graphical user interface, you can figure out the equivalent options from the links above. I also found the expected issues using Bug Finder by enabling all checkers.

As for your bigger question about the NIST Juliet Test Suite for C / C ++, please contact MathWorks Technical Support. I believe they have run the tools on this test suite and can discuss all cases with you.

[HONGJUN CHOI]

Hi Anirban,

Sorry I didn't see that it was caused by not specifying the main function entry point.

Thanks for the kind explanation!