循环迭代程序的一种可信计算算法

循环迭代程序作为软件的基本组成部分,其正确运行具有重要意义.然而,有时(比如其相关错数大于0时)计算时的舍入误差(或表示误差)会导致循环迭代的计算结果不稳定.基于“中间计算精度自动动态调整”的计算技术,给出了循环迭代程序的一种可信计算算法.利用该算法,可获得循环迭代程序任意次迭代的任意位的正确有效数字.目前,通过C++语言该算法已被编程实现于ISReal中.

一种基于斯格明子介质的高效存内计算框架

存内计算(processing in memory, PIM)作为一种新兴的技术,支持数据在存储单元内就地处理,减少了数据的移动并增加了数据的并行处理,在一定程度上弥补了冯·诺依曼架构的缺陷.和传统易失随机存储介质相比,赛道型内存(racetrack memory, RM)具有密度大、非易失且静态功耗低等特点,支持高效的存内计算.为解决性能与功耗问题,提出了一种新型的基于斯格明子(Skyrmion)介质的非易失性存内计算框架.该框架采用斯格明子赛道内存(Skyrmion-based racetrack memory)作为存储单元,采用斯格明子逻辑门(Skyrmion-based logic gate)构成的加法/乘法器组成计算单元,无须大量CMOS(complementary metal oxide semiconductor)电路辅助,设计复杂度大大降低.同时,通过在电路级优化存储单元读写端口数目与在系统级改进内存地址映射方式,大幅提高该框架的运行效率.实验结果表明:相比基于磁畴壁(domain-wall)的非易失性存内计算框架,提出的框架在运行时间上节省了48.1%,同时在能耗上节省了42.9%.

高效的多边形布尔计算方法

针对计算机图形学中应用广泛的多边形布尔计算,提出了一种新的、适用于一般多边形的并集、交集和差集算法。算法主要分为计算交点、将交点插入多边形顶点序列、遍历三个步骤。通过采用循环单链表的数据结构、避开复杂的出入点计算、及预先的一些碰撞检测以避开复杂的求交运算与链表遍历等技巧,提高了算法的执行速度、减少了存储单元。算法能够很好地处理一些奇异情形(边界情形),比如重叠边、交点为边的顶点等情形,具有很好的鲁棒性。与经典的Weiler算法、Vatti算法和Greiner-Hormann算法相比,该算法具有较低的时间复杂度O((m+n+k)log d))和空间复杂度。实验结果显示该算法在处理2 222×2 222个顶点、42个交点时比经典的Weiler算法速度提高了296倍。算法的主要思想对确定两个多面体的交、并、差问题亦有参考价值。

一种基于学习的高维数据c-近似最近邻查询算法

针对高维数据近似最近邻查询,在过滤-验证框架下提出了一种基于学习的数据相关的c-近似最近邻查询算法.证明了数据经过随机投影之后,满足语义哈希技术所需的熵最大化准则.把经过随机投影的二进制数据作为数据的类标号,训练一组分类器用来预测查询的类标号.在此基础上计算查询与数据集中数据对象的海明距离.最后,在过滤后的候选数据集上计算查询的最近邻.与现有方法相比,该方法对空间需求更小,编码长度更短,效率更高.模拟数据集和真实数据集上的实验结果表明,该方法不仅能够提高查询效率,而且方便调控在查询质量和查询处理时间方面的平衡问题.

边缘计算隐私保护研究进展

