摘要:

摘要:计算机系统被应用于各种重要领域,这些系统的失效可能会带来重大灾难.不同应用领域的系统对于可信性具有不同的要求,如何建立高质量的可信计算机系统,是这些领域共同面临的巨大挑战.近年来,具有严格数学基础的形式化方法已经被公认为开发高可靠软硬件系统的有效方法.目标是对形式化方法在不同系统的应用进行不同维度的分类,以更好地支撑可信软硬件系统的设计.首先从系统的特征出发,考虑6种系统特征:顺序系统、反应式系统、并发与通信系统、实时系统、概率随机系统以及混成系统.同时,这些系统又运行在众多应用场景,分别具有各自的需求.考虑4种应用场景:硬件系统、通信协议、信息流以及人工智能系统.对于以上的每个类别,介绍和总结其形式建模、性质描述以及验证方法与工具.这将允许形式化方法的使用者对不同的系统和应用场景,能够更准确地选择恰当的建模、验证技术与工具,帮助设计人员开发更加可靠的系统.

摘要:当前,人脸识别理论和技术取得了巨大的成功,被广泛应用于政府、金融和军事等关键领域.与其他信息系统类似,人脸识别系统也面临着各类安全问题,其中,人脸欺诈(face spoofing,FS)是最主要的安全问题之一.所谓的人脸欺诈,是指攻击者采用打印照片、视频回放和3D面具等攻击方式,诱骗人脸识别系统做出错误判断,因而是人脸识别系统所必须解决的关键问题.对人脸反欺诈(face anti-spoofing,FAS)的最新进展进行研究:首先,概述了FAS的基本概念;其次,介绍了当前FAS所面临的主要科学问题以及主要的解决方法及其优缺点;在此基础上,将已有的FAS工作分为传统方法和深度学习方法两大类,并分别进行详细论述;接着,针对基于深度学习的FAS域泛化和可解释性问题,从理论和实践的角度进行说明;然后,介绍了FAS研究所使用的典型数据集及其特点,并给出了FAS算法的评估标准和实验对比结果;最后,总结了FAS未来的研究方向并对发展趋势进行展望.

摘要:随着机器学习在安全关键领域的应用愈加广泛,对于机器学习可解释性的要求也愈加提高.可解释性旨在帮助人们理解模型内部的运作原理以及决策依据,增加模型的可信度.然而,对于随机森林等机器学习模型的可解释性相关研究尚处于起步阶段.鉴于形式化方法严谨规范的特性以及近年来在机器学习领域的广泛应用,提出一种基于形式化和逻辑推理方法的机器学习可解释性方法,用于解释随机森林的预测结果.即将随机森林模型的决策过程编码为一阶逻辑公式,并以最小不满足核为核心,提供了关于特征重要性的局部解释以及反事实样本生成方法.多个公开数据集的实验结果显示,所提出的特征重要性度量方法具有较高的质量,所提出的反事实样本生成算法优于现有的先进算法;此外,从用户友好的角度出发,可根据基于反事实样本分析结果生成用户报告,在实际应用中,能够为用户改善自身情况提供建议.

摘要:基于线性抽象的符号传播方法在神经网络验证中具有重要地位.针对这类方法,提出了多路径回溯的概念.现有方法可看作仅使用单条回溯路径计算每个神经网络节点的上下界,是这一概念的特例.使用多条回溯路径,可以有效地改善这类方法的精度.在数据集ACAS Xu,MNIST和CIFAR10上,将多路径回溯方法与使用单条回溯路径的DeepPoly进行定量比较,结果表明,多路径回溯方法能够获得明显的精度提升,而仅引入较小的额外时间代价.此外,在数据集MNIST上,将多路径回溯方法与使用全局优化的Optimized LiRPA比较,结果表明,该方法仍然具有精度优势.

