当使用Polyspace代码验证时，错误否定

4次浏览(最近30天)

显示旧的评论

HONGJUN崔 2020年5月1日

评论道: HONGJUN崔2020年5月18日

答:接受 Anirban

这个问题被标记为基督教的吟游诗人

显示标志

你好。

我是一个对Polyspace工具感兴趣的初学者。

在Polyspace®代码验证器™入门指南的第63页，代码验证器说没有假阴性。

然而，通过使用Polyspace Code Prover对NIST Juliet Test Suite for C / c++的一部分进行静态分析，发现在以下CWE ID中存在假阴性。

CWE 126(缓冲区过载)
CWE 561(失效代码)
CWE 674(非受控递归)
CWE 835(无法到达退出条件的循环(“无限循环”))

我分析了代码，但我还是问了因为我不明白为什么会出现假阴性。

- CWE 561 True Positive(代码验证器检测到它)的示例。

空白CWE561_Dead_Code__return_before_code_01_bad ()

｛

返回;

/ *缺陷:代码后的'return' * /

printLine(“Hello”);

｝

- CWE 561假阴性(无法检测到代码验证器)的例子

static void helperBad ()

｛

printLine(“helperBad () ");

｝

任何地方都没有调用helperBad函数。

1评论
显示隐藏 None

马特·罗兹 2020年5月11日

嗨Hongjun,

死代码是一个非常模棱两可的术语。您可以有逻辑上不可访问的代码(这是代码验证器的主要检查)和未调用的函数(代码库中没有被任何东西调用的函数)。代码验证器会找到两者，没有假阴性，在为证明所提供的假设范围内．

在第二个例子中可能如果它在代码库中没有被调用，则它是一个未被调用的函数。而且，这个实例可能指向一个不正确的行为，但是所提供的所有代码实际上在逻辑上是可访问的。

对于这类问题，如果它对您很重要，那么您最好使用启发式搜索，以字符串字面量查找所有函数调用的情况。这样做的困难之处在于，在不知道您的需求的情况下，就不可能知道是故意让一个字符串字面量引用一个函数，还是让返回的值包含在字符串中。背景也可能提供一些线索。在这个人为的例子中，我将质疑任何声称发现这是死代码的证明工具的有效性。

登录评论。

登录回答这个问题。

接受的答案

Anirban 2020年5月7日

0
链接

直接链接到这个答案

//www.tatmou.com/matlabcentral/answers/522161-false-negative-when-using-polyspace-code-prover#answer_431071

嗨Hongjun,

对于你给出的两个具体例子，你必须打开检查函数不叫和函数不可以．用户通常对这两种检查不感兴趣，例如，因为他们正在单元上运行代码验证程序，而一些函数可能在单元内未被调用，但最终会从另一个单元调用。这两个检查默认是禁用的。要启用它们，请使用它们这个选项．

有关调优代码验证器检查的所有选项，请参阅本节检查行为和验证假设．

4评论
显示隐藏 3年长的评论

HONGJUN崔 2020年5月11日

是否可以从其他ccie中检查出flase阴性?

原始的朱丽叶文件和必要的头文件在这里。

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

CWE 126(缓冲区过载)

                             / *模板生成TESTCASE文件
                            
                             文件名:CWE126_Buffer_Overread__char_declare_memcpy_32.c
                            
                             标签定义文件:CWE126_Buffer_Overread.stack.label.xml
                            
                             模板文件:来源- - 32. tmpl.c下沉
                            
                             *／
                            
                             ／*
                            
                             * @description
                            
                             * CWE: 126缓冲上了
                            
                             * BadSource:设置数据指向小缓冲区的指针
                            
                             * GoodSource:设置数据指向大缓冲区的指针
                            
                             *水槽:memcpy
                            
                             BadSink:拷贝数据使用memcpy设置字符串
                            
                             *流量变体:32数据在同一个函数中使用两个指向相同值的指针进行流处理
                            
                             ＊
                            
                             * * /
                            
                             ＃包括“std_testcase.h”
                            
                             ＃包括< wchar.h >
                            
                             ＃如果未定义OMITBAD
                            
                             无效CWE126_Buffer_Overread__char_declare_memcpy_32_bad ()
                            
                             ｛
                            
                             char *数据;
                            
                             char * *dataPtr1 = &data;
                            
                             char * *dataPtr2 = &data;
                            
                             char dataBadBuffer [50];
                            
                             char dataGoodBuffer [100];
                            
                             memset (dataBadBuffer,“一个”、博彩);/ *充满“一个”s * /
                            
                             博彩dataBadBuffer [] =' \ 0；/* null terminate */
                            
                             memset (dataGoodBuffer,“一个”, 100 - 1);/ *充满“一个”s * /
                            
                             dataGoodBuffer (100 - 1) =' \ 0；/* null terminate */
                            
                             ｛
                            
                             char *data = *dataPtr1;
                            
                             /*漏洞:设置数据指针到一个小的缓冲区*/
                            
                             数据= dataBadBuffer;
                            
                             * dataPtr1 =数据;
                            
                             ｝
                            
                             ｛
                            
                             char *data = *dataPtr2;
                            
                             ｛
                            
                             char dest [100];
                            
                             memset(桌子,“C”, 100 - 1);
                            
                             (100 - 1) =不在座位上' \ 0；/* null terminate */
                            
                             /*可能的缺陷:使用memcpy与dest的长度，其中数据
                            
                             *可能比dest小，导致缓冲区过载*/
                            
                             memcpy(服务台、数据strlen(桌子)* sizeof (char));
                            
                             (100 - 1) =不在座位上' \ 0；
                            
                             printLine(桌子);
                            
                             ｝
                            
                             ｝
                            
                             ｝
                            
                             ＃endif /* OMITBAD */
                            
                             ＃如果未定义OMITGOOD
                            
                             / * goodG2B()使用使用BadSink */的GoodSource
                            
                             静态空白goodG2B ()
                            
                             ｛
                            
                             char *数据;
                            
                             char * *dataPtr1 = &data;
                            
                             char * *dataPtr2 = &data;
                            
                             char dataBadBuffer [50];
                            
                             char dataGoodBuffer [100];
                            
                             memset (dataBadBuffer,“一个”、博彩);/ *充满“一个”s * /
                            
                             博彩dataBadBuffer [] =' \ 0；/* null terminate */
                            
                             memset (dataGoodBuffer,“一个”, 100 - 1);/ *充满“一个”s * /
                            
                             dataGoodBuffer (100 - 1) =' \ 0；/* null terminate */
                            
                             ｛
                            
                             char *data = *dataPtr1;
                            
                             /*修正:设置数据指针到一个大的缓冲区*/
                            
                             数据= dataGoodBuffer;
                            
                             * dataPtr1 =数据;
                            
                             ｝
                            
                             ｛
                            
                             char *data = *dataPtr2;
                            
                             ｛
                            
                             char dest [100];
                            
                             memset(桌子,“C”, 100 - 1);
                            
                             (100 - 1) =不在座位上' \ 0；/* null terminate */
                            
                             /*可能的缺陷:使用memcpy与dest的长度，其中数据
                            
                             *可能比dest小，导致缓冲区过载*/
                            
                             memcpy(服务台、数据strlen(桌子)* sizeof (char));
                            
                             (100 - 1) =不在座位上' \ 0；
                            
                             printLine(桌子);
                            
                             ｝
                            
                             ｝
                            
                             ｝
                            
                             无效CWE126_Buffer_Overread__char_declare_memcpy_32_good ()
                            
                             ｛
                            
                             goodG2B ();
                            
                             ｝
                            
                             ＃endif /* OMITGOOD */
                            
                             / *以下是main()。它只在构建这个测试用例时使用
                            
                             *自己的用于测试或构建用于测试二进制文件的二进制文件
                            
                             *分析工具。它是当将所有测试用例编译为一个时不使用
                            
                             *应用程序,源代码分析工具是如何测试的。
                            
                             *／
                            
                             ＃如果定义了INCLUDEMAIN
                            
                             intMain (int argc, char * argv[])
                            
                             ｛
                            
                             /*种子随机*/
                            
                             将srand ((unsigned)时间(NULL));
                            
                             ＃如果未定义OMITGOOD
                            
                             printLine (“打电话好()……”）;
                            
                             CWE126_Buffer_Overread__char_declare_memcpy_32_good ();
                            
                             printLine (“完成好()”）;
                            
                             ＃endif /* OMITGOOD */
                            
                             ＃如果未定义OMITBAD
                            
                             printLine (“叫坏()……”）;
                            
                             CWE126_Buffer_Overread__char_declare_memcpy_32_bad ();
                            
                             printLine (“完成坏()”）;
                            
                             ＃endif /* OMITBAD */
                            
                             返回0；
                            
                             ｝
                            
                             ＃endif

CWE 674(非受控递归)

                             ／*
                            
                             * @description不受控制递归
                            
                             ＊
                            
                             * * /
                            
                             ＃包括“std_testcase.h”
                            
                             ＃如果未定义OMITBAD
                            
                             静态空白helperBad(无符号级别)
                            
                             ｛
                            
                             /*缺陷:虽然这不能导致“无限”递归，本质上限制在UINT_MAX
                            
                             *在大多数系统中是相当大的*/
                            
                             如果(要求等级= = 0)
                            
                             ｛
                            
                             返回；
                            
                             ｝
                            
                             helperBad(- 1)水平;
                            
                             ｝
                            
                             无效CWE674_Uncontrolled_Recursion__unbounded_recursive_call_01_bad ()
                            
                             ｛
                            
                             helperBad (UINT_MAX);
                            
                             ｝
                            
                             ＃endif /* OMITBAD */
                            
                             ＃如果未定义OMITGOOD
                            
                             ＃定义MAX_RECURSION10
                            
                             静态空白helperGood(无符号级别)
                            
                             ｛
                            
                             /*修正:限制递归到合理的级别*/
                            
                             如果(要求等级> MAX_RECURSION)
                            
                             ｛
                            
                             printLine (“递归错误”）;
                            
                             返回；
                            
                             ｝
                            
                             如果(要求等级= = 0)
                            
                             ｛
                            
                             返回；
                            
                             ｝
                            
                             helperGood(- 1)水平;
                            
                             ｝
                            
                             静态空白good1 ()
                            
                             ｛
                            
                             helperGood (UINT_MAX);
                            
                             ｝
                            
                             无效CWE674_Uncontrolled_Recursion__unbounded_recursive_call_01_good ()
                            
                             ｛
                            
                             good1 ();
                            
                             ｝
                            
                             ＃endif /* OMITGOOD */
                            
                             / *以下是main()。它只在构建这个测试用例时使用
                            
                             *自己的用于测试或构建用于测试二进制文件的二进制文件
                            
                             *分析工具。它是当将所有测试用例编译为一个时不使用
                            
                             *应用程序,源代码分析工具是如何测试的。
                            
                             *／
                            
                             ＃如果定义了INCLUDEMAIN
                            
                             intMain (int argc, char * argv[])
                            
                             ｛
                            
                             /*种子随机*/
                            
                             将srand ((unsigned)时间(NULL));
                            
                             ＃如果未定义OMITGOOD
                            
                             printLine (“打电话好()……”）;
                            
                             CWE674_Uncontrolled_Recursion__unbounded_recursive_call_01_good ();
                            
                             printLine (“完成好()”）;
                            
                             ＃endif /* OMITGOOD */
                            
                             ＃如果未定义OMITBAD
                            
                             printLine (“叫坏()……”）;
                            
                             CWE674_Uncontrolled_Recursion__unbounded_recursive_call_01_bad ();
                            
                             printLine (“完成坏()”）;
                            
                             ＃endif /* OMITBAD */
                            
                             返回0；
                            
                             ｝
                            
                             ＃endif

CWE 835(无法到达退出条件的循环(“无限循环”))

                             ／*
                            
                             * @description无限循环——做. .而()
                            
                             ＊
                            
                             * * /
                            
                             ＃包括“std_testcase.h”
                            
                             ＃如果未定义OMITBAD
                            
                             无效CWE835_Infinite_Loop__do_true_01_bad ()
                            
                             ｛
                            
                             Int I = 0;
                            
                             /*缺陷:Infinite Loop - do..而(真正的)没有断点*/
                            
                             做
                            
                             ｛
                            
                             printIntLine(我);
                            
                             我+ +;
                            
                             ｝而（1）；
                            
                             ｝
                            
                             ＃endif /* OMITBAD */
                            
                             ＃如果未定义OMITGOOD
                            
                             静态空白good1 ()
                            
                             ｛
                            
                             Int I = 0;
                            
                             做
                            
                             ｛
                            
                             /*修正:添加打破点For循环if I = 10 */
                            
                             如果(我= = 10)
                            
                             ｛
                            
                             打破；
                            
                             ｝
                            
                             printIntLine(我);
                            
                             我+ +;
                            
                             ｝而（1）；
                            
                             ｝
                            
                             无效CWE835_Infinite_Loop__do_true_01_good ()
                            
                             ｛
                            
                             good1 ();
                            
                             ｝
                            
                             ＃endif /* OMITGOOD */
                            
                             / *以下是main()。它只在构建这个测试用例时使用
                            
                             *自己的用于测试或构建用于测试二进制文件的二进制文件
                            
                             *分析工具。它是当将所有测试用例编译为一个时不使用
                            
                             *应用程序,源代码分析工具是如何测试的。
                            
                             *／
                            
                             ＃如果定义了INCLUDEMAIN
                            
                             intMain (int argc, char * argv[])
                            
                             ｛
                            
                             /*种子随机*/
                            
                             将srand ((unsigned)时间(NULL));
                            
                             ＃如果未定义OMITGOOD
                            
                             printLine (“打电话好()……”）;
                            
                             CWE835_Infinite_Loop__do_true_01_good ();
                            
                             printLine (“完成好()”）;
                            
                             ＃endif /* OMITGOOD */
                            
                             ＃如果未定义OMITBAD
                            
                             printLine (“叫坏()……”）;
                            
                             CWE835_Infinite_Loop__do_true_01_bad ();
                            
                             printLine (“完成坏()”）;
                            
                             ＃endif /* OMITBAD */
                            
                             返回0；
                            
                             ｝
                            
                             ＃endif

Anirban 2020年5月11日

嗨Hongjun,

很抱歉我之前的回答不完整。代码验证器确实需要一些设置，因此仅凭这些代码片段本身不会触发您期望的结果。在我解释原因之前，让我再提一个建议。

既然你有代码验证器，你也有Bug查找器。所以，如果你在启用后运行Bug Finder 所有使用选项的检查器发现缺陷(检查) ，您应该看到您期望看到的问题。不需要其他设置。Bug Finder是推荐给CWE的工具，部分原因是它的简单性。详情请参阅 CWE编码标准和多空间结果．

代码验证器也将检测问题。因为代码验证器更详尽，所以在更复杂的场景(不仅仅是测试中的简单场景)中很可能不会出现假阴性。但需要注意的是，代码验证程序需要您进行一些初始设置工作。

对于您最初问题中的两个特定示例，如果您想使用Code Prover，除了启用检测未调用和不可达函数的选项外，还必须调优被称为主发电机的选择，特别是选项 -main-generator-calls ．要为一个完整的应用程序实现详尽的证明，首先要进行代码验证分析主要然后沿着呼叫树向下。如果您没有一个完整的应用程序，因此没有主要，代码验证器生成一个。缺省情况下，生成的主要调用提供给Polyspace的代码中任何地方都没有调用的所有函数。因为生成的主要调用 helperBad ，它不被认为是未调用的。要解决这个问题，必须在设置期间显式指定如何生成主要创建(或提供主要你自己)。我做了以下事情。这段代码:

                             无效CWE561_Dead_Code__return_before_code_01_bad ()
                            
                             ｛
                            
                             返回；
                            
                             //缺陷:代码后“返回”
                            
                             printLine (“你好”）;
                            
                             ｝
                            
                             无效printLine (char * str) {
                            
                             ｝
                            
                             静态空白helperBad ()
                            
                             ｛
                            
                             printLine (“helperBad()”）;
                            
                             ｝

我使用以下选项运行代码验证程序:

                             -main-generator- main-generator-calls自定义=CWE561_Dead_Code__return_before_code_01_bad函数检查所有
                            

我看到了预期的结果。如果您正在使用图形用户界面，您可以从上面的链接中找出等价的选项。通过启用所有检查器，我还在Bug Finder中发现了预期的问题。

至于你更大的问题，关于NIST朱丽叶测试套件的C / c++，请联系 MathWorks技术支持金宝app ．我相信他们已经在这个测试套件上运行了工具，可以和你讨论所有的案例。

HONGJUN崔 2020年5月18日

嗨Anirban,

抱歉，我没有看到这是由于没有指定主函数入口点造成的。

谢谢您的解释!

登录评论。

当使用Polyspace代码验证时，错误否定

1评论
显示隐藏 None

接受的答案

4评论
显示隐藏 3年长的评论

更多的答案(0)

另请参阅

类别

标签

下载188bet金宝搏

释放

社区寻宝

当使用Polyspace代码验证时，错误否定

1评论 显示隐藏 None

接受的答案

4评论 显示隐藏 3年长的评论

更多的答案(0)

另请参阅

类别

标签

下载188bet金宝搏

释放

社区寻宝

1评论
显示隐藏 None

4评论
显示隐藏 3年长的评论