移动通信与大数据理论的广泛应用使得外包系统蓬勃发展,资源受限的本地用户将大批量的数据文件和开销巨大的计算任务外包给云服务器完成.然而,为了解决单一的云服务器容易成为敌手俘获攻击的目标导致单点失败,且在基于多输入输出的多用户、多任务场景中由于远离用户端易造成反馈延迟较大而成为外包系统瓶颈的问题,边缘计算应运而生.在边缘计算中,多个位于云服务器与用户端之间的边缘节点相互合作完成外包存储与外包计算任务,很大程度上解决了外包系统的实时性问题;但同时也带来了巨大的安全与隐私保护挑战.首先给出了边缘计算特有的网络模型与安全模型,并在此基础上从边缘计算的隐私保护数据聚合、隐私保护外包计算和包括隐私保护集合运算、隐私保护机器学习、隐私保护图像处理、隐私保护生物认证、隐私保护的密文搜索等面向应用的安全计算问题3方面出发,基于数据扰动、全同态加密、安全多方计算、全同态数据封装机制和可验证与可审计等密码技术,对边缘计算隐私保护领域的国内外最新研究成果进行了系统的阐述、总结与科学归类.最后,探讨了边缘计算隐私保护当前面临的挑战、未来潜在的研究方向及其解决思路,以期进一步推动边缘计算隐私保护研究的发展与应用.

分布式数据流上的高性能分发策略

随着大数据应用的普及,高效可扩展的数据流操作在实时分析处理中扮演着越来越重要的角色.分布式并行处理架构是应对大流量、低延时数据流处理任务的一种有效解决方案.然而在Key-based分组并行处理中,由于数据的倾斜分布及数据流本身的实时、动态和数据规模不可预知等特性,使得数据流分布并行处理系统存在持续且动态负载不均衡现象,这会造成系统时效性降低、硬件资源浪费等问题.现有的研究工作处理均衡负载有两种方案:(1)基于key粒度的迁移,使得并行处理节点负载达到均衡;(2)基于元组粒度级别的拆分,采用随机分发使系统均衡.前者将系统调整至给定的均衡容忍范围内,类似于一维装箱的NP问题;后者对key的拆分势必带来新的为维护Key-based操作的正确性而增加的额外代价,如内存及网络通信成本.综合两种方法,提出对key按需拆分、尽量合并的方法,通过轻量级均衡调整算法以及保证Key-based操作特性的拆分方法,使系统既能达到后者的均衡,又能减少细粒度均衡所带来的额外代价.

人工智能系统可信性度量评估研究综述

近年来,人工智能技术突飞猛进,人工智能系统已经渗透到人们生活中,成为人们生活中不可或缺的一部分.然而,人工智能系统需要数据训练模型,数据扰动会对其结果造成影响.并且随着人工智能系统业务多样化,规模复杂化,人工智能系统的可信性愈发受到人们的关注.首先,在梳理不同组织和学者提出的人工智能系统可信属性基础上,提出人工智能系统的9个可信属性;接着,从数据可信性、模型可信性和结果可信性分别介绍现有的人工智能系统数据、模型、结果可信性度量方法,设计人工智能系统可信证据收集方法.其次,总结当前人工智能系统的可信度量评估理论与方法.然后,结合基于属性的软件可信评估方法与区块链技术,建立一个人工智能系统可信度量评估框架,包括可信属性分解及可信证据获取方法、联邦式可信度量模型与以及基于区块链的人工智能系统可信度量评估架构.最后,讨论人工智能系统可信度量技术面临的机遇和挑战.

面向云网融合的细粒度多接入边缘计算架构

随着智能终端设备的爆发式增长,多接入边缘计算(multi-access edge computing,MEC)成为支持多服务、多租户生态系统的关键技术之一.多接入边缘计算通过结合云端的移动计算技术和接入网的无线通信技术,实现了云端和网络的高效融合.然而,目前的边缘计算技术对于所有可能的资源(例如计算、通信、缓存)并没有细粒度的控制能力,因此并不能对延迟敏感的实时服务提供很好的支持.为了解决这个关键问题,设计了一种基于软件定义(software defined)的细粒度多接入边缘计算架构,可以对网络资源和计算资源进行细粒度的控制并进行协同管理,并设计了一种基于深度强化学习Q-Learning的两级资源分配策略,从而提供更有效的计算卸载和服务增强.大量的仿真实验证明了该架构的有效性.

ChatModeler:基于大语言模型的人机协作迭代式需求获取和建模方法

