一种出具证明编译器中的汇编级断言和证明生成的方法

携带证明代码允许代码消费方通过检查代码生产方提供的证明,来判断代码是否满足相应的安全规范.本文实现了一个类C语言的出具证明编译器原型,它在将带有规范标注的源代码编译成汇编代码的同时,还能产生汇编代码满足相应规范的Coq可检查证明,从而保证汇编代码的安全性.本文设计了一种Hoare风格的汇编级验证框架,并在此框架下提出并实现一种新的自动生成汇编级断言和证明的方法.     

渐进式标记-清扫垃圾收集机制验证

垃圾收集已经成为可靠、高效程序运行平台的一个重要组成部分.渐进式垃圾收集由于在用户程序运行时并行的执行垃圾收集操作,其算法及实现则更为复杂,其可靠性也更难以得到保证.本文论述使用Hoare风格的程序验证框架形式验证渐进式标记-清扫垃圾收集机制及其写拦截器在汇编语言层次上的实现的研究工作.被验证的属性涵括了简单的类型安全到整个内存堆上的数据保持.本文所有的验证工作都实现在Coq辅助定理证明工具中,从而可以迅速的用于构造携带证明的代码包.     

基于提示的移动代码安全检查

基于语言内部安全机制能够有效地保证移动代码的安全执行，其思想是要在移动代码中附加详细且足够的满足安全策略检查的注解信息．基于提示的移动代码的安全检查，克服了目前PCC存在的验证条件必须回送和证明长度过于庞大等缺陷，从而获得了更佳的代码安全检查性能．     

动态存储管理安全验证的Coq实现

随着软件规模和复杂度的日益提升,软件安全的问题变得越来越严峻,同时有越来越多的研究工作集中在高可信软件的开发上 .由于类型系统表达能力的不足,现有的研究不触及底层软件的验证 .由于Hoare逻辑更好的表达能力,采用Hoare逻辑风格的推理,在汇编语言级别,使用Coq形式化与定理证明工具可以实现一个经过安全验证的动态存储管理函数库,这是程序验证技术一次有意义的实践 .实践表明,程序验证技术可以应用到高可信软件的开发上 .     

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

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

一种基于ROP技术的代码混淆方法

针对静动态逆向分析容易获取程序内部核心代码的问题,提出一种基于ROP技术的代码混淆方法。借鉴ROP攻击技术的代码组织和调用方式,利用内存空间随机分布的gadget指令序列执行目标代码的等价功能,实现隐藏目标代码和抵抗逆向分析的目的。从有效性、时间开销和空间开销三个方面评价方法的性能,分析和实验表明,该方法能够有效增加攻击者静动态获取和分析目标代码的难度,具有较好的时间和空间开销性能。     

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

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

一种汇编语言指针逻辑的设计与实现

软件的安全性日益重要,软件满足安全策略的证明方法成为一个研究热点.而指针程序的安全性质证明是难点之一.根据已经提出的安全程序设计与证明的框架以及PointerC指针逻辑,提出一种汇编语言指针逻辑.该逻辑解决了Hoare逻辑处理别名问题面临的困难,保证通过验证的汇编指针程序不存在空指针引用和内存泄露等安全问题.此逻辑的可靠性证明已在证明辅助工具Coq中完成.此外,本文还实现一个原型系统,并使用该系统对链表、二叉树等非平凡的指针程序的进行了自动的安全验证.     

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

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

编写安全的代码

不可否认,我确实抱着怀疑的态度去接触这个题目。虽然它得到了比尔·盖茨的大力推荐,虽然它被誉为“未来‘高信度软件’之惟一必读”,虽然它得到了各界的广泛赞誉,但这确实是一个非常崭新的话题,于是我带着这种将信将疑的态度读完了全书。     

Interactive and Probabilistic Proof of Mobile Code Safety

This paper proposes a new proof-based approach to safe evolution of distributed software systems. Specifically, it extends the simple certification mechanism of proof-carrying code (PCC) to make it interactive and probabilistic, thereby devising interactive proof-carrying code (iPCC). With iPCC, a code consumer is convinced, with overwhelming probability, of the existence and validity of a safety proof of a transmitted code through interaction with a code producer. The iPCC mechanism theoretically solves the problem of proof explosion with PCC and can be used to efficiently prove a greater variety of safety properties that may require longer proofs. Technically, the class (PSPACE) of safety properties that are efficiently provable by iPCC is larger than the class (NP) efficiently provable by PCC. To illustrate the power of iPCC, this paper demonstrates that the verification of certain basic safety properties of typical machine instruction codes needs co-NP-complete computation, and shows how these safety properties can be efficiently verified by the iPCC mechanism.This is an extended and revised version of Tsukada (2001a), which appeared in the Proceedings of the 2000 International Symposium on Principles of Software Evolution. A preliminary version was also presented at the International Conference on Advances in Infrastructure for Electronic Business, Science, and Education on the Internet (Tsukada, 2001b).     