摘要:如今,越来越多的社会决策借助机器学习模型给出,包括法律决策、财政决策等等.对于这些决策,算法的公平性是极为重要的.事实上,在这些环境中引入机器学习的目的之一,就是为了规避或减少人类在决策过程中存在的偏见.然而,数据集常常包含敏感特征,或可能存在历史性偏差,会使得机器学习算法产生带有偏见的模型.由于特征选择对基于树的模型具有重要性,它们容易受到敏感属性的影响.提出一种基于概率模型检查的方法,以形式化验证决策树和树集成模型的公平性.将公平性问题转换为概率验证问题,为算法模型构建PCSP#模型,并使用PAT模型检查工具求解,以不同定义的公平性度量衡量模型公平性.基于该方法开发了FairVerify工具,并在多个基于不同数据集和复合敏感属性的分类器上验证了不同的公平性度量,展现了较好的性能.与现有的基于分布的验证器相比,该方法具有更高的可扩展性和鲁棒性.

摘要:随着深度学习技术的快速发展,对其质量保障的研究也逐步增多.传感器等技术的迅速发展,使得收集测试数据变得不再困难,但对收集到的数据进行标记却需要花费高昂的代价.已有工作尝试从原始测试集中筛选出一个测试子集以降低标记成本,这些测试子集保证了与原始测试集具有相近的整体准确率(即待测深度学习模型在测试集全体测试输入上的准确率),但却不能保证在其他测试性质上与原始测试集相近.例如,不能充分覆盖原始测试集中各个类别的测试输入.提出了一种基于多目标优化的深度学习测试输入选择方法DMOS (deep multi-objective selection),其首先基于HDBSCAN (hierarchical density-based spatial clustering of applications with noise)聚类方法初步分析原始测试集的数据分布,然后基于聚类结果的特征设计多个优化目标,接着利用多目标优化求解出合适的选择方案.在8组经典的深度学习测试集和模型上进行了大量实验,结果表明,DMOS方法选出的最佳测试子集(性能最好的Pareto最优解对应的测试子集)不仅能够覆盖原始测试集中更多的测试输入类别,而且对各个类别测试输入的准确率估计非常接近原始测试集.同时,它还能保证在整体准确率以及测试充分性上的估计也接近于原始测试集:对整体准确率估计的平均误差仅为1.081%,比最新方法PACE (practical accuracy estimation)减小了0.845%的误差,提升幅度为43.87%;对各个类别测试输入的准确率估计的平均误差仅为5.547%,比最新方法PACE减小了2.926%的误差,提升幅度为34.53%;对5种测试充分性度量的平均估计误差仅为8.739%,比最新方法PACE减小了7.328%的误差,提升幅度为45.61%.

摘要:深度神经网络在物体检测、图像分类、自然语言处理、语音识别等众多领域上得到广泛应用.然而,深度神经网络很容易受到对抗样本(即在原有样本上施加人眼无法察觉的微小扰动)的攻击,而且相同的扰动可以跨模型、甚至跨任务地欺骗多个分类器.对抗样本这种跨模型迁移特性,使得深度神经网络在实际生活的应用受到了很大限制.对抗样本对神经网络的威胁,激发了研究者对对抗攻击的研究兴趣.虽然研究者们已提出了不少对抗攻击方法,但是大多数这些方法(特别是黑盒攻击方法)的跨模型的攻击能力往往较差,尤其是对经过对抗训练、输入变换等的防御模型.为此,提出了一种提高对抗样本可迁移性的方法:RLI-CI-FGSM.RLI-CI-FGSM是一种基于迁移的攻击方法,在替代模型上,使用基于梯度的白盒攻击RLI-FGSM生成对抗样本,同时使用CIM扩充源模型,使RLI-FGSM能够同时攻击替代模型和扩充模型.具体而言,RLI-FGSM算法将Radam优化算法与迭代快速符号下降法相结合,并利用目标函数的二阶导信息来生成对抗样本,避免优化算法陷入较差的局部最优.基于深度神经网络具有一定的颜色变换不变性,CIM算法通过优化对颜色变换图像集合的扰动,针对防御模型生成更多可迁移的对被攻击的白盒模型不那么敏感的对抗样本.实验结果表明,该方法在一般网络和对抗网络模型上都取得了更高的成功率.

