-
公开(公告)号：CN114741278B
公开(公告)日：2024-10-22
申请号：CN202210283082.X
申请日：2022-03-22
Applicant: 华东师范大学
IPC: G06F11/36
Abstract: 本申请提供了一种机载软件中目标代码到源代码的验证分析系统，具体的，第一代码模块根据第一目标代码通过反汇编得到第一汇编代码，根据第一汇编代码进行反编译得到第一C代码；关系映射模块将第一C代码与源代码进行对比，得到源代码变量名之间的对应关系；根据对应关系，结合第一汇编代码，得到源代码变量名与汇编代码的指令中逻辑地址的关系映射表；第二代码模块根据第二目标代码通过反汇编得到第二汇编代码；根据关系映射表对汇编代码进行反编译，得到第二C代码；第一验证分析模块将第二C代码与源代码进行对比，得到第一验证结果。本申请解决了IDA Pro不能对COFF格式文件进行反编译的缺陷，提供了新的可执行目标代码到源代码可追溯性验证思路。
-
公开(公告)号：CN114741123A
公开(公告)日：2022-07-12
申请号：CN202210129476.X
申请日：2022-02-11
Applicant: 华东师范大学
Abstract: 本发明公开了一种机载软件形式化验证系统，系统包括：需求验证结果生成模块、源代码验证结果生成模块、目标代码验证结果生成模块、验证通过模块。因此，采用本申请实施例，由于本申请将机载软件的验证活动分为需求与设计、源代码和可执行目标代码三个阶段，并针对每个阶段的验证活动，结合DO‑333中定义的验证目标，提出了形式化分析与验证的方法论进行验证，从而提升了机载软件的安全性。
-
公开(公告)号：CN114721734A
公开(公告)日：2022-07-08
申请号：CN202210130444.1
申请日：2022-02-11
Applicant: 华东师范大学
IPC: G06F9/445
Abstract: 本发明公开了一种机载软件形式化验证方法，方法包括：对机载软件的需求与设计阶段进行验证，生成初始验证结果；对机载软件的源代码阶段进行验证，生成源代码验证结果；对机载软件的可执行目标代码阶段进行验证，生成目标代码验证结果；当初始验证结果、源代码验证结果以及目标代码验证结果全部符合预设数值时，确定机载软件验证通过。因此，采用本申请实施例，由于本申请将机载软件的验证活动分为需求与设计、源代码和可执行目标代码三个阶段，并针对每个阶段的验证活动，结合DO‑333中定义的验证目标，提出了形式化分析与验证的方法论进行验证，从而提升了机载软件的安全性。
-
公开(公告)号：CN111240972A
公开(公告)日：2020-06-05
申请号：CN202010011072.1
申请日：2020-01-06
Applicant: 华东师范大学 , 上海丰蕾信息科技有限公司
Abstract: 本发明公开了一种基于源代码的模型验证装置，所述装置包括：源代码获取模块，用于获取目标源代码；第一模型生成模块，用于根据AADL建模技术将所述目标源代码进行建模后生成AADL模型；第二模型生成模块，用于基于预设转换方式将所述AADL模型转换生成时间自动机模型；模型检查模块，用于利用预设模型检测器对所述时间自动机模型进行检查。因此，采用本申请实施例，可以提高验证效率。
-
公开(公告)号：CN110532778A
公开(公告)日：2019-12-03
申请号：CN201910625643.8
申请日：2019-07-11
Applicant: 华东师范大学 , 上海丰蕾信息科技有限公司
Abstract: 本发明涉及工业控制系统、深度对抗学习、模糊测试领域，特别涉及一种基于生成对抗网络的工控协议漏洞挖掘系统。包括：深度对抗学习模块，生成模糊测试数据；攻击测试模块，把深度对抗学习模块生成的模糊测试数据注入到系统中，并记录系统的异常反馈，挖掘该系统的漏洞。本发明通过将模糊测试技术与深度对抗学习技术相结合，实现高效，自主的学习通讯数据的格式，并生成带有变异的模糊测试数据，这种技术将极大减轻漏洞挖掘中人的负担，做到高效且智能。
-
Patent Agency Ranking
公开(公告)号：CN106096789A
公开(公告)日：2016-11-09
申请号：CN201610456945.3
申请日：2016-06-22
Applicant: 华东师范大学
CPC classification number: G06Q10/04 , G06Q10/0635 , G08B21/00
Abstract: 本发明公开了一种基于机器学习技术的可自感知异常的工控安全防护与报警系统，其包括数据采集和预处理模块、数据存储单元、异常检测单元、操作单元，其中数据存储单元包括本地存储模块和网络存储模块，异常检测单元包括预测模块、分析模块、判断模块和决策模块，操作单元包括报警模块和保护模块；该系统配置在需要监控的工控系统中，采集工控系统之间信号发送的数据并进行预处理后，对所述数据基于机器学习框架的异常性进行检测，当有异常于常规操作的情况发生时，自动发出报警或是产生相关的拒绝指令。
-
公开(公告)号：CN108469987B
公开(公告)日：2020-12-29
申请号：CN201810160216.2
申请日：2018-02-26
Applicant: 华东师范大学 , 上海华元创信软件有限公司
IPC: G06F9/48
Abstract: 一种基于中断控制流图的中断验证系统，包括：代码转换模块，用于根据中断驱动程序获取汇编代码；中断信息统计模块，根据所述汇编代码统计中断信息；控制流图生成模块，根据所述汇编代码生成控制流图；中断控制流图生成模块，根据所述控制流图与所述中断信息生成中断控制流图；处理模块，用于对所述中断控制流图切片处理；分析模块，根据所述中断控制流图切片，验证所述中断驱动程序的时间安全与内存安全。本发明提出了一个新的用以表示中断驱动程序控制流结构的模型—中断控制流图，并给出削减中断控制流图规模(切片)的方法，实现了在同一模型中验证中断驱动程序最常出现的两类问题，提高了中断驱动程序验证的可靠性与安全性。
-
-
公开(公告)号：CN110417755A
公开(公告)日：2019-11-05
申请号：CN201910626439.8
申请日：2019-07-11
Applicant: 华东师范大学 , 上海丰蕾信息科技有限公司
Abstract: 本发明涉及工业控制系统、深度对抗学习、模糊测试领域，特别涉及一种基于生成对抗网络的工控协议漏洞挖掘方法。包括：深度对抗学习，生成模糊测试数据；攻击测试，把深度对抗学习生成的模糊测试数据注入到系统中，并记录系统的异常反馈，挖掘该系统的漏洞。本发明通过将模糊测试技术与深度对抗学习技术相结合，实现高效，自主的学习通讯数据的格式，并生成带有变异的模糊测试数据，这种技术将极大减轻漏洞挖掘中人的负担，做到高效且智能。
-
公开(公告)号：CN106940659A
公开(公告)日：2017-07-11
申请号：CN201710139115.2
申请日：2017-03-09
Applicant: 华东师范大学 , 上海丰蕾信息科技有限公司
IPC: G06F9/48
CPC classification number: G06F9/4831
Abstract: 本发明公开了一种基于加权下推系统的中断验证方法，首先根据程序目标代码中指令的跳转关系将其建模成加权下推系统，然后通过加权下推系统的可达性算法，得出所有的可达格局；最后遍历所得的可达格局，判断当前格局信息是否满足需求，如果不满足，则判断错误类型，返回错误路径，若遍历完所有可达格局没有发现错误，则返回正确。本发明的方法可以：将实时系统的中断验证与加权下推系统相结合，以形式化的方式对实时系统中断进行验证，提高了验证的可靠性和鲁棒性；同一个模型下同时验证有关中断的时序逻辑、优先级反转、内存访问冲突以及超时问题，具有高效性，同时也节约了成本。
-
-
-
-
-
-
-
-
-
Search Results
41
records
(took 0.03 seconds)