Certifying Compilation and Run-Time Code Generation

A certifying compiler takes a source language program and produces object code, as well as a certificate that can be used to verify that the object code satisfies desirable properties, such as type safety and memory safety. Certifying compilation helps to increase both compiler robustness and program safety. Compiler robustness is improved since some compiler errors can be caught by checking the object code against the certificate immediately after compilation. Program safety is improved because the object code and certificate alone are sufficient to establish safety: even if the object code and certificate are produced on an unknown machine by an unknown compiler and sent over an untrusted network, safe execution is guaranteed as long as the code and certificate pass the verifier.Existing work in certifying compilation has addressed statically generated code. In this paper, we extend this to code generated at run time. Our goal is to combine certifying compilation with run-time code generation to produce programs that are both fast and verifiably safe. To achieve this goal, we present two new languages with explicit run-time code generation constructs: Cyclone, a type safe dialect of C, and TAL/T, a type safe assembly language. We have designed and implemented a system that translates a safe C program into Cyclone, which is then compiled to TAL/T, and finally assembled into executable object code. This paper focuses on our overall approach and the front end of our system; details about TAL/T will appear in a subsequent paper.     

Garbage Collector Verification for Proof-Carrying Code

We present the verification of the machine-level implementation of a conservative variant of the standard mark- sweep garbage collector in a Hoare-style program logic.The specification of the collector is given on a machine-level memory model using separation logic,and is strong enough to preserve the safety property of any common mutator program.Our verification is fully implemented in the Coq proof assistant and can be packed immediately as foundational proof-carrying code package.Our work makes important attempt toward building fully certified production-quality garbage collectors.     

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

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

Certifying Concurrent Programs Using Transactional Memory

Transactional memory (TM) is a new promising concurrency-control mechanism that can avoid many of the pitfalls of the traditional lock-based techniques. TM systems handle data races between threads automatically so that programmers do not have to reason about the interaction of threads manually. TM provides a programming model that may make the development of multi-threaded programs easier. Much work has been done to explore the various implementation strategies of TM systems and to achieve better perfor...     

一种基于指针逻辑的代码安全属性分析方法

在分析和总结前人工作的基础上,提出了一种改进的代码安全属性验证方法.该方法在利用传统的源代码安全属性验证工具的基础上,加入了指针逻辑,针对现有代码属性分析技术只能对C语言子集进行分析验证的不足,利用指针逻辑对源代码的分析结果对源代码中的指针进行替换,从而避开了传统静态代码属性验证工具对指针处理功能太弱的瓶颈,可以实现对C语言中的部分指针及运算进行处理.     

一种基于图数据库的代码结构解析与搜索方法

软件复用是在软件开发中避免重复劳动的解决方案.在复用一个已有的软件项目时,软件开发人员通常需要理解某些代码元素以及其间的关联关系,称之为代码结构.软件开发人员一般通过浏览软件源代码的方式理解代码结构.由于源代码往往规模较大且结构复杂,理解代码结构通常会耗费大量的时间与精力.因此,将软件开发人员想要理解的代码结构自动、清晰地展示出来是很有帮助的.提出一种基于图数据库的代码结构解析与搜索方法以实现这一目的.这一方法可对软件的代码结构进行解析,并在图数据库中对其进行有效的组织和管理.搜索时,软件开发人员输入自然语言查询语句,该方法中的搜索机制会分析查询语句,并从图数据库中截取出与其相对应的代码结构进行展示.该方法具有高度的可扩展性：不同粒度的结点与多样化的关联关系可以容易地存储进图数据库中,且面向不同搜索目的的代码结构搜索算法亦可以容易地集成进搜索机制中.这一方法已在相应的工具中得到了实现,其有效性在一个商业案例研究中得到了验证.     

Bytecode Analysis for Proof Carrying Code

Out of annotated programs proof carrying code systems construct and prove verification conditions that guarantee a given safety policy. The annotations may come from various program analyzers and must not be trusted as they need to be verified. A generic verification condition generator can be utilized such that a combination of annotations is verified incrementally. New annotations may be verified by using previously verified ones as trusted facts. We show how results from a trusted type analyzer may be combined with untrusted interval analysis to automatically verify that bytecode programs do not overflow. All trusted components are formalized and verified in Isabelle/HOL.