同步数据流语言输入结构体的可信翻译

为最大程度地减少同步数据流语言编译过程中由编译器引入的错误,需要利用形式化方法自动生成代码,保证编译器产生的代码能够应用于核能仪控系统.本研究使用定理证明工具Coq,对同步数据流语言Lustre到Clight的主节点输入结构翻译阶段涉及的语法、语义及翻译算法进行了形式化定义,并完成翻译算法的形式化证明.研究表明这种经过形式化的编译器能够生成与源代码行为一致的可信目标代码,同时生成的目标代码能够很好满足核能仪控系统的执行规范.

同步数据流语言可信编译器的构造

同步数据流语言近年来在航空、高铁、核电等安全关键领域得到广泛应用.然而,此类语言相关开发工具本身的安全性业已成为被高度关注的安全隐患之一.借助辅助定理证明器实现常规语言编译器的构造和验证已被证明是成功的,有望最大限度地解决误编译问题.基于这种方法,开展了从同步数据流语言(Lustre为原型)到串行命令式语言(C为原型)的可信编译器构造的关键技术研究.其挑战性在于两类语言之间的巨大差异,源语言具有时钟同步、数据流、并发及流数据对象等特征,而目标语言则具有顺序控制流特征.同类研究中,目前尚无针对核心翻译过程的公开成果.就单一时钟的情形实现了一个经过形式化验证的完整编译过程,相关技术将应用于安全关键领域编译系统的开发.综述了这一可信编译器的研究背景、意义、总体设计框架、核心技术、现状以及进行中或后续的工作.

可信编译器L2C的核心翻译步骤及其设计与实现

同步数据流语言(如Lustre)近年来在航空、高铁、核电等安全攸关领域得到广泛应用.这些领域对相关开发工具本身的安全性有着相当高的要求.为尽力解决好"误编译"问题,近期人们借助reliable-by-construction辅助定理证明器实现常规命令式语言编译器的构造和验证,取得了很大的成功,如Comp Cert C编译器.L2C是基于这种方法开发的可信编译器.它以扩展的Lustre语言为源语言,以Clight(Comp Cert中的C语言子集)为目标语言.L2C是面向实际工业应用的同步数据流语言编译器.重点介绍L2C编译器的核心翻译步骤及其设计与实现过程中考虑的主要问题和相关经验.

一种用于指针程序验证的指针逻辑

本文改进并扩展先前为验证指针程序提出的指针逻辑,主要贡献是提出了合法访问路径集合的概念,极大地简化了访问路径上的基本运算,并使得指针逻辑推理规则变得易理解.另外,增加了局部推理规则和函数构造的推理规则,使得指针逻辑可以方便地用于有函数调用的场合.

一种汇编程序的形式验证框架

在高可信软件的各种性质中,安全性是关注的重点.软件满足安全策略的证明方法是安全性研究的热点之一.根据前期提出的安全程序设计与证明的框架以及指针逻辑推理系统,介绍在所实现的出具证明编译器(certifying compiler)原型系统中有关目标机器的形式定义、汇编程序的形式验证框架以及汇编程序指针程序性质证明等方面的研究.它们的主要特点是汇编验证框架是基于Hoare风格的程序验证方式;与指针有关的性质使用和源语言一级类似的指针逻辑推理系统进行证明;使用一个简单的类型系统完成有关指针的类型检查.

一个C语言安全子集的可信编译器

以安全关键领域的安全标准为依托、安全相关软件的语言编码和编译要求为指导,进行了以下几方面的研究和探索:首先对形式化验证可信编译技术进行分析研究,特别着重当前广受关注的经过验证的CompCert编译器。然后以我国安全领域C语言安全子集标准《航天型号软件C语言安全子集》为依据构造测试用例、创新测试方法,并以此对CompCert编译器进行测试评估。之后依据测试结果,为CompCert编译器增加未支持的C语言标准特性,裁剪不符合C语言安全子集要求的特性,构建符合C语言安全子集标准的可信编译器。最后的实测结果表明,所实现的编译器符合C语言安全子集标准的要求,且没有降低C代码的执行效率。

汇编代码验证中的形式规范自动生成

