Polyspace Server™for Ada是一个良好的静态分析引擎,它可以证明Ada83和Ada95代码中没有溢出、除零、越界数组访问和某些其他运行时错误。它对所有可能的控制和数据流(包括多线程代码)执行过程间分析,以确定每个操作总是安全的、总是错误的、不可访问的或易受攻击的。Polyspace Server for Ada识别没有运行时错误、已证明失败、不可访问或未验证的代码段。
您可以在服务器类机器上运行Polyspace Server for Ada,并将其集成到构建和持续集成系统中,以便使用Jenkins等工具进行自动验证®.分析结果可以使用Polyspace Client™for Ada进行复查,也可以发布到Polyspace Access™进行分类和解析。
证明没有关键的运行时错误
详细检查每个Ada83或Ada95代码操作的运行时正确性。识别永远不会出现运行时错误的语句,无论运行时条件如何。在事件跟踪、变量值范围和与发现相关的调用树的支持下分析运行时漏洞。Polyspace Server for Ada使用形式化方法来检测逃避其他测试方法的错误。在不执行代码的情况下,分析所有可能输入的所有代码路径。
自动化并集成到DevOps中
通过分析集成代码作为现有DevOps工作流和工具的一部分,支持现代软件开发实践。Polyspace Server for Ada可以使用流行的持续集成工具,如Jenkins和Bamboo®.
静态应用程序安全测试
通过详尽地强调潜在的易受攻击的Ada语句(如内存访问、缓冲区溢出或数值溢出),证明应用程序没有严重的安全漏洞。支持20条CWE弱点规则。利用Polyspace Server为Ada生成的结果来补充或取代模糊测试,转而关注易受攻击的操作。
改进和补充健壮性和功能测试
使用Polyspace Server for Ada可以通过将测试集中在已证明不安全的语句(如除零或溢出)上来改进健壮性测试。使用Polyspace Server for Ada的结果创建和维护边界和分区测试,利用控制和数据流分析,以及计算函数参数和全局变量的范围。