可信计算的研究与发展

可信计算是一种信息系统安全新技术,它已经成为国际信息安全领域的一个新热潮,并且取得了令人鼓舞的成绩.我国在可信计算领域起步不晚、水平不低、成果可喜.我国已经站在国际可信计算的前列.文中综合论述近年来可信计算理论与技术的一些新发展,特别是介绍我国可信计算的一些新发展,并对目前可信计算领域存在的一些问题和今后发展提出了自己的看法和观点.     

信息安全综述

21世纪是信息的时代．信息成为一种重要的战略资源，信息的获取、处理和安全保障能力成为一个国家综合国力的重要组成部分．信息安全事关国家安全、事关社会稳定．因此，必须采取措施确保我国的信息安全．近年来，信息安全领域的发展十分迅速，取得了许多新的重要成果．信息安全理论与技术的内容十分广泛，但由于篇幅所限，这里主要介绍密码学、可信计算、网络安全和信息隐藏等方面的研究和发展．     

基于形式化测试的实时系统变更后安全性验证

变更后系统实现的安全性验证是安全攸关系统维护过程中必不可少的环节,也是其面临的主要挑战之一.软件模型检测和程序验证是目前常用的作用于代码层面的自动化安全性验证技术.本文站在系统行为角度,基于形式化方法,提出了一种将变更后系统实现的安全性验证问题归结为一致性测试的方法,尝试通过自动生成的一致性测试用例在系统行为级别上判定系统实现是否安全.为此,首先以时间输入输出自动机及其语义模型为基础,构建了该方法的证明体系,证明了该方法的正确性;其次,建立了变更后系统实现安全性验证的回归测试生成框架.相对于其它实时系统测试方法,这种测试方法不仅可以发现实时系统中常规的不一致性缺陷,而且为变更后系统实现在运行时是否满足指定的安全性属性提供了依据.最后,以轨道交通系统中的列车自动防护功能的变更情景为案例研究,说明了方法的具体应用.     

一种基于扩展有限状态机的自动化测试用例生成方法

扩展有限状态机(EFSM)是使用最广泛的测试模型之一.由于不可行路径的存在,运用EFSM模型生成测试用例仍然是个难题.本文提出了一种基于EFSM模型的自动化测试用例生成方法 (ATGEM).为解决不可行路径问题,首先提出一种基于数据流分析的路径可行性度量方法来预测路径的可行性,以尽可能避开不可行路径,提高测试用例自动化生成的效率.然后通过建立动态可执行模型来获取运行时反馈信息作为搜索算法的适应度函数(fitness function),实现测试数据和预言信息的自动生成.该方法结合静态分析和动态分析技术生成一个较优可行路径子集和对应测试用例来达到指定的覆盖准则,能够应用于多种数据类型的测试用例生成,适用范围较广.通过实验在多个EFSM模型上验证了ATGEM方法中测试用例生成和路径可行性度量方法的有效性,实验结果表明,利用路径可行性度量方法可以大幅度提高测试用例生成效率,与现有方法相比,ATGEM中的测试用例生成方法具有更高的效率.     

远程证明方法的研究综述

远程证明方法是可信计算理论中一个重要的组成部分，本文追踪该领域的最新发展方向，重点剖析了四大类远程证明模型，并就其优缺点做出了详细的分析，横向上对所有模型进行了比较，从而进一步得到了现有远程证明模型的不足，展望了其未来的发展方向，为该领域的研究奠定了很好的基础.     

基于流形鸽群优化的智能合约重入性漏洞检测方法研究

