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