摘要:信息物理系统(cyber-physical system,CPS)的安全控制器设计是一个热门研究方向,现有基于形式化方法的安全控制器设计存在过度依赖模型、可扩展性差等问题.基于深度强化学习的智能控制可处理高维非线性复杂系统和不确定性系统,正成为非常有前景的CPS控制技术,但是缺乏对安全性的保障.针对强化学习控制在安全性方面的不足,围绕一个工业油泵控制系统典型案例,开展安全强化学习算法和智能控制应用研究.首先,形式化了工业油泵控制的安全强化学习问题,搭建了工业油泵仿真环境;随后,通过设计输出层结构和激活函数,构造了神经网络形式的油泵控制器,使得油泵开关时间的线性不等式约束得到满足;最后,为了更好地权衡安全性和最优性控制目标,基于增广拉格朗日乘子法设计实现了新型安全强化学习算法.在工业油泵案例上的对比实验表明,该算法生成的控制器在安全性和最优性上均超越了现有同类算法.在进一步评估中,所生成神经网络控制器以90%的概率通过了严格形式化验证;同时,与理论最优控制器相比实现了低至2%的最优目标值损失.所提方法有望推广至更多应用场景,实例研究的方案有望为安全智能控制和形式化验证领域其他学者提供借鉴.

摘要:领域驱动设计作为一种应对领域复杂性的软件开发方法,近年来得到了广泛应用.作为其中的关键步骤,领域建模仍然面临着领域模型与程序设计之间松散的逻辑关系带来的种种问题.为了应对此问题,基于模型驱动的逆向工程,提出了一种面向领域驱动设计的代码到模型的转换方法,以更好地支持领域建模,并实现了自动化工具原型.该方法能够实时抽象出程序设计对应的领域模型,一方面有助于通过对比程序设计与领域模型的分歧来避免设计偏离模型,另一方面减少了知识消化过程中对代码实现细节的依赖,从而促进了程序设计对建模过程的反馈.案例研究部分将该方法应用于实际软件项目,结果充分表明了其有效性.

摘要:代码审查是一种由其他开发者而非代码作者本人评审代码的形式.在代码审查系统中,开发者通过提交代码变更来修复软件缺陷或添加软件特性.并非所有的代码变更都会被集成到代码库中,部分代码变更会被拒收.被拒收的代码变更有可能被恢复,并继续接受审查,提供代码贡献者改进代码变更的机会.然而,审查恢复过的代码变更需要花费更多的时间.收集了4个开源项目中的920 700条代码变更,采用主题分析方法识别出11类代码变更恢复的原因,并定量分析被恢复的代码变更的特征.主要发现包括:1)导致代码变更恢复的原因中,“提升改进”类型占比最大;2)不同项目之间,代码变更被恢复的原因类别分布存在差异,但并不显著;3)与从未恢复过的代码变更相比,恢复的代码变更接收率低10%,评论数量平均多1.9倍,审查所用时间平均多5.8倍;4)81%的恢复代码变更被接收,19%的恢复代码变更被拒收.

摘要:粗糙集理论(RST)中,求解最小属性约简MAR (minimal attribute reduction)是一种NP-难(non-deterministic polynomial hard)组合优化问题.蚁群优化算法ACO (ant colony optimization)是进化算法中的一种启发式全局优化算法,粗糙集理论与ACO相结合,是求解属性约简的一种有效、可行的方式.针对蚁群优化算法易于陷入局部最优解、收敛速度慢等问题,首先以一种改进的信息增益率作为启发信息,提出了冗余检测机制,对每个被选属性和每代最优约简集合进行冗余检测,并提出了概率提前计算机制,可避免每只蚂蚁在搜索过程中相同路径上的信息反复计算;针对大数据集的属性约简问题,考虑到蚁群优化算法具有并行能力以及粗糙集中“等价类”计算的可并行性,提出一种将ACO与云计算相结合用于求解大数据集的属性约简算法,在此基础上,进一步提出一种多目标并行求解方案.该方案可以同时计算出其余属性相对于当前属性或约简集合的重要度.实验结果表明,该算法在处理大数据的情况下能够得到最小属性约简,计算属性重要度的时间复杂度由O (n²)降至O (|n|).

