False Negative when using Polyspace Code Prover

13 visualizaciones (últimos 30 días)
HONGJUN CHOI
HONGJUN CHOI el 1 de Mayo de 2020
Comentada: HONGJUN CHOI el 18 de Mayo de 2020
Christian Bard ha marcado con alerta este/a pregunta
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.
  1 comentario
Matt Rhodes
Matt Rhodes el 11 de Mayo de 2020
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.

Iniciar sesión para comentar.

Respuesta aceptada

Anirban
Anirban el 7 de Mayo de 2020
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.
  4 comentarios
Anirban
Anirban el 11 de Mayo de 2020
Editada: Anirban el 11 de Mayo de 2020
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
HONGJUN CHOI el 18 de Mayo de 2020
Hi Anirban,
Sorry I didn't see that it was caused by not specifying the main function entry point.
Thanks for the kind explanation!

Iniciar sesión para comentar.

Más respuestas (0)

Productos


Versión

R2020a

Community Treasure Hunt

Find the treasures in MATLAB Central and discover how the community can help you!

Start Hunting!

Translated by