联锁验证工具软件

Interlocking verification tool software

C代码单元测试工具

C code unit test tool

轨道交通系统信息安全检测工具箱

Information security detection toolbox of rail transit system

工控系统安全态势感知

Safety situation awareness of industrial control system

大数据安全运营服务

Big data security operation service

  • 联锁验证工具软件

  • C代码单元测试工具

  • 轨道交通系统信息安全检测工具箱

  • 工控系统安全态势感知

  • 大数据安全运营服务

    联锁验证工具软件

    SmartRocket iVerifier是国内首款iLOCK型计算机联锁系统验证工具，可以自动对所有安全要求进行正式验证，并且在验证不通过的情况下会给出反例，同时反例会呈现到对应的模型图和周期图上供用户推导出性质被违背的完整过程

    联锁的形式化验证

    系统模型的建立

    在通用系统建模的过程中，采用面向对象的方法，设计了道岔、进路、信号 机、轨道电路等基本父类，在其中定义了各种类型设备的基本属性，并且可被子 类继承，在子类中根据设备的具体类型对基本属性进行细化和增加。

    安全属性模型的建立

    模型检验还应该对系统安全属性进行规范性表示，阐明系统必须满足的属性。需要注意的是，形式化验证只能确保系统满足规范表达的安全属性，而安全属性的语义无法验证，所以需要人工保证系统在意义上是正确的。

    产品特色

    国内首款iLock型计算机联锁系统验证工具，针对禁止的不安全状态提供100％验证覆盖率。

    功能自动

    用户只需要点击上传按钮输入所要验证的安全需求文档和待验证的系统设计文档，再点击验证按钮即可根据安全需求一键式自动验证系统设计，验证结果自动分类为验证通过，验证未通过和通过推导成功通过的安全需求三种情况。

    全面覆盖

    该工具的核心功能——验证功能是采用的形式化验证方法，形式化验证方法使用数学证明来确保系统满足要求，每条属性的真伪结论基于严格的数学证明，证明为真的属性任何情况下进行仿真都不会出错，即覆盖率可以达到100%。

    提供反例

    点击选择安全需求验证未通过的每个轨道交通设备，工具不仅会提供该设备的具体每个周期的验证结果（截止到出现反例的周期），还会提供该设备的逻辑关系模型图供用户点击该设备的关联设备以进行追溯。

    高性能

    基于模型检验的形式化验证方法内核，该工具即使针对大型的联锁系统也只需要花费少量时间即可进行完整的安全验证，快速验证即可快速发现系统设计错误并进行改正，实现良性循环，大大缩短了系统设计的周期。

    大容量

    该工具的内核验证功能采用的是基于模型检验的形式化验证方法，模型检验技术已在航空电子，电子设计自动化等行业中得到使用的证明，即可以对超大型系统进行验证，同样我们的工具可以对超大型联锁系统进行验证。

    C代码单元测试工具

    嵌入式智能化测试工具SmartRocket TestGrid支持静态分析，满足根据国军标8114标准对源码进行质量分析；支持C/C++语言的单元测试，采用人工智能算法，利用自动推理与符号执行技术，分析程序路径，产生满足覆盖率的测试用例并在后台自动执行，对于C代码可以自动生成覆盖率高达100%的测试用例。

    特色功能

    简洁高效的用户界面

    表格化管理使结果及覆盖率情况一目了然。用例管理与覆盖率分析位于同一视图，使其用例及代码覆盖情况、控制流程图结构覆盖情况尽收眼底。

    监控分析运行时错误

    通过分析程序语义，自动检测执行过程中的运行时错误，将潜在的程序缺陷及时扼杀在单元测试阶段

    价值优势

    支持语句、分支、MC/DC覆盖准则

    SmartRocket TestGrid能够针对覆盖准则生成测试用例，支持语句、分支、MC/DC及边界覆盖准则，能够自动执行生成的测试用例并提供筛选项，能够满足D0-178B、ISO26262、EN50128等行业标准苛刻的测试要求。

    生成精简的测试用例集

    SmartRocket TestGrid可针对不同的准则生成精简化的用例集，使得用例间没有冗余。其他用例生成工具无覆盖准则之分，通过随机生成或数据字典方式来生成用例往往存在大量冗余。在测试航天某控制软件代码时，SmartRocket TestGrid仅生成 十多个用例就能够达到语句、分支及MC/DC的100%覆盖的函数，而使用的其他软件工具则给出了数百个测试用例，导致 大量用例的冗余。

    全面设计形参、全局变量、桩函数及桩函数形参数据

    SmartRocket TestGrid能针对形参、全局变量、桩函数及桩函数形参等进行全面设计，自动设计桩返回值及参数输出值等。而随机生成或数据字典生成测试用例工具通常只支持形参、全局变量的数据设计，从而导致无法达到较高的覆盖率。

    支持系统函数调用

    在被测代码中，有时我们想要保留系统函数，尤其是memcpy、memset等可能影响覆盖率的内存函数。对随机生成或数据字典生成测试用例的工具而言，该类系统函数无法正确识别，而 SmartRocket TestGrid 能够自动捕获此类函数的内存变化约束，生成正确的测试用例。

    自动执行用例，满足预期值检查规范

    SmartRocket TestGrid生成用例后会自动执行用例，捕获用例的预期值等输出检查信息并自动比对。该检查项满足功能安全认证的要求，检查函数返回值、检查全局变量被修改值、检查形参指针指向内容被修改值等。而其他工具则无此检查项或检查项较为薄弱(例如:只检查函数返回值等)，后续还需要大量的人工来补充该部分数据，从而导致效率降低。

    轨道交通系统信息安全检测工具箱

    轨道交通系统信息安全检测工具箱是一款软硬件结合的一站式轨道交通系统信息安全检测工具平台，主要用于轨道网络生产控制系统的信息安全风险评估和现场工作管理。适用于轨道交通各个子系统，根据相应标准提供综合全面的安全检测，提高检测工作效率，降低检查工作量。

    关键技术优势

    自主研发的软件漏洞检测工具

    利用智能漏洞分析引擎来扫描组件中所含的漏洞与许可证风险。该引擎利用了第三方数据库与开源组件独有的特性和漏洞特性来提升扫描结果的准确率。

    自主研发的工业控制协议模糊检测工具

    工业控制协议模糊测试工具用于测试工业控制网络协议的实现的健壮性，它是采用构造畸形数据包，将畸形数据包发送给被测工控目标，从而测试被测工业控制网络协议的安全性。

    检测类型

    信息项目规划，服务底层架构，智慧集成设计，工业互联物联，农业互联交换、服务业互联物联，中台智慧大脑等多元化智慧信息与数字应用服务。

    渗透测试

    SYNFlood攻击;ARP欺骗攻击;指令重放攻击

    主机安全

    弱口令爆破;业务端口拒绝服务攻击;木马攻击;数据库安全检测;web安全检测

    控制器安全

    弱口令爆破;业务端口拒绝服务攻击;木马攻击

    网络安全

    端口扫描;服务探测

    漏洞扫描

    系统漏洞扫描;软件漏洞扫描

    通讯协议安全

    工控协议安全检测;专用协议安全检测

    工控系统安全态势感知

    近来工业信息安全事件频发，不仅对企业本事造成重大经济损失，在重大关键基础设施行业内，还会对国家安全造成损失。随着工业信息化、工业智能化、工业互联网的发展，工业信息安全的风险与日俱增。

    工控系统安全方案

    平台基于分布式部署、集中管理设计，具备高性能的流量捕捉和大容量的数据存储能力，不仅提供万兆流量下载数据包级的网络实时分析和诊断，还针对工业互联网提供针对性的工控警报规则，实现对关键网络链路流量的长期捕获与保存。

    工控全网颗粒度管控

    提供基于元数据的网络行为配置和丰富行为模型，利用大量的元数据和灵活方便的定义规则准确定义工控网络内外联等异常行为，达到对违规上网、非法外联、违规回传数据等行为的颗粒度管控。

    中心赋能，共享工控全网资源

    通过对接中心平台，可共享安全情报、检测规则、定期更新漏洞库，支持人员远程操作等多种方式，快速提升工控网络各分支安全响应能力，为核心系统及分支系统提供全面防护保障。

    产品优势

    高效的网络行为检测

    集成BDE网络行为检测引擎和SDE网络规则检测引擎，可识别广泛网络应用层协议，辨别文件真实类型。通过协议分析、内容萃取、事件触发、跟踪监控等报告事件，再经深度分析快速鉴别出DDoS攻击、SSH/FTP暴力破解、SQL注入、DNS/ARP污染、漏洞扫描等网络恶意行为。

    独特的威胁变种基因检测

    具有业界独特的基因检测技术，可以利用恶意代码在变种过程中的遗传学特征，即基因在遗传过程中的复制特性及部分基因突变特性，对恶意代码进行检测。通过基因比对，可以很轻易的识别出恶意代码变种，并且检测的时间粒度在毫秒级别。

    敏捷的机器学习

    具备学习功能，利用基因检测情报自动升级病毒特征库，利用未知威胁检测情报自动升级基因图谱库。各检测引擎相互学习、相互补充，机器将不断自我强壮，进一步巩固防御能力。

    先进的未知威胁沙箱检测

    支持各种WEB沙箱、Windows沙箱、Android沙箱、Office沙箱、PDF沙箱等；并基于沙箱技术对各种文件进行内容“引爆”，通过恶意行为模式匹配检测未知威胁，具有高检出率，低误报率，防变种，防逃逸等特点。

    全面的高级持续性威胁检测

    通过内置的防病毒引擎对已知威胁进行静态检测；其次通过基因检测技术对已知威胁的变种进行检测，并结合智能检测技术防止逃逸和躲避（AET）；通过对恶意代码在沙箱中的主机行为和网络行为进行深入分析，对未知威胁进行检测。

    强大的处理性能

    威胁发现与预警监测系统带宽处理能力可达10Gbps；文件处理性能可达10万文件/天；并支持集群技术，集群数量可按需扩展。

    大数据安全运营服务

    安全服务人员的专业技能，从数据安全摸底、数据安全策略的制定及升级、数据安全风险管理以及数据安全优化等方面对数据安全提供全方位安全服务。

    大数据安全应用价值

    网络安全工作的重点与难点之一在于安全规划的落地与实践。

    完善的运营体系建设

    根据用户组织架构、业务特点进行调研、梳理，设计运营岗位、运营流程、运营制度、运营考评机制。充分考虑现有安全组织机构情况、安全建设水平、安全保障能力等安全建设现状，为运营体系设计提供现实支撑保障。标准化的机制、输出物及反馈流程设计，让运营成果可视可见。

    客户单位获得的价值

    高水平的、具有较强防守技术与实操能力的专业安全人员、及安全管理人员，快速建立安全运营团队。 持续的安全建设及安全运营经验交流，获取国内前沿的安全建设及安全运营经验。 持续迭代提高的安运运营水平，做到“真的安全”。

    大数据安全运营中心解决方案

    基于大数据平台架构，分为数据采集层、大数据处理分析层、管控层和综合展现层等；平台具备开放性、可扩展性，能够灵活定制平台功能，并且在日志采集、处理等性能方面能够平滑扩展。

    安全态势的感知平台

    经过多重分析，及时发现异常问题，当风险产生时，多种告警响应方式实时通知。

    安全状况的可视化平台

    基于ISO13335的风险评价，涵盖各类仪表板、统计报表，企业安全状况一目了然。

    安全指挥的应急响应平台

    基于ITIL工单流程、ISO27001的安全管理，当安全事件发生时，及时响应处理，形成完整的闭环操作，工单系统跟踪每一个问题的落实情况。

    安全情报的交换与预警平台

    实现主动的预警，通过企业安全运营中心和各个安全服务供应商共同合作，形成一条完整的预警处理链，可以保证在漏洞出现还未被利用前就送达各个管理员并保证被采取了应对的措施。

    安全工作的承载平台

    使管理者了解系统整体和宏观的安全状况和安全态势；业务人员提升运营质量，提高业务安全运维效率；技术人员了解设备的运营状态、及时处理安全故障，减少运维工作量。

    数据服务平台

    从服务检索、注册、订阅、点评等资产服务旅程的建设，不断提升数据消费者的消费体验，不断提升数据资产的价值。