摘要:法律条文(简称法条)是司法量刑的主要依据,法律条文的精准推荐,能够辅助提高法律智能判决的质量.目前,主流的法条推荐模型是将有限数量的法条当作类别标签,采用分类的思想,根据法律文书的案例描述将其归类到相关的法条.但是法条作为法律规范的文字表述形式,现有的分类方法简单将其作为类别标签的索引编号,导致对其语义信息利用不足,影响了推荐质量.针对此问题,研究将主流的法条推荐方法从分类模型转化为语义匹配模型,提出了基于深度语义匹配的法条推荐方法(DeepLawRec).该方法包含局部语义匹配模块和全局语义推荐模块,分别设计双向Transformer卷积网络模型和基于回归树的推荐模型,在理解文本序列的同时,关注与法条匹配学习相关的局部语义特征,增强法条推荐的准确率和可解释性.在公开数据集上的实验结果表明,DeepLawRec方法在推荐质量上优于传统的文本分类以及经典的语义匹配方法,并进一步探讨了如何分析和判读推荐结果.

摘要:智慧考场是智慧校园的重要组成部分,准确、快速地检测考场中的学生状态,是智慧考场应用的基本任务和关键环节.标准化考场中的考生分布相对密集且成像尺寸差异较大,而现有目标检测算法未充分考虑真实考场的环境特征,很难精确、实时地检测出考生目标,加之大部分目标检测算法需对不同目标手工设计先验锚框,模型部署范围受限.针对以上问题,提出一种高效的无锚框全卷积目标检测模型.该模型采用全卷积网络对输入图像进行逐像素预测,在可能存在目标的区域回归其包围框.在该模型中,设计了基于级联注意力的特征增强模块,通过逐级细化修正特征增强特征图的判别性,有效地提高考生目标识别精度;另一方面,针对真实考场中大量交叠目标检测问题,提出了点监督机制,以进一步提升交叠多目标的识别效果;最后,在构建的标准化考场检测专用数据集上,对所提模型进行验证.实验结果表明,与当前最先进的目标检测模型相比,针对真实复杂的考场环境特征提出的基于级联注意力和点监督机制的全卷积目标检测模型的mAP指标为92.9%,检测速度为22.1 f/s,泛化能力突出,综合效果最优.

摘要:知识图谱是一种基于图的结构化知识表示方式.如何构造大规模高质量的知识图谱,是研究和实践面临的一个重要问题.提出了一种基于互联网群体智能的协同式知识图谱构造方法.该方法的核心是一个持续运行的回路,其中包含自由探索、自动融合、主动反馈3个活动.在自由探索活动中,每一参与者独立进行知识图谱的构造活动.在自动融合活动中,所有参与者的个体知识图谱被实时融合在一起,形成群体知识图谱.在主动反馈活动中,支撑环境根据每一参与者的个体知识图谱和当前时刻的群体知识图谱,向该参与者推荐特定的知识图谱片段信息,以提高其构造知识图谱的效率.针对这3个活动,建立了一种层次式的个体知识图谱表示机制,提出了一种以最小化广义熵为目标的个体知识图谱融合算法,设计了情境无关和情境相关两种类型的信息反馈方式.为了验证所提方法及关键技术的可行性,设计并实施了3种类型的实验:仅包含结构信息的仿真图融合实验、大规模真实知识图谱的融合实验,以及真实知识图谱的协同式构造实验.实验结果表明,该知识图谱融合算法能够有效利用知识图谱的结构信息以及节点的语义信息,形成高质量的知识图谱融合方案;基于“探索-融合-反馈”回路的协同方法能够提升群体构造知识图谱的规模和个体构造知识图谱的效率,并展现出较好的群体规模可扩展性.

摘要:在大数据时代,数据的样本数量、特征维度和类别数量都在急剧增加,且样本类别间通常存在着层次结构.如何对层次结构数据进行特征选择具有重要意义.近年来,已有相关特征选择算法提出,然而现有算法未充分利用类别的层次结构信息,且忽略了不同类节点具有共有与固有属性的特点.据此,提出了基于标签关联性的分层分类共有与固有特征选择算法.该算法利用递归正则化对层次结构的每个内部节点选择对应的固有特征,并充分利用层次结构分析标签关联性,进而利用正则化惩罚项学习各子树的共有特征.该模型不仅能够处理树结构层次化数据,也能直接处理更为复杂常见的有向无环图结构的层次化数据.在6个树结构数据集和4个有向无环图结构数据集上的实验结果,验证了该算法的有效性.