需求获取和建模是需求工程中的关键步骤,影响后续系统设计与实现.传统的需求获取和建模方法通常由需求提供者、需求分析师等多类干系人共同协作、反复迭代完成,需要耗费大量的人力.如何减轻需求提供者与需求分析师的负担、提高获取和建模的效率有着重要意义.现有工作中有的使用知识库来提供更多知识,以辅助获取或者建模,有的利用自然语言处理等技术对获取或者建模过程进行自动化,但是它们并没有减轻需求提供者的负担.利用大语言模型(large language models,LLMs)的生成能力,提供了一种人机协作的迭代式需求获取和建模框架ChatModeler.具体来说,根据真实世界中需求团队的分工及协作关系,将部分需求提供者、需求分析师等角色的工作由大语言模型承担,而需求提供者只需要进行确认.为大语言模型扮演的各种角色进行了提示词设计,该提示词会随需求的元模型而变化.ChatModeler在7个需求案例上与3种需求模型的自动建模方法进行了14组对比实验,证明了ChatModeler在降低需求提供者的负担和生成高质量需求模型2个方面上的优越性.

关于安全案例论证构建的综述

安全案例提供清晰、全面和可靠的论据,说明系统在特定环境下的操作满足可接受的安全性.在受监管的安全攸关领域,如汽车、航空和核能等领域,认证机构通常要求系统经过严格的安全评估程序,以确保其符合一个或多个安全标准.在系统开发中应用安全案例是一种新兴的技术手段,以结构化和全面的方式表达安全攸关系统的安全属性.对安全案例的4个基本构建步骤:确定目标、收集证据、构建论证和评估安全案例,进行简要介绍.然后聚焦于构建论证这一关键步骤,详细介绍现有的8种安全案例表达形式,包括目标结构符号(GSN)、声明-论点-证据(CAE)、结构化安全案例元模型(SACM)等,并分析了它们的优缺点.由于安全案例所需材料的显著复杂性,软件工具通常被用作构建和评估安全案例的实用方法.比较7种用于安全案例开发和评估的工具,包括astah system safety、gsn2x、NOR-STA、Socrates、ASCE、D-Case Editor和AdvoCATE.此外,还深入探讨了安全案例构建中所面临的多重挑战,这些挑战包括数据的可靠性和完整性、复杂性和不确定性的管理、监管和标准的不一致、人因工程、技术的快速发展以及团队和跨学科合作6个方面.最后,展望安全案例的未来研究方向,揭示其潜在应用和研究问题.

用户评论的质量检测与控制研究综述

随着网络技术的发展,越来越多用户生成的内容(user-generated content)出现在网络应用中,其中,用户评论富含用户的观点,它们在网络环境中充当越来越重要的角色.据美国Cone公司2011年的调查报告,64%的用户在购买行为之前会参考已有的用户评论.因此,为用户提供准确、简洁和真实的评论是一个迫切且重要的任务.主要围绕评论质量评估、评论总结和垃圾评论检测这3个方面综述了国际上评论质量检测与控制的研究内容、技术和方法的研究进展.在此基础上,展望该领域的发展给出了可能的研究方向.

推荐系统的隐私保护研究进展

推荐系统是建立在海量数据挖掘基础之上的一种智能平台,根据用户个人信息与物品特征,比如用户的兴趣、历史购买行为和物品的材质、价格等,利用统计分析和机器学习等人工智能技术建立模型,预测用户对新物品的评价与喜好,从而向用户推荐其可能感兴趣的潜在物品,以实现个性化的信息服务和决策支持.然而,推荐系统的历史数据集、预测模型和推荐结果都与用户的隐私休戚相关,如何能在有效保护用户隐私的前提下,提供正确性可验证的有效推荐结果是一个具有挑战性的重要研究课题.国内外现有的工作多是通过数据扰动或公钥全同态加密技术来试图解决这个问题,但都无法满足推荐系统对高效性、精确性和各类隐私保护的要求.从推荐系统隐私保护的模式、安全模型、轻量级的推荐系统隐私保护一般性构造与推荐结果正确性可验证、可审计等方面,系统阐述了国内外最新研究成果,并在此基础上提出了存在问题、未来研究方向与解决方案.在安全模型方面,聚焦于标准模型或通用组合模型下,用户数据隐私、预测模型隐私和推荐结果隐私等多种安全模型的形式化刻画;在轻量化方面,将不依赖公钥全同态加密技术,通过减少公钥加密解密次数(最优时一次),在单用户、多数据模型和多用户、多数据模型下,提出高效的推荐系统隐私保护一般性构造方法;最后,通过批量验证技术研究推荐结果轻量化防欺诈与抗抵赖的一般性理论问题.从而,为适用于推荐系统隐私保护的新型加密方案研究及其实用化提供理论和方法支撑.

