一种HSM行为模型的约束路径验证方法与流程

摘要: 本发明涉及硬件安全模块的行为架构建模、软件验证和图约束分析领域,具体涉及将hsm行为模型中的模块、安全域和受控接口表示为有向架构图,并依据必经网关、禁止节点和返...
一种HSM行为模型的约束路径验证方法与流程

本发明涉及硬件安全模块的行为架构建模、软件验证和图约束分析领域,具体涉及将hsm行为模型中的模块、安全域和受控接口表示为有向架构图,并依据必经网关、禁止节点和返回出口约束验证数据路径的方法。本发明用于对可执行行为参考模型、设计阶段架构描述或接口配置进行一致性验证,不直接声称在物理芯片中形成电气隔离、抗侧信道隔离或经认证的安全边界。

背景技术:

1、hsm设计通常将外部请求适配、主体权限判断、生命周期控制、秘密状态处理、事件错误处理和响应输出分配给不同模块。为了便于设计评审,模块及其接口可以被记录为架构描述或行为参考模型。仅检查模块名称是否重复、接口端点是否存在以及控制条件是否为空,只能发现格式错误,不能证明从外部入口至受保护目标的每一条可达路径均经过指定安全网关。

2、在模块数量增加或接口复用后,新增的一条边可能绕过权限门或命令门而直接到达受保护状态节点。即使设计者预期正常路径经过网关,只要架构图中存在另一条可达旁路,单纯列举预期路径仍不能暴露该旁路。另一方面,目标节点处理结果可能必须经事件错误控制和响应适配模块返回;若只验证正向到达而不验证受控返回,异常结果可能缺少统一出口。

3、常规图可达性算法能够判断目标是否可达,但无法直接表达“必须按给定顺序经过多个网关”这一条件。若仅把网关节点从图中删除后再检查可达性,也难以同时处理多个网关顺序、数据类别限制和禁止节点,并且难以输出可复核的最小旁路路径。

4、此外,行为模型频繁迭代时,每次均对全部入口、目标和规则执行完整遍历会产生重复计算。若验证结果未与具体模型版本绑定,历史通过结果还可能被错误地复用于已经修改的架构。

5、因此,需要一种将必经网关进度纳入遍历状态、能够输出确定性最小违规路径并支持按依赖关系增量重验的约束路径验证方案。

技术实现思路

1、本发明要解决的技术问题如下:

2、如何验证外部入口到受保护目标的所有有效路径均按顺序经过指定网关,而不是仅验证一条预设正常路径;如何同时识别正向旁路和受控返回路径缺失,并给出可复核、可稳定重现的违规路径。

3、如何使验证结果与架构版本绑定,并在模块或接口发生局部变更时只重新计算受影响规则,避免旧结果误用和无差别全量遍历。

4、为解决上述技术问题,本发明采用如下技术方案:

5、把模块定义转换为节点,把受控接口转换为有向边,并在边上保存数据类别、主体类别、访问方向、启用条件和安全域转换信息。每条安全域路径规则明确入口节点集合、受保护目标集合、有序必经网关序列、禁止节点集合和允许返回出口集合。

6、执行约束遍历时,单个访问状态不是仅由节点标识构成,而是由当前节点与必经网关进度联合构成。遍历到下一必经网关时推进进度;未满足数据类别、主体类别、启用条件或禁止节点约束的边不被扩展。以该方式可以区分“到达同一节点但已经经过不同网关阶段”的不同状态。

7、当目标节点在必经网关进度未完成时可达,生成旁路违规;当目标节点虽被合规到达但不存在按规定网关顺序返回允许出口的路径时,生成返回路径缺失违规。利用父状态指针回溯节点和边,并采用广度优先和字典序规则选出确定性的最小违规路径。

8、对规范化后的模型定义计算版本指纹,并建立模块或边到路径规则的依赖索引。模型变化时,利用变更项查询依赖索引,仅使对应规则的缓存结果失效并重新验证。

9、与仅采用常规并列处理或单一状态比较的方案相比,本发明至少具有如下技术效果:

10、把网关顺序作为可计算状态参与遍历,可发现“目标可达但网关约束未满足”的旁路,而不是把目标可达误判为合规。

11、最小违规路径同时携带缺失网关、违规边和模型指纹,便于设计人员定位新增接口或错误域转换,不依赖不稳定的日志顺序。

12、正向路径与返回路径分别验证,可使受保护操作和事件错误返回均具有可核验的受控通路。

13、依赖索引和版本指纹使局部修改的验证范围明确,并防止将旧架构的通过结果应用到新架构。