与传统的高级语言程序验证相比,汇编代码验证中所需要的形式规范往往比较复杂,通常的做法是要求程序员手写形式规范,或是牺牲形式规范的表达能力以期能够自动生成规范.本文提出一种能够自动生成形式规范的方法,该方法依托一个出具证明的编译器自动生成汇编级形式规范,从而减轻程序员的负担.使用该方法生成的规范比现有的其他方法自动生成的规范具有更强的表达能力.文章主要描述该方法在出具证明编译器中的实现.

基于ECC的自认证广义指定验证者签密

广义指定验证者签名允许签名的持有者指定签名给指定的验证者,但仅有指定的验证者能够验证这个签名,针对该问题,利用椭圆曲线密码体制(ECC)和自认证签密的特点,提出一个基于ECC的自认证广义指定验证者签密。该方案不仅消除了证书存在问题和密钥托管问题,而且具有算法复杂度低、处理速度快、存储空间占用小等特点,适合应用于电子投票、电子拍卖等领域。

自认证广义指定验证者签密方案

基于自认证签密和广义指定验证者签名的思想,一个新的自认证广义指定验证者签密方案被提出,在椭圆曲线离散对数问题和双线性Diffie-Hellman问题的困难性假设下,该方案被证明是安全的。该方案允许签密的持有者指定签密给指定的验证者,仅仅只有指定的验证者能够验证这个签密,不存在证书管理问题和密钥托管问题,具有存储量小、安全性强等优点,在电子商务和电子政务中具有很实用的价值。

基于DLP的自认证代理签密方案

自认证密码体制可以实现无公钥证书和密钥托管,代理签密是将代理签名和签密相结合的一种方案。在已有研究的基础上,集成自认证密码体制和代理签密,提出了一种新的基于DLP的自认证代理签密方案,并在有限域上离散对数问题的难解性下,给出了其正确性和安全性证明。

基于类型注解的认证编译器设计与实现

基于类型注解的认证编译器是安全策略系统的核心部件 ,它不仅能够用C语言的类型安全子集编写的程序编译成优化的Intelx86 /linux汇编语言程序 ,而且还可以根据类型安全策略的要求产生带注解的汇编程序 实验结果表明 ,新设计的认证编译器可实现 :①类型安全的C语言子集的编译 ;②许多标准的局部优化 ;③可以对数组运行时越界操作进行检查 由于安全策略系统的证明是建立在含注解的代码基础之上的 ,因此 。

基于扩展逻辑变换系统_μTS证明循环优化正确性

循环优化对于提高Cache性能、发掘程序的并行性以及减少执行循环的开销都有着重要的作用,证明带循环优化功能的现代编译器的正确性已成为可信编译的一个挑战性的问题.形式化证明一个羽翼丰满的优化编译器本质上是不可行的,可以使用替代的方法,即不是证明优化编译器本身,而是形式化证明每一次循环变换前后编译对象的正确性.提出一种新颖的基于扩展逻辑变换系统μTS来证明循环优化正确性的方法.系统μTS在逻辑变换系统TS的基础上扩展了若干条派生规则,经谓词抽象将源程序与目标程序转换为形式化Radl语言后,使用μTS的派生规则能证明常见循环变换的正确性,如循环融合、循环分配、循环交换、循环反转、循环分裂、循环脱皮、循环调整、循环展开、循环铺盖、循环判断外提、循环不变代码外提等.循环优化可以看作一系列循环变换的组合,从而系统μTS能证明循环优化的正确性.为了支持自动化证明循环优化的正确性并出示证据,进一步提出了一个辅助证明算法.最后通过一个典型实例对这一方法进行了详细的阐述,实际效果表明了该方法的有效性.该方法对设计高可信优化编译器具有重要的指导意义.

20世纪80年代以来国内李益诗歌研究述评

李益是中唐前期的著名诗人,近20年来李益研究逐渐深入。学界在李益生平事迹的考证、诗集的整理、作品真伪考辨以及李益诗歌的题材内容、艺术特色等方面取得了丰富的成果。同时,李益研究也存在着考证结论缺乏确凿证据,部分研究建立在前人颇多瑕疵的结论之上,选题立论及论述单一重复,部分领域无人涉及等问题。李益研究拥有广阔的前景,有待于学者去挖掘和探索。

PCC中数组边界检查的优化和生成