重入性漏洞在智能合约中普遍存在,可能造成巨大的经济损失.现有的基于符号执行的静态分析工具通过预设的规则判断漏洞是否存在,然而预设规则不全面可能会导致重入性漏洞的误报.为了避免误报,本研究尝试从软件测试用例生成的动态分析角度解决这一难题.本文将该应用场景抽象为存在重入性循环路径的路径覆盖测试用例自动生成问题,通过生成并执行覆盖重入性循环路径的测试用例来检测重入性漏洞.以鸽群算法为代表的群体智能算法是求解测试用例生成这类黑盒优化问题的常用方法.鸽群算法在整个决策空间内围绕种群最优解邻域搜索,然而,问题的最优解可能并不在该邻域内,导致路径覆盖率较低.为了提升鸽群算法的路径覆盖率,本文将利用流形启发式算子改进鸽群算法,使其分配更多的算力搜索与优化目标相关的子空间,从而提升鸽群算法求解效率,覆盖重入性循环路径.实验结果显示,改进后的流形鸽群算法能够更加高效地生成覆盖重入性循环路径的测试用例,检测出被测合约的重入性漏洞.与Oyente, Securify和Smartcheck这三个智能合约测试工具相比,本文提出的方法能够有效避免重入性漏洞的误报,在实验的8个被测试智能合约中重入性漏洞识别准确率分别...     

一个网构软件可信实体模型及基于评估的信任度量

对于运行在开放、动态、难控的互联网环境的网构软件,其可信性保障与管理是一个重要课题．目前的研究多是基于信任网络思想的信任度量及演化模型,这种模型对于网构软件来说,在信任的来源、实体间信任关系的约束、信任传递参数的设置方面仍存在着不足．因此,本文引入可信计算中信任链模型的思想,提出了一个网构软件可信智能实体模型,并在此基础上构建了基于评估的信任度量方法．首先通过动态自省、显式自明和自主演化的机制保障了实体本身的可信,建立了信任的基点;并给出了形式化的描述及交互行为的动态监测;然后通过建立Bayes网络综合推荐信任并使用评估方法加以修正,以精确计算信任传递过程中的衰减参数,建立了信任链传递过程中的可信认证机制;最后通过实验验证了所提出方法的正确性．     

基于金融业务系统的功能测试基准库方法研究

软件自动化测试技术的出现，大大减轻了测试人员的压力，显著提高了测试的效率，但是回归测试中的用例复用是测试自动化所面临的又一难题。本文提出了一种基于金融业务系统的功能测试基准库方法，对回归测试进行有效的支持，力求解决大型业务系统分析资源的积累和测试用例的有效复用等问题。这种方法在一定程度上减轻了测试人员管理测试用例的压力，增强了用例的可复用性，从而有效地提高了自动化测试的效率。     

扩展的语义分析的WAP协议缺陷测试

首先介绍了一种基于语义分析的缺陷测试技术.该测试方法利用语义测试及软件错误注入来进行测试.它比传统测试的成本要小,同时能达到很好的效果.但该方法只能检测协议实现级别的漏洞,而不能检测协议设计中可能存在的缺陷.本文结合了Petri网在协议测试方面的优点提出了一种扩展的语义分析的协议缺陷测试方法.它能通过对协议Petri网模型的分析来捕获协议层面的缺陷,而为此所需的额外开销是很小的.这弥补了原缺陷测试在协议层面的不足.之后对该方法各个阶段进行了介绍.对WAP-WSP协议的进行了缺陷测试,并对结果进行了分析,证明其可行性.     

一种基于一阶逻辑的软件代码安全性缺陷静态检测技术

软件代码安全性缺陷是可能引发软件系统高危后果的一类重要缺陷,针对该类缺陷的自动化检测和定位技术在软件维护和演化研究领域具有重要意义.本文提出并实现了一种形式化检测方法——基于一阶逻辑的软件代码安全性缺陷静态检测方法,利用命题逻辑和谓词逻辑定义模式路径公式,引入多个与依赖关系相关的谓词构造逻辑函数表达式,作为模式路径节点产生的制导条件,实现了对多类软件代码安全性缺陷的形式化描述,把安全性缺陷检测问题转化成在中间代码对应的有限状态空间中是否存在相应模式路径公式的判定问题.实验结果表明,该方法能适用于大多数类型的软件代码安全性缺陷检测,在对openssl,wu-ftpd等13个开源程序的测试中,准确重现了10个已公开安全漏洞,发现2个未公开安全漏洞.并且,与现有的模型检验等形式化静态分析方法相比,该方法的测试时间和代码规模成渐近线性关系.     

基于网络的可信软件大规模协同开发与演化

