摘要：网络隐蔽信道是以合法网络通信信道作为载体建立的一种隐蔽通信技术.相比信息加密,网络隐蔽信道不仅隐藏了传输信息的内容,同时还隐藏了传输信息的行为,因而具有更强的隐蔽性.隐蔽信道技术的出现,使得网络通信中的信息安全和隐私保护受到了极大的威胁,尤其是间谍和其他不法分子可以利用隐蔽信道绕过系统的安全检查机制,窃取机密信息.因此,研究高效且准确率高的隐蔽信道检测技术势在必行.在分析和总结前人研究成果的基础上,提出了差分信息熵的概念,进而提出了基于差分熵的网络时序型隐蔽信道检测算法.首先给出了差分信息熵的定义和相关特性,然后给出了基于差分信息熵的隐蔽信道检测算法的实现原理,以及算法在具体实现过程中的参数设定,最后设计实验检测算法的性能和效果.实验结果表明,基于差分信息熵的检测算法可以有效检测IPCTC,TRCTC,JitterBug 时序型隐蔽信道.

摘要：面向对象技术的发展改变了传统软件系统的结构和设计方法学．本文作者提出一种称为ＳＣＯＰ的面向对象的软件系统结构模式，即软件是对象模块的复合，而软件设计则是对象模块经过程控制进行复合的构造生成．本文从语义模型、描述语言、设计方法学和支持环境等几方面对ＳＣＯＰ进行扼要的介绍．

摘要：为类C小语言PointerC设计的指针逻辑是Hoare逻辑的一种扩展,可用来对指针程序进行精确的指针分析,以支持指针相等关系确定的程序的安全性验证.通过增加相等关系不确定的指针类型访问路径集合,可扩展这种指针逻辑,使得扩展后的指针逻辑可以应用于有向图等指针相等关系不确定的抽象数据结构上的指针程序性质证明.

摘要：离散时空事件预测是城市计算领域中的重要科学问题之一.现有工作主要聚焦于使用多样化的时空神经网络对城市动态特征与事件时空关联进行建模,且已经取得了一定成效,但仍然存在以下问题:首先,城市事件具有诱因多源和时空稀疏性,而这种时空稀疏性可能同时源于事件本身的稀少性和采集的不完整性,现有工作尚未能解决短期预测中的稀疏性挑战及零膨胀问题;其次,已发生事件倾向于继续向周边区域传播事件风险,但由于现有工作同质化了动态特征和事件之间的交互关联,因此其不能捕捉历史事件对未来事件风险带来的交互影响.鉴于此,为协同地利用事件标记信息和时空特征,本文提出基于教师-学生时空半监督学习框架以预测短期离散事件的时空分布.在教师网络中,为应对事件标记的稀疏性,本文在时空学习中引入半监督机制,提出基于自编码器的特征重建和时空方差异常描述引导的动态特征表示学习;在学生网络中,本文设计了特征-事件解耦的双管道学习机制,并提出时空衰减图卷积网络与长短期记忆网络来模拟事件在时空范围内发生的风险传播.此外,本文发展了时空多粒度预测机制,通过易学的粗粒度预测任务指导细粒度的高质量预测,最终实现粗-细粒度协同提名的离散时空事件预测.实验基于纽约和苏州工业园区数据集开展,本文模型能够在事件击中准确率上分别超越最好的基线模型5.46%和10.65%,充分验证了提出方法的有效性.

摘要：形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来验证系统软件的功能正确性,这种验证方式表达力强,可以证明复杂系统,但是自动化程度低、验证代价比较高;而使用程序验证器接受经过规范标注的源代码生成验证条件,并将验证条件交给约束求解器自动求解,这种方式自动化程度高,缺点在于它很难验证复杂系统软件的全部功能的正确性.结合上述两种方式的优点,在定理证明工具Coq中实现了一个自动证明策略smt4coq,它通过在Coq中调用约束求解器Z3自动证明32位机器整数相关的数学命题,提高了自动化验证的程度,减少了用户手动验证程序的开销.