摘要:近年来,随着网络加密技术的普及,使用网络加密技术的恶意攻击事件也在逐年增长,依赖于数据包内容的传统检测方法如今已经无法有效地应对隐藏在加密流量中的恶意软件攻击.为了能够应对不同协议下的加密恶意流量检测,提出了基于Profile HMM的加密恶意流量检测算法.该方法利用生物信息学上的基因序列比对分析,通过匹配关键基因子序列,实现识别加密攻击流量的能力.通过使用开源数据集在不同条件下进行实验,结果表明了算法的有效性.此外,设计了两种规避检测的方法,通过实验验证了算法具有较好的抗规避检测的能力.与已有研究相比,该工作具有应用场景广泛以及检测准确率较高的特点,为基于加密流量的恶意软件检测研究领域提供了一种较为有效的解决方案.

摘要:5G技术为智能家居行业开拓了更大的发展空间,但安全问题也日益突出,用户身份认证作为信息安全防护的第一道关卡备受关注.智能家居系统传统的认证方法存在中心化信任挑战,且资源开销大.区块链技术因其去中心化、不可篡改等优势成为研究热点,为实现分布式智能家居系统安全认证提供了新思路.但无中心认证面临着用户与多个分布式终端认证的效率问题和用户隐私泄露问题两个方面的挑战.提出了一种基于区块链的动态可信轻量级认证机制(dynamic trusted lightweight authentication mechanism,DTL).DTL机制采用联盟链构建区块链系统,既保证了仅授权的智能家居传感器节点可加入网络,又满足分布式高效认证和安全访问需求.DTL具有以下优点:(1) 针对认证效率问题,通过改进共识算法建立面向智能家居的动态可信传感设备组(DT sensor group,DTSG)认证机制,避免了传统的用户端与传感终端或者网关节点之间一对一的频繁认证引起的接入效率低和用户访问速率低问题,实现了轻量级认证;(2) 针对用户隐私保护问题,创新性地设计了DTSG机制和零知识证明结合的认证方案,在不泄露用户隐私情况下,实现了用户身份的认证.对DTL的安全特性进行了定性分析,并通过大量仿真实验对DTL的实用性和轻量级进行了验证.

摘要:近年来,生成对抗网络(generative adversarial network,GAN)家族已在人脸年龄合成任务上取得了巨大的成功.然而,通过研究发现,在解决人脸年龄合成的问题时,即使是善于利用年龄先验信息的条件生成对抗网络(conditional generative adversarial network,CGAN),重要的人脸年龄相关信息在一程度上也会被丢弃.这是导致以CGAN为代表的GAN家族在人脸年龄合成上的性能到达瓶颈期的一个重要因素.为此,提出了一种类别注意实例归一化机制(class-aware instance normalization,CAIN).该机制能够灵活地嵌入到CGAN中,形成一种新的生成对抗网络模型,即CAIN-GAN.CAIN-GAN能够充分利用人脸年龄先验信息来进一步提高人脸年龄合成性能.在公开数据集上的实验结果表明,与其他几种GAN家族的方法对比,CAIN-GAN方法仅通过利用人脸年龄相关信息就能对人脸年龄合成性能进行提升.

摘要:草图一直是人类传递信息的重要工具之一.草图可以通过简单明了的形式更快地表达人类的一些复杂思想,因此,草图处理算法一直是计算机视觉领域的研究热点之一.目前,对草图的研究主要集中在识别、检索和补全等方面.随着研究者对于草图细粒度操作的重视,对草图分割方面的研究也得到越来越多的关注.近年来,随着深度学习与计算机视觉技术的发展,出现了大量基于深度学习的草图分割方法,草图分割的精确度和效率也都得到了较大提升.但是,由于草图自身的抽象性、稀疏性和多样性,草图分割仍然是一个非常具有挑战性的课题.对基于深度学习的草图分割算法进行整理、分类、分析和总结,首先阐述了3种基本的草图表示方法与常用的草图分割数据集,再按草图分割算法的预测结果分别介绍了草图语义分割、草图感知聚类与草图解析算法,然后在主要的数据集上收集与整理草图分割算法的评测结果并对结果进行分析,最后总结了草图分割相关的应用并探讨未来可能的发展方向.