随着网络时代的来临,软件的开发模式、运行环境和提供方式发生了巨大变化.互联网作为一种开放的协同工作环境,其中孕育的大规模协同创作机理对软件开发和应用产生了深刻影响.如何将其与工业化可信软件生产相结合以提高软件生产效率和质量,是网络时代软件技术面临的新课题.本文提出汇聚群体智慧的可信软件开发新方法——群体化方法,该方法的核心是"群体协同、资源分享、运行监控、可信分析",支持创新软件作品向可信软件产品转化,支持软件的可信演化.提出一种基于证据的可信软件概念模型,将软件在开发阶段、分享阶段和应用阶段的基础数据作为软件的可信证据,并据此建立了软件演化过程模型;提出一种支持可信软件协同开发与演化的服务模型,支持软件创作与生产深度协同的可信软件社会化生产、开放有序的可信软件资源分享,以及基于海量数据分析的软件可信评估.最后以"十一五"国家高技术研究发展计划重点项目"高可信软件生产工具及集成环境"为背景,阐述了面向群体化方法的关键技术、开发环境和应用实践.     

面向协同应用的编程语言Cova

Cova是面向集成性协同应用而设计的一种新型语言. 它提供了一套完整的描述协同系统控制部分及计算部分的设施,并以此为基础通过其运行时系统提供协作过程不同阶段所需的协同计算服务,从而为不同模式协同应用系统的开发提供一个统一的平台. 详细讨论了Cova的语言特性及其运行时系统,并给出了有关结论及进一步工作.     

虚拟计算环境中的嵌入式DHT覆盖网技术

随着计算技术与网络技术的飞速发展,人们提出在互联网之上构建和谐、可信、透明的虚拟计算环境.通过覆盖网动态组织互联网资源是在虚拟计算环境中实现资源有效共享的重要途径.基于DHT的覆盖网技术具有可扩展、延迟低、可靠性高等优点,然而,虚拟计算环境中现有的DHT覆盖网无法满足互联网应用的"可信"需求.针对该问题,文中提出一种虚拟计算环境中的嵌入式DHT技术TrustedSKY,支持上层应用在覆盖网中选择可信节点形成"可信子组"(trustedsubgroup)结构,进而在组中实现安全可信的DHT路由.     

基于身份的跨域直接匿名认证机制

针对现有DAA方案存在计算开销大和无法满足跨域匿名认证需求的不足,本文提出基于身份的直接匿名认证机制,采用代理签名和直接匿名证明技术实现移动互联网下可信移动平台(TMP)的跨域匿名认证;验证者基于签名的合法性完成对TMP平台的真实性鉴别,并在认证过程中协商了会话密钥,增强了跨域证明系统的安全性;同时基于CK模型的安全性证明表明本文机制是可证安全的.分析显示,本文机制具有匿名性、无关联性和高性能等性质的同时,能够抵抗平台的伪装攻击、替换攻击和重放攻击等敌手攻击行为,其性能更适用于移动互联网等无线网络环境.     

基于小波变换的图像扩散滤波方法

图像的非线性扩散滤波基于热扩散方程, 其关键是确定适当的扩散量与扩散方向. 在已有的滤波模型中, 扩散系数依赖于梯度, 因而容易受到噪声的干扰. 为了克服这一缺陷, 首先给出了一种新的计算扩散系数的多尺度方法. 然后建立了一类用于图像恢复的非线性小波扩散（NWD）模型. NWD模型有较强的抗噪能力, 但同已有的模型一样, 需要较大的计算量. 为此, 通过NWD模型的简化, 给出了线性小波扩散（LWD）模型. LWD模型由输运与扩散两部分组成. 由于存在输运, 所以其滤波是各向异性的, 能够较好地保持边缘, 尽管在边缘点处扩散是各向同性的. LWD模型的优点是简单易于分析, 具有较小的计算量. 最后给出了所提模型与已有模型相比较的数值实验结果.     

基于进化算法的递归神经网络系统辨识方法