摘要：形式验证是提高软件可信程度的重要方法,基于逻辑推理对程序性质进行严格的自动证明是当前的研究热点,但尚无可供工业界使用的产品,其根源在于自动定理证明方面的困难.介绍在通过程序分析建立起各程序点的形状图的基础上,如何利用形状图提供的信息来支持程序验证的方法.提出一种利用形状图信息来消除访问路径别名,使得指针程序中非指针部分的性质仍然可以用Hoare逻辑来进行验证的方法,并证明了该方法的可靠性.还提出一种在不使用自定义谓词的情况下,易变数据结构上数据性质的描述和验证方法.另外,介绍所设计并实现的基于上述方法的PointerC语言的程序验证器的原型.它不仅能自动验证操作易变数据结构程序的性质,也能自动验证使用一维数组的程序的性质.

摘要：Rust是为了解决系统编程领域的安全性问题,而设计的一门面向系统编程的兼具类型安全、内存安全和并发安全的新型程序设计语言,强调安全性和高性能,已经在操作系统内核、Web浏览器、网络协议栈、数据库和区块链等底层软件系统的构建中得到了越来越广泛的应用。现有研究表明,尽管Rust的设计目标是保证安全性,但其自身仍然存在许多安全问题。作为一门系统编程语言,Rust的安全性直接影响到基于Rust开发的软件系统的安全性。随着Rust的广泛应用,对Rust语言安全的研究显得尤为重要。Rust语言安全研究正在成为研究热点,并且在近几年已经取得了较大研究进展。本综述基于该研究领域已经公开发表的46篇研究论文,对该领域的相关研究进行了系统整理、分析和总结:首先,研究分析了Rust的核心安全特性,包括函数式编程范式、强多态类型系统、基于所有权模型的自动内存管理、对非安全代码的显式标记和隔离;其次,提出了Rust语言安全研究领域的分类学,将已有研究分为安全实证研究、漏洞检测研究、安全增强研究和形式化验证研究四个热点方向,并分别对这四个方向上的相关研究进行了综述、深入分析和总结,同时分析了四个研究方向的内在联系;最后,指出了该研究领域的待解决的科学问题,并对未来可能的研究方向进行了展望,提出了四个潜在的研究方向,以期为相关领域的研究者提供有价值的参考。

摘要：提出一种H.264去块滤波系统的优化设计方法。通过合理设计流水线级数提高并行性,适当增加内部SRAM来提高系统速度和总线利用率,使用一种层次化的有限状态机设计方法,实现对数据流的精确控制并且有效降低硬件实现复杂度。基于FPGA的验证结果显示在最坏情况下滤波每个宏块平均只需220个时钟,比原有方案快10个时钟以上。

摘要：本文是[1]中内容的继续,讨论系统模型开发的形式化技术。基于多类一阶逻辑设计的概念模型语言CML可用来描述系统模型,并可用CMA对模型描述进行静态一致性和动态时序特性的检查。

摘要：随着互联网技术的进步,以视频实时评论为代表的众包短文本(又称弹幕)逐渐流行,对在线媒体分享平台和娱乐产业都带来了重要影响.针对此类短文本展开研究,为推荐系统以及人工智能等领域的发展提供了新的机遇,在各行各业都具有巨大价值.然而在弹幕带来机遇的同时,理解和分析这种面向视频的众包短文本也面临诸多挑战:视频实时评论的高噪声、不规范表达和隐含语义等特性,使得传统自然语言处理(natural language processing, NLP)技术具有很大局限性,因此亟需一种容错性强、能刻画短文本深度语义的理解方法.针对以上挑战,在"相近时间段内的视频实时评论具有相似语义"假设的基础上,提出了一种基于循环神经网络(recurrent neural network, RNN)的深度语义表征模型.该模型由于引入了字符级别的循环神经网络,避免了弹幕噪声对文本分词带来的影响.通过使用神经网络,使所得的语义向量能够表达弹幕的隐含语义.在此基础上,进一步设计了基于语义检索的弹幕解释框架,同时作为对语义表征结果的应用验证.最后,设计了多种对比方法,并采用不同指标对所提出的模型进行充分的验证.该模型能够精准地刻画弹幕短文本的语义,也证明了关于弹幕相关假设的合理性.