PCC的数组边界检查存在着由于无法确定数组下标表达式符号值的范围 ,而造成拒绝执行一些安全的移动代码等问题 .本文给出的一种数组边界检查的优化及生成算法 ,不仅能够比较好地解决了这一问题 ,同时还生成了循环不变式注解中的条件谓词 .我们设计的编译器———认证编译器———已经实现了这些算法 ,并完成了从用C编程语言的类型安全子集编写的源程序到携带注解的Intelx86 /linux汇编语言程序的编译过程 .由于基于语言安全策略系统的证明是建立在携带注解的代码基础之上的 ,因此该认证编译器中实现的算法在移动代码安全检查中非常有用 .

基于DLP的自认证广义指定验证者密签方案

有机集成广义指定验证者签名和自认证签密的思想,提出了一个基于DLP的自认证广义指定验证者签密方案,方案的困难性基于有限域上的离散对数问题.所提方案不仅能够保护签密持有者的隐私,而且消除了证书存在问题和密钥托管问题.由于新方案具有通信代价低、计算量少和安全性强等优点,在电子商务和电子政务活动中将具有重要应用.

使用双线性对的指定验证人代理签密

指定验证人代理签密要求代理签密人只能对发给指定验证人的信息代理原始签密人签密,而其他人则不能代理原始签密人签密。基于指定验证人代理签密和自认证密码系统的理论,一个使用双线性对的指定验证人代理签密被提出。该方案具有以下特点:在传送代理签密时,没有必要传送消息,因为指定验证人能从代理签密中正确恢复出消息;能够在逻辑单步内同时验证代理签密的有效性和公钥的真伪;克服了密钥托管问题;不需要对公钥显式认证。与已有方案相比,新方案仅仅需要2次pairings运算,效率很高。

新的基于自认证公钥的代理签名方案

代理签名在数字化信息社会中有着广泛的应用.基于自认证公钥系统,提出了一个新的基于自认证公钥的代理签名方案.该方案不仅可以实现代理签名人代表原始签名人生成代理签名的目的,而且在传送签名时,不需要传送消息本身,因为验证人在验证代理签名时可以恢复出消息.和其它代理签名方案,该方案降低了传输消息本身所需的通信开销,适用于对短消息签名.

论钱谦益与明史的修撰与考证

钱谦益在明清两朝均担任过史职,因此他始终以修国史为己任。早在天启初年他参与编纂《神宗实录》时就十分留心相关史料的搜集。他计划编纂一部纪传体《明史》,准备先作长编和事略,后作本纪和列传,并已纂修明史百卷,另编次明代文集百余卷,可惜毁于绛云楼一炬。流传下来的《国初群雄事略》、《太祖实录辨证》两书,在客观保存元明之际的史料及考订史料真伪、弥补前史记载的缺漏、订正前史内容的错误等方面具有重要作用,并颇具特色。钱谦益对元末明初史事的编纂和考证,反映了他实事求是的治史精神。他考证史事,严格遵循言必有据的原则,其考史的成果多被清修《明史》所采纳。他所采用的考史方法对清初乃至乾嘉考据学都产生了一定的影响。

一种用于Java虚拟机的类型化低级语言

为了能够减小运算系统的需信任计算基础、描述较小粒度的安全策略,目前的研究倾向于从程序设计语言和编译器入手来提高软件的安全性·基于以上研究背景设计了一种类型化的低级语言TLL·TLL是一种为Java虚拟机即时编译器设计的类型安全中间语言,以构造一个具有更小需信任计算基础的Java虚拟机系统为目的·TLL的类型系统基于多态的类型化λ演算,它具有丰富的表现力且能够编码各种高级语言的抽象·基于TLL的一个虚拟机原型系统已经实现,它可以作为实现一个高安全且面向多种源语言的运行时系统的起点·

出具证明编译器中代码优化与程序规范转换

出具证明编译器在软件安全研究得到越来越多的关注,是程序验证研究的一个重要方向.但目前关于出具证明编译器的研究主要是在程序逻辑设计和定理自动化证明方面,很少关注编译优化对规范的影响.而编译优化是决定出具证明编译器是否能走向应用的关键因素之一.通过研究数据流优化的基本行为,提出利用数据流分析结果来变换规范的方法,以使原规范的约束准确而充分地施加于优化后的代码,并实现了一个包含多种优化和相应规范转换的编译器原型系统,展示了方法的可行性.