在线/离线密文策略属性基可搜索加密

在云计算环境中,越来越多的手机用户通过移动网路来共享自己的数据文件.但是由于云不是完全可信的,所以会出现一些安全隐私上的问题,针对这些问题,随之提出了各种基于属性基加密的解决方案.然而,其中大部分的工作要么是在加解密阶段存在大量的在线计算成本,要么是不支持加密数据的关键字搜索功能.而且大多的属性基加密机制会对数据共享、信息查询、数据细粒度管理等方面的效率性产生影响.为了解决这些问题带来的挑战,提出了一种新的密码学原语:在线/离线密文策略属性基可搜索加密方案(online/offline ciphertext-policy attribute-based searchable encryption scheme,OOCP-ABSE).通过利用现有的在线/离线属性加密技术和属性基加密的外包解密技术,构造出高效的OO-CP-ABSE方案,使得数据拥有者端的在线计算代价最小化,同时使得数据用户端的解密计算代价最低;还给出了在云计算环境下,OO-CP-ABSE方案在移动设备上的应用;最后,给出了OO-CP-ABSE方案的安全性分析(数据机密性、关键字隐私安全、搜索可控性、陷门安全性)以及同现有其他方案的效率比较.

信息物理融合系统的时间需求一致性分析

信息物理融合系统(cyber-physical system,简称CPS)蕴藏着巨大的潜在应用价值.时间在CPS中起到非常重要的作用,应该在需求早期阶段明确.提出了一个基于逻辑时钟的CPS时间需求一致性分析框架.首先,构建了CPS软件的时间需求概念模型,提供时间需求和功能需求的基本概念,并给出了概念模型的形式化语义;然后,在模型制导下,从CPS的交互环境特性和约束中提取出其软件时间需求规约.基于形式化语义,定义了时间需求规约的一致性特性.为了支持形式化验证,将时间需求规约转换成NuSMV模型,用CTL公式表述要检测的特性,并使用NuSMV工具实施了一致性检测.

嵌入式实时操作系统内核混合代码的自动化验证框架

"如何构造高可信的软件系统"已成为学术界和工业界的研究热点.操作系统内核作为软件系统的基础组件,其安全可靠是构造高可信软件系统的重要环节.为了确保操作系统内核的安全可靠,将形式化方法引入到操作系统内核验证中,提出了一个自动化验证操作系统内核的框架.该验证框架包括:(1)分别对C语言程序和混合语言程序(C语言和汇编语言)进行验证;(2)在混合语言程序验证中,为汇编程序建立抽象模型,并将C语言程序和抽象模型粘合形成基于C语言验证工具可接收的验证模型;(3)从规范中提取性质,基于该自动验证工具,对性质完成自动验证;(4)该框架不限于特定的硬件架构.成功地运用该验证框架对两种不同硬件平台的嵌入式实时操作系统内核μC/OS-Ⅱ进行了验证.结果显示,利用该框架在对两个不同的硬件平台上内核验证时,框架的可重复利用率很高,高达83.8%,虽然其抽象模型需要根据不同的硬件平台进行重构.在对基于这两种平台的操作系统内核验证中,分别发现了10处~12处缺陷.其中,在ARM平台上两处与硬件相关的问题被发现.实验结果表明,该方法对不同硬件平台的同一个操作系统分析验证具有一定的通用性.

不确定环境下智能大厦空调系统调度策略评估

