买专利卖专利找龙图腾，真高效！ 查专利查商标用IPTOP,全免费！专利年费监控用IP管家,真方便！

龙图腾网获悉浙江大学;杭州优稳自动化系统有限公司申请的专利并发系统信息流安全精化关系的验证方法及装置获国家发明授权专利权，本发明授权专利权由国家知识产权局授予，授权公告号为：CN120763932B 。

龙图腾网通过国家知识产权局官网在2026-05-12发布的发明授权授权公告中获悉：该发明授权的专利申请号/专利号为：202510625765.2，技术领域涉及：G06F21/57；该发明授权并发系统信息流安全精化关系的验证方法及装置是由王文海;孙欢;王竟亦;徐斌;王秋婷;李昕怡;张稳稳设计研发完成，并于2025-05-15向国家知识产权局提交的专利申请。

本并发系统信息流安全精化关系的验证方法及装置在说明书摘要公布了：本发明公开了一种并发系统信息流安全精化关系的验证方法及装置。本方法涉及计算机安全领域，特别是并发系统的信息流安全精化关系验证。针对传统精化技术无法保障信息流安全性的技术缺陷，该方法将设计层面和实现层面的并发系统抽象为并发事件系统，再证明设计层面和实现层面并发事件系统满足安全保留模拟关系。证明安全保留模拟关系保证如果设计层面并发系统满足安全规约，则实现层面并发系统也满足安全规约。此外，本发明提供通用编程语言接口，使得方法适用于不同的编程语言。本发明利用形式化验证和机器证明技术，严格地验证了并发系统信息流安全精化关系，可以用于证明大规模并发系统的信息安全，防患于未然。

本发明授权并发系统信息流安全精化关系的验证方法及装置在权利要求书中公布了：1.一种并发系统信息流安全精化关系的验证方法，其特征在于，包括： 将设计层面和实现层面的并发系统分别建模为并发事件系统，所述并发事件系统包含多个并行执行的事件系统，每一个事件系统包含多个可能执行的事件，每个事件由一种编程语言进行建模；所述事件系统执行某个事件时，事件执行的过程可被其他事件系统打断； 根据所述并发事件系统，分别设计设计层面和实现层面信息流安全规约，所述信息流安全规约包括：操作域集合、可流向关系、事件域函数和观察函数，分别表示执行事件的操作域、操作域信息流的流向关系、将事件到相应操作域的映射关系以及在某个状态下操作域能够观察到的变量集合； 根据所述信息流安全规约，设计安全保留模拟关系以及每个事件系统的依赖、保证关系，所述安全保留模拟关系包括设计层面和实现层面的状态模拟关系和动作模拟关系；所述依赖、保证关系包括设计层面的依赖、保证关系和实现层面的依赖、保证关系； 根据所述安全保留模拟关系和依赖、保证条件，证明设计层面和实现层面的精化关系，并验证设计层面的并发事件系统满足安全规约，从而证明实现层面同样满足安全规约； 其中，所述状态模拟关系需要与观察函数相匹配，即如果和是设计层面的两个状态，和是实现层面的两个状态，和以及和分别满足状态模拟关系，如果状态和下操作域能观察到的变量集合相同，那么状态和下操作域能观察到的变量集合也相同； 所述动作模拟关系需要满足任意实现层面的动作被映射到静步或映射到设计层面的某一特定动作；如果实现层面的动作被映射到设计层面的动作，则两者的操作域需要相同； 所述依赖条件需要包含所有其他事件系统可能造成的状态变化，所述保证条件需要包含所有被验证事件系统可能造成的状态变化； 所述精化关系需要满足设计层面和实现层面的初始状态满足状态模拟关系，如果实现层面的某一个动作被动作模拟关系映射到静步，则实现层面执行该动作后的状态和设计层面状态仍满足状态模拟关系，并且执该动作造成的状态变化包含爱执行该动作的事件系统的保证条件中；如果实现层面的某一动作被动作模拟关系映射到设计层面的某一动作，则实现层面和设计层面分别执行相应动作后的状态仍满足模拟关系，并且设计层面和实现层面执行该动作造成的状态变化包含在执行该动作的事件系统的保证条件中；任何依赖条件包含的状态变化仍然满足状态模拟关系且不同事件系统的依赖、保证条件相容。

如需购买、转让、实施、许可或投资类似专利技术，可联系本专利的申请人或专利权人浙江大学;杭州优稳自动化系统有限公司，其通讯地址为：310058 浙江省杭州市西湖区余杭塘路866号；或者联系龙图腾网官方客服，联系龙图腾网可拨打电话0551-65771310或微信搜索“龙图腾网”。

以上内容由龙图腾AI智能生成。