公开(公告)号：CN116107862A

公开(公告)日：2023-05-12

申请号：CN202210974710.9

申请日：2022-08-15

Applicant: 西安电子科技大学

Inventor： 于斌 ,  董彦松 ,  田聪 ,  段振华 ,  王小兵 ,  陆旭 ,  张南 ,  赵亮

IPC: G06F11/36

Abstract: 本发明公开了一种面向完全正则时序逻辑性质的高效运行时监控方法，包括：采用MSVL语言编写待监控程序，得到MSVL程序；采用PPTL公式形式化描述待验证的时序逻辑性质；针对PPTL公式中涉及的与MSVL程序有关的程序变量，对MSVL程序进行插桩；根据MSVL程序在动态执行过程中生成的状态序列，检测MSVL程序的实时运行状态，并根据检测结果判断MSVL程序的运行状态是否满足待验证的时序逻辑性质。本发明提供的利用分布式架构的运行时监控方法可用于对MSVL程序的完全正则时序逻辑性质的正确性检测，使得MSVL程序的动态执行状态能够得到及时检测，有效地保障了MSVL程序的可靠性和安全性。

公开(公告)号：CN116861433A

公开(公告)日：2023-10-10

申请号：CN202310594839.1

申请日：2023-05-24

Applicant: 西安电子科技大学

Inventor： 张诗雯 ,  谷卓亚 ,  于斌 ,  李昱霖 ,  刘屹 ,  张钰涵 ,  陆旭 ,  田聪

IPC: G06F21/57 ,  G06F21/64 ,  G06F21/53 ,  G06F21/62 ,  G06F21/56 ,  G06Q40/04 ,  G06F8/41

Abstract: 本发明公开了一种基于No GIL并行的以太坊智能合约交易缺陷检测方法及装置，本发明所提供的一种基于No GIL并行的以太坊智能合约交易缺陷检测方法中：利用以太坊虚拟机重放交易，收集交易过程中字节码级别的跟踪数据；根据跟踪数据间的依赖关系划分跟踪数据，以模拟EVM堆栈构建交易处理图；基于No GIL对交易处理图进行处理，构造中间表示信息，得到数据文件；利用预设检测规则对数据文件进行检测，进而检测交易过程中是否存在被攻击的隐患。由于本发明实施例使用基于No GIL的并行方法对字节码进行解析，因此原本最容易超时的交易处理图构建和转换部分的效率极大提高，缩短了攻击检测的时间。

公开(公告)号：CN113238759A

公开(公告)日：2021-08-10

申请号：CN202110399134.5

申请日：2021-04-14

Applicant: 西安电子科技大学

Inventor： 段振华 ,  谷宇天 ,  张南 ,  田聪 ,  王小兵 ,  赵亮 ,  陆旭 ,  于斌 ,  张捷

IPC: G06F8/41 ,  G06F8/76

Abstract: 本发明属于计算机程序设计语言及应用技术领域，公开了一种类Python程序设计语言XD‑M的解释系统及方法，所述类Python程序设计语言XD‑M的解释方法包括：对于XD‑M语言中的基本语句和源自建模仿真验证语言MSVL的语句，通过调用MSVL解释器底层接口的方法进行解释；对于具有XD‑M语言特性的语句，为语句建立等价的MSVL语法树，扩展底层接口，编写底层对该语句的解释方法。本发明使用XD‑M语言编写的XD‑M程序可以进行建模、仿真和验证，提高了XD‑M语言的正确性、可靠性和安全性，实现类Python的使用简单变量而无需类型声明的编程风格，提高XD‑M程序的灵活性；依托MinGW开发环境。

公开(公告)号：CN117312137A

公开(公告)日：2023-12-29

申请号：CN202311154956.2

申请日：2023-09-07

Applicant: 西安电子科技大学

Inventor： 于斌 ,  刘元哲 ,  邢恒睿 ,  王宇兴 ,  林滕劼 ,  李鸿 ,  杨铠铭 ,  陆旭 ,  田聪 ,  王小兵 ,  赵亮

IPC: G06F11/36 ,  G06F9/48

Abstract: 本发明公开了一种面向中断驱动程序的原子性违反缺陷检测方法及装置，该方法包括：确定中断驱动程序对应的所有节点中的中断节点，以及每个中断节点对应的中断驱动程序中的会受影响的中断服务例程；根据中断驱动程序生成可达树，得到所有节点中各个节点的原始状态；根据可达树的路径走向确定待处理的中断节点，针对每个待处理的中断节点的原始状态对应的程序语句对中断驱动程序中的共享变量的访问情况、以及会受影响的中断服务例程对共享变量的访问情况，确定原始状态是否存在对应的中断触发状态，并当存在时，生成中断触发状态的后继状态流，并记录对每个共享变量的访问信息，根据记录的访问信息和不可序列化的交织模式，检测原子性违反缺陷。

公开(公告)号：CN117094263A

公开(公告)日：2023-11-21

申请号：CN202210520515.9

申请日：2022-05-13

Applicant: 西安电子科技大学

Inventor： 田聪 ,  刘廷 ,  于斌 ,  段振华 ,  曲南江 ,  张学士 ,  王小兵 ,  张南 ,  陆旭

IPC: G06F30/347

Abstract: 本发明涉及一种基于商用Xilinx Virtex‑7FPGA芯片资源模型的解析绘制方法，包括：通过解析.xml格式的Virtex‑7FPGA架构体系文件，获取Virtex‑7FPGA芯片属性信息存储至第一结构体中；通过解析.net格式的网表电路文件，获取网表电路文件的资源信息存储在集群网表类中；通过解析.place格式的电路布局文件，获取电路布局文件的资源信息存储至第二结构体中；根据第一结构体、集群网表类、第二结构体绘制Virtex‑7FPGA芯片架构、电路的可布局块分布以及网络连接；通过解析.route格式的电路布线文件，获取电路布线文件的资源信息，并存储轨迹向量中；根据集群网表类、电路布线文件的资源信息和预设布线资源图，绘制电路的布线连接和关键布线路径时延。本发明整体运行效率较为高效且消耗资源较低。

公开(公告)号：CN113626813A

公开(公告)日：2021-11-09

申请号：CN202110876832.X

申请日：2021-07-31

Applicant: 西安电子科技大学

Inventor： 于斌 ,  陆旭 ,  田聪 ,  段振华 ,  张南 ,  曲南江

IPC: G06F21/56 ,  G06F11/36

Abstract: 本发明属于程序运行验证技术领域，公开了一种基于运行时验证的边缘服务器DoS攻击检测方法，所述基于运行时验证的边缘服务器DoS攻击检测方法包括：采用PPTL公式形式化描述边缘服务器预期行为；采用PPTL公式形式化描述边缘服务器DoS攻击特征；针对PPTL公式中涉及的程序变量与程序函数，对边缘服务器运行程序进行插桩；针对边缘服务器程序的动态执行轨迹，采用并行运行时验证框架检测程序运行状态，根据检测结果判断边缘服务器是否正在被DoS攻击。本发明提供的基于并行运行时验证框架能够充分利用边缘服务器的空闲计算与存储资源，提高验证效率，及时发现攻击，还能够使得程序执行的每一个状态均能够得到可靠的验证，有效保障了边缘服务器安全性。