近年来,智能大厦的概念在国内外受到了高度的关注.相比于传统的建筑,智能大厦更加节能、舒适、易维护,已成为未来建筑的发展趋势.作为智能大厦空调通风系统的关键部分,空调系统及其调度策略决定了大厦整体的节能效果以及大厦中用户的舒适度.然而,由于智能大厦所处的环境具有许多不确定因素,极大地增加了空调系统调度策略设计与评估的复杂程度.因此,如何设计与评估不确定环境下空调系统的调度策略成为了智能大厦设计者面临的一大挑战.已有的方法主要针对智能大厦空调系统进行能耗与性能等方面的分析,但尚未有方法针对调度策略本身进行分析与评估.提出一种基于价格时间自动机的调度策略评估框架,支持对不确定环境下的智能大厦进行精确建模与定量评估.该框架使用UPPAAL-SMC作为属性查询引擎对模型进行随机模拟运行,根据模拟结果对不同调度策略下大厦的能耗及用户的舒适度进行定量分析.实验结果表明,该方法能够有效地帮助设计者进行策略的制定和选取.

软件动态正确性的形式化描述

软件正确性是一个逐渐改进的过程.通过不断地修改,软件越来越接近于正确.同时软件的执行依赖于环境.为了刻画软件的动态正确性并考虑环境的因素,以参数化互模拟为基础,利用极限的观点,建立软件动态正确性的形式化描述.首先建立参数化互模拟的无限演化理论,给出参数化极限互模拟的定义,并给出几个特殊的参数化极限互模拟实例.其次,建立参数化互模拟极限,给出参数化互模拟极限的规约刻画.最后,证明参数化互模拟极限的唯一性、与参数化互模拟的相容性等代数性质.

基于Coq的Paxos形式化建模与验证

Paxos是一个在不可靠的分布式处理器网络中解决共识问题的算法族.共识问题是指分布式系统中一组参与者就一个结果达成一致的过程.随着Paxos在大型分布式系统中的广泛运用,比如区块链系统以及谷歌文件系统等,其安全性证明越来越重要.在定理证明工具Coq中,形式化描述和定义了Lamport的Basic Paxos算法,并且证明了其满足共识性.

传感网中的四锚点节点定位实解个数分析

针对物联网感知层调度问题,研究和分析三维空间基于四锚点节点定位实解个数的分类问题.利用不等式机器证明理论和研究成果以及不等式机器证明软件DISCOVERER,分析了四锚点定位在特定情形下的实解分类判别问题.首先给出定位问题的数学描述,将传统定位方法中存在的非线性方程组转化为不等式约束的多项式方程组;然后,利用不等式机器证明理论和工具初步探讨了方程组在部分参数固定情况下的解的分类,给出了这种情况下的解的完全分布.分析结果表明:空间四锚点定位存在多解问题,给出的多解分类判别条件对实际应用具有指导作用,对提高节点布局和精确信息感知具有参考价值.

SDN数据平面软件一致性测试用例生成方法

SDN(software-definednetwork)旨在解决架构复杂且分散的传统网络出现的问题,使网络具有更强的灵活性.P4编程语言的特征在于用户可以直接根据自己对处理数据包的需求定义P4程序,然后经过编译过程,生成适配文件将用户需求配置到网络设备.面向P4编程语言的SDN数据平面一致性测试,是将一致性测试用例发送给P4网络设备,评估实际输出和预期输出的一致程度.一致性测试用例是执行一致性测试的载体,而传统的人工构造测试用例是一项繁琐耗时费力的工作.重点分析了面向P4编程语言的SDN数据平面软件一致性测试用例设计原则和生成方法,给出了一致性测试用例覆盖标准,设计了命令信息实体结构和测试用例实体结构,以装载P4程序的simpleswitch虚拟交换机为测试对象,说明一致性测试用例生成过程,实现了一个用于P4网络设备一致性测试的测试用例自动生成工具,并验证了该工具自动生成测试用例的有效性,实现了一致性测试用例构造过程简易性.