-
公开(公告)号：CN110705316B
公开(公告)日：2023-03-24
申请号：CN201910935932.8
申请日：2019-09-29
Applicant: 南京大学
IPC: G06F40/42
Abstract: 本发明公开了一种智能家居线性时序逻辑规约生成的方法和装置，用于在智能家居领域中将用户输入的自然语言需求文本转换成线性时序逻辑规约。该方法首先对输入的自然语言文本进行预处理；然后使用自然语言处理技术，生成语法分析树和语法依存关系；识别句子中的各个子句，以及每个子句中的主语、谓语、宾语、布尔运算符、条件变量和时序运算符，生成树形的中间表示形式；最后遍历树结构，自动生成对应的线性时序逻辑规约。本发明解决了普通智能家居用户难以直接提供形式化规约的问题，有效节约时间和人力成本，并且能够弥补现有智能家居物联网验证系统的不足，使得不具备专业知识的普通用户所提出的自然语言需求能够被自动的验证。
-
公开(公告)号：CN111461261A
公开(公告)日：2020-07-28
申请号：CN202010417999.5
申请日：2020-05-18
Applicant: 南京大学
Abstract: 本发明公开了神经网络分类识别中的对抗样本生成的方法和装置。本发明架构了一种对抗样本自动化生产的平台，在这平台中，用户可按照特定样本的应用场景构建出相应的合成函数、不满足度评估函数、噪音空间收缩策略函数组成特定的搜索策略，然后通过本发明的平台自动生成对抗样本，由此固化对抗样本生成的算法，对某种特定样本生成对抗样本效率低的情形时，用户仅需要改变其中的搜索策略即可改进对抗样本的生成效率。
-
公开(公告)号：CN108763064B
公开(公告)日：2020-07-07
申请号：CN201810442423.7
申请日：2018-05-10
Applicant: 南京大学
IPC: G06F11/36
Abstract: 本发明公开了一种基于黑盒函数与机器学习的代码测试生成方法和装置。本发明通过对被测程序代码静态分析，提取先前测试未覆盖的节点所对应的未覆盖路径，然后将未覆盖路径上的复杂结构的程序代码用黑盒函数打包后，采用基于学习验证的约束求解器和符号执行分析器进行验证求解，得到能够覆盖先前测试未覆盖的节点的测试用例数据，从而使得测试工程师能够利用这些测试用例数据进行回归测试从而测试覆盖先前测试未覆盖的节点。本发明将被测程序中的复杂代码替换成黑盒函数，减少了符号执行过程中对复杂代码片段的分析，将更多系统资源分配在对目标结点覆盖的求解上，从而提高了程序分析效率和目标节点的覆盖率。
-
公开(公告)号：CN107180193B
公开(公告)日：2020-03-27
申请号：CN201710480725.9
申请日：2017-06-22
Applicant: 南京大学
IPC: G06F21/56
Abstract: 本发明公开了一种将程序代码转换成数据约束的方法和装置。该方法首先将程序代码转换成中间指令集，然后将中间指令集进行细化拆分，细化拆分时将原变量定义指令中涉及的复杂类型的变量细化拆分成多个简单类型的变量，然后将简单类型的变量再进一步细化成简单类型的地址指针变量和简单类型的指针指向变量，最后再将相应的变量定义指令细化拆分成针对简单类型的地址指针变量和简单类型的指针指向变量的内存分配指令和初始化数据存储指令，然后提取细化拆分后的中间指令集中的存取指令、算术指令和比较指令作为数据约束。
-
公开(公告)号：CN106055318A
公开(公告)日：2016-10-26
申请号：CN201610343482.X
申请日：2016-05-23
Applicant: 南京大学
Abstract: 本发明公开了一种智能家居物联网系统验证与修复的方法和装置。本发明通过智能家居设备描述信息和IFTTT规则构建混成自动机模型，然后通过对混成自动机模型的路径分析，找出可能到达系统不安全的路径，然后将这些可达路径编码成SMT约束进行求解，如果存在可达路径对应的SMT约束可解，则根据可解的SMT约束对IFTTT规则This部分中实数型条件值进行修正。修正的方法是通过将可解的SMT约束中的对应的IFTTT规则This部分中实数型条件值参数化后并将整个SMT约束取反，然后消去量词后进行求解，将可解值替换This部分中实数型条件值。
-
Patent Agency Ranking
公开(公告)号：CN103400025B
公开(公告)日：2016-01-20
申请号：CN201310280740.0
申请日：2013-07-04
Applicant: 南京大学
IPC: G06F19/00
Abstract: 本发明提出一种混成系统的可达性分析方法，包括以下步骤：解析混成自动机输入文件，将该自动机的有界图结构编码成一组命题逻辑公式集合；利用SAT求解器对该公式集合进行求解，若不可解则输出结果不可解，如果可解则将可满足赋值解码成输入自动机图结构上的一条路径；根据混成自动机的语义对目标路径进行编码形成线性约束；对该线性约束求解，如果可解则输出该路径作为结果，否则转下一步；给出线性约束的不可约不可解集合；将不可达路径编码成一组命题逻辑公式集合并加到自动机图结构的公式集合里。采用本发明方法可快速找出到达目标节点的候选路径，减少对混成自动机图结构进行搜索的时间。
-
公开(公告)号：CN103220179A
公开(公告)日：2013-07-24
申请号：CN201310148619.2
申请日：2013-04-25
Applicant: 南京大学
IPC: H04L12/24
Abstract: 本发明提供一种网络系统的鲁棒性的评测系统及其工作方法。评测系统首先构造网络系统协议的时间自动机，描述协议的整体工作流程。然后，在模型中引入加权迁移对该时间自动机进行扩展，构建系统的随机时间自动机，以对环境中的不确定因素建模。基于该随机时间自动机，可以使用统计模型检验技术对系统的性能进行分析与评估，以在协议设计和选择阶段，实现参数配置、性能比较等目标。本方法主要是通过对不稳定网络系统中协议及环境的建模，分析与评估网络系统在特定环境下的性能，以此评测该网络系统的鲁棒性。统计模型检验技术基于仿真及统计的方法避免了对系统状态的穷尽搜索，在时间和空间上的消耗大大降低，能够用于处理大规模系统。
-
公开(公告)号：CN116389122A
公开(公告)日：2023-07-04
申请号：CN202310371707.2
申请日：2023-04-10
Applicant: 南京大学
IPC: H04L9/40
Abstract: 本发明公开了一种基于异常状态的攻击检测方法、装置、介质及机器。本发明的攻击检测方法如下：首先从网上抓取攻击缺陷描述文本，然后对攻击缺陷描述文本进行解析后得到攻击状态迁移信息的集合，监测机器执行操作系统和应用程序的行为时，并根据行为结果是否与状态迁移信息集合中的攻击状态信息一致判断机器是否出现异常状态，当出现异常状态时发出异常状态的预警。本发明通过监测攻击状态之间的迁移判断是否存在攻击的判断准确度很高，基本不会产生误报问题。此外，本发明可以实时跟踪和下载当前的攻击行为、攻击手段以及所利用的软件漏洞会缺陷，使得机器攻击模型图样本保持最新，从而能够使得机器能够及时应对新的攻击手段。
-
公开(公告)号：CN111444112A
公开(公告)日：2020-07-24
申请号：CN202010344638.2
申请日：2020-04-27
Applicant: 南京大学
Abstract: 本发明公开了一种基于共享不可行路径池的代码并行验证方法和装置。该方法分为初始化过程、找出潜在路径过程和对潜在路径分析过程。在初始化过程中，输入的源程序和验证目标被构建成相应的SAT约束编码G。然后通过对不可行路径池中路径和SAT约束编码G的SAT求解，得到其SAT解对应的路径作为潜在路径存入并行任务池。再以多线程并行方式对并行任务池各个潜在路径进行SMT求解，若SMT无解，则抽取不可满足的最小集合X对应的不可行程序路径片段加入至不可行路径池。由此通过迭代，最终得到验证目标是否可达。为提高验证效率，本发明还增加了对不可行路径剪枝步骤。相比于现有技术，本发明大大提高代码验证效率。
-
公开(公告)号：CN106055318B
公开(公告)日：2019-04-12
申请号：CN201610343482.X
申请日：2016-05-23
Applicant: 南京大学
Abstract: 本发明公开了一种智能家居物联网系统验证与修复的方法和装置。本发明通过智能家居设备描述信息和IFTTT规则构建混成自动机模型，然后通过对混成自动机模型的路径分析，找出可能到达系统不安全的路径，然后将这些可达路径编码成SMT约束进行求解，如果存在可达路径对应的SMT约束可解，则根据可解的SMT约束对IFTTT规则This部分中实数型条件值进行修正。修正的方法是通过将可解的SMT约束中的对应的IFTTT规则This部分中实数型条件值参数化后并将整个SMT约束取反，然后消去量词后进行求解，将可解值替换This部分中实数型条件值。
-
-
-
-
-
-
-
-
-
Search Results
47
records
(took 0.02 seconds)