针对传统的递归神经网络学习算法存在的缺陷,本文利用进化算法对递归神经网络进行优化设计,提出了一种基于改进进化算法的递归神经网络系统辨识方法.该方法利用高斯变异和柯西变异相结合的方式进行变异操作,利用个体适应度和种群多样性指标使交叉概率和变异概率进行自适应调整,可以保证变异操作按一定的幅度均匀地分布在整个网络上,提高算法的收敛速度,避免早熟现象.给出了算法的具体步骤,通过仿真实验证明了该算法的有效性.     

公平交换协议的一个形式化模型

基于对现有公平交换协议的研究，使用求精过程建立了精确的形式化结构模型，在这一过程中，使用不可靠信道模拟攻击行为．模型首次给出了交换项的形式化定义，提出的公平性、可追究性目标能够更加完整地反映公平交换协议的内在要求．为了能高效而又细致地对协议进行检测、证明和设计，模型提出了适用于所有公平交换协议的不可滥用性的新性质，给出了第三方可信赖串的定义和设计安全高效的公平交换协议的一般准则．文中通过一个典型的公平交换协议分析实例，阐明了使用该模型分析公平交换协议的详细步骤．发现了一种过去从未发现过的新攻击，给出了攻击发生时系统运行的全过程，深刻揭示了攻击发生的各种原因．最后，对有缺陷的协议进行了改进，改进后的协议满足所需要的各种性质．     

基于特征的矢量场自适应纹理绘制

针对3D流场纹理可视化方法面临的遮挡问题,提出了一种基于流场特征模糊提取的自适应稀疏纹理绘制方法.该方法建立在一种可扩展的模糊流场特征区域描述与提取算法基础上,首先通过采用模糊理论对流场特征区域进行描述,建立了流场特征的测度规则并得到相应特征向量,然后基于特征向量偏差给出了最小平方和误差准则下的模糊测度隶属度的确定方法.根据得到的流场特征模糊隶属度场,生成可突出流场特征信息的自适应高斯噪声以进行纹理LIC卷积.同时针对纹理方法难以明确表示3D流场具体方向的缺陷,提出了两种冷暖光照方法,通过在LIC卷积过程中采用冷暖光照方法突出流场具体方向显示,有效解决了该问题.实验表明,本文方法相对于传统特征提取方法更具有可扩展性.同时自适应技术的采用,有效缓解了3D流场可视化存在的遮挡和混淆现象.而冷暖光照处理的加入,则解决了纹理方法对流场具体方向表现上的缺陷.     

互联网软件的可信机理

通过分析互联网软件的可信内涵及互联网应用的基本特征，指出：一方面，在开放、动态的互联网环境下，软件的身份可信、能力可信都面临新的问题和挑战；另一方面，基于自主协同运行模式的新型网络应用需要对软件群体行为进行有效约束，以保障其行为可信．在此基础上，给出了一种面向互联网虚拟计算环境（iVCE）的互联网软件可信概念模型，并提出集身份可信、能力可信和行为可信为一体的网络软件可信保证体系，并以跨域的授权管理机制、高可用的服务保证机制和面向自主协同的行为激励机制为突破口，研究和探索互联网软件可信问题的技术途径．     

基于多活性代理的复杂信息系统研究

文中在系统理论指导下分析了信息系统（特别是在激烈对抗环境下,需要多种功能动态运筹发挥作用的复杂信息系统）的特点,提出了基于多活性代理的复杂信息系统研究方法．首先,给出了多活性代理方法的基本描述,初步得到了代理的“活性”表征及丧失的定性定量描述与分析,并从系统功能发挥剖面给出了多活性代理的基本动力学表征;其次,从系统自组织功能剖面给出了活性自组织机理的两集合模型;再次,给出了信息安全与对抗领域多活性代理复杂信息系统构建的功能模型,以及在此模型基础上多活性代理的3层次协商、协调模型;分析了基于Swarm群体结构的多活性代理复杂信息系统的3层次机理模型;最后,通过2个具体实例说明了如何利用多活性代理方法分析信息安全对抗领域复杂信息系统．多活性代理理论的提出将衔接应用基础层和应用层研究,对信息安全与对抗领域复杂信息系统的构建和分析提供基本的研究方法与理论支持．