14、“hsm行为模型”是描述模块职责、状态处理和接口关系的软件模型或架构数据,不等同于真实芯片的物理结构。“受保护目标节点”是规则中要求经指定网关方可到达的模型节点。

15、“必经网关进度”表示有序网关序列已完成的前缀长度。例如网关序列为g1、g2时,到达g2但未先到达g1不推进进度;随后到达目标仍构成旁路。

16、“最小违规路径”优先指边数最少的违规路径;当边数相同,采用固定标识排序获得唯一结果。该定义用于结果稳定复现,不表示该路径在真实系统中发生概率最高。

17、“增量重验”仅复用模型指纹一致且未被依赖变更影响的规则结果。若规范化算法、规则版本或接口解释方式变化,应使相关缓存全部失效。

1.一种hsm行为模型的约束路径验证方法,其特征在于,由处理器执行,包括:根据hsm行为模型中的模块定义、模块所属安全域以及模块之间的受控接口定义构建有向架构图,所述有向架构图中的节点对应模块,边对应携带数据类别、访问方向、启用条件和域转换标记的受控接口;读取至少一条安全域路径规则,每条安全域路径规则包括入口节点集合、受保护目标节点集合、按顺序经过的必经网关集合、禁止到达节点集合以及允许返回出口集合;针对每一入口节点与受保护目标节点组合执行带约束可达性遍历,在遍历状态中联合记录当前节点和已按顺序经过的必经网关进度,仅扩展启用条件满足且未到达禁止节点的边;当遍历到受保护目标节点而必经网关进度未完成时,把对应路径确定为旁路路径,当无法从所述受保护目标节点经允许返回路径到达允许返回出口时,把对应路径确定为返回路径缺失;按照预设的边排序规则和路径长度生成至少一条确定性的最小违规路径,并在违规记录中关联入口节点、目标节点、缺失网关、违规边和模型版本指纹;根据模块定义和受控接口定义计算所述模型版本指纹,并建立模块或边到安全域路径规则的依赖索引;在模型定义发生变化时,根据所述依赖索引仅重新验证受影响的安全域路径规则;以及仅在不存在旁路路径、返回路径缺失和配置完整性错误时输出所述hsm行为模型通过约束路径验证的结果。

2.根据权利要求1所述的方法,其特征在于,所述必经网关集合为有序网关序列,所述必经网关进度由整数或位掩码表示;仅当当前扩展边的目的节点等于下一必经网关时推进所述必经网关进度,且在网关顺序不满足时不把已访问该网关视为完成约束。

3.根据权利要求1所述的方法,其特征在于,所述受控接口定义还包括数据类别集合和主体类别集合;当边传输的数据类别或主体类别不属于对应安全域路径规则允许的类别时,将该边作为禁止扩展边,并在违规记录中写入不匹配的数据类别或主体类别。

4.根据权利要求1所述的方法,其特征在于,所述最小违规路径通过广度优先遍历生成,在路径长度相同时按照源节点标识、目的节点标识和接口标识的字典序确定唯一输出路径,并通过父状态指针回溯得到从入口节点至目标节点的完整节点序列和边序列。

5.根据权利要求1所述的方法,其特征在于,所述允许返回路径要求从受保护目标节点出发依次经过事件错误控制网关和外部响应适配网关后到达允许返回出口;未按所述顺序到达允许返回出口的路径不被认定为有效返回路径。

6.根据权利要求1所述的方法,其特征在于,所述模型版本指纹由规范化排序后的模块标识、模块安全域、接口标识、接口端点、数据类别、访问方向和启用条件的摘要值组合生成;当指纹变化时,依据发生变化的模块或边查询所述依赖索引,并保留未受影响规则的上一次验证结果。

7.根据权利要求1所述的方法,其特征在于,在执行带约束可达性遍历之前还执行配置完整性校验,所述配置完整性校验至少包括节点标识唯一、边的源节点和目的节点存在、每条安全域路径规则至少具有一个入口节点和一个目标节点、必经网关存在以及允许返回出口存在;所述配置完整性错误与所述最小违规路径采用不同的错误类别记录。

8.一种hsm行为模型的约束路径验证系统,其特征在于,包括架构图构建模块、路径规则读取模块、带约束可达性遍历模块、最小违规路径生成模块、模型版本指纹模块、依赖索引模块和结果输出模块;所述各模块被配置为执行权利要求1至7任一项所述的方法。

9.一种电子设备,包括处理器和存储器,所述存储器中存储有计算机程序,其特征在于,所述计算机程序被所述处理器执行时,使所述处理器执行权利要求1至7任一项所述的方法。

10.一种计算机可读存储介质,其上存储有计算机程序,其特征在于,所述计算机程序被处理器执行时实现权利要求1至7任一项所述的方法。