上下文敏感的控制流完整性保护的改进方法

面对控制流劫持攻击的威胁,业界使用控制流完整性保护技术来保障进程的执行安全。传统的控制流完整性验证保护机制依赖于动态二进制改写技术,在分析、实施等过程中难度较大,且有可能带来二进制兼容的问题。通过研究近几年提出的上下文敏感的控制流保护技术PathArmor,分析了其检测进程控制流的时机。然后针对PathArmor只在进程做系统调用时才进行检测的机制,提出了改进的方法。该方法依据内核页错误中断处理机制,通过修改用户页面的保护属性主动触发可执行页面的执行错误;接着,修改页错误中断处理过程,钩挂do_page_fault以处理主动触发的执行错误。用户进程代码和数据的完整性得以保证的同时,得到了更多陷入内核接受检查的机会。在Nginx,bzip2,SQLite等典型应用环境下的实验结果表明,改进的方法能够明显增加系统安全分析的粒度,更好地保护程序的控制流。     

基于LTP的Linux内核测试方法研究

内核作为Linux最关键的部分,其稳定性决定了系统的稳定性.Linux版本升级频繁,应用范围不断扩大,功能不断增强,但层出不穷的补丁程序为内核引入了诸多问题.因此,做好充分的内核测试是确保内核稳定的火键.LinuxTest Project(简称LTP)为测试内核开发了一套测试集,通过自动化测试方法对内核进行有针对性的压力测试,从而验证内核的稳定性、可靠性和健壮性.     

对象驱动的Linux内核crash分类技术研究

Crash(程序崩溃)分析是漏洞挖掘与利用的关键阶段,精准的crash分类是crash分析和漏洞利用的前提.针对现有的Linux内核crash存在大量重复的问题,本文提出一种对象驱动的Linux内核crash分类方法.该方法将内核crash与内核对象的关系建模为二部图结构,从而将crash分类问题转化为内核对象的相似性对比问题.首先,通过对crash执行后向污点分析提取crash相关的内核对象;其次,构造内核对象调用图计算内核与根本原因的相关性度量;最后,基于上述结果构造二部图实现crash相似性比较算法.基于上述方法,本文开发出了Linux内核crash分类的原型系统.通过在真实的数据集上进行实验,验证了系统的有效性和可用性,弥补了现有分类方法粒度较粗,存在误报较多的问题.     

Linux内核调试技术

开发Linux应用时经常需要对Linux内核进行裁剪或修改，由于操作系统内核的特殊性，不能用调试普通用户程序的方法调试内核.该文首先介绍了常用的Linux内核调试方法，分析了其优缺点，然后详细讲解了一种利用KGDB的远程Linux内核调试技术。     

针对内核非控制数据攻击的在线检测方法研究

操作系统安全是计算机系统安全的基础保障和前提条件,而操作系统安全则主要依赖于系统内核的安全。针对内核的非控制数据攻击是指通过篡改内核中的某些关键数据结构,诱发内核出现漏洞和产生一系列稳定性问题,从而严重影响操作系统乃至整个计算机系统的安全。提出一种基于Kprobes内核调试机制和监视器内核线程的在线检测方法,前者用于监控内核关键函数的执行和检查相关动态性数据结构的一致性,后者通过设立专门的内核线程实现静态性内核数据结构的持续监测和不变性验证。然后在Linux平台上运用C语言设计实现了相应的内核非控制数据攻击在线检测器KNCDefender,进行了一系列验证实验和性能测试实验。实验结果表明,该方法是完全轻量级的,并能够及时检测出针对内核的各种非控制数据攻击。     

Linux内核性能诊断分析

Linux由于性能安全上的优势,操作系统的占有率上一直是名列前茅,远远地超过了Unix,Windows的市场占有率.Linux上的应用程序能够快速稳定的运行,这对程序的开发设计有着非常重要的意义,但是Linux从自身的角度来看,即从内核层面上看,它本身也提供了非常多的功能来探测系统,探测系统的瓶颈,从Linux内核函数执行时间的角度看,探测系统硬件尤其是网卡性能之间的对比,TCP协议栈上,得到一个关于重传的时间特征,这将会对Linux上应用程序的故障分析提供了更广阔的思路.     

复杂内核数据结构程序形式化验证

操作系统内核作为软件系统的基础组件, 其安全可靠是构造高可信软件系统的重要环节, 但是, 在实际的验证工作中, 操作系统内核中全局性质的不变式定义, 复杂数据结构程序的形式化描述和验证仍存在很多困难. 本文针对操作系统内核中满足的全局性质, 在代码层以函数为单位, 用全局不变式进行定义, 并在不同的函数中进行形式化验证, 从而证明各个函数符合操作系统内核的全局性质; 针对操作系统内核中经常使用的复杂数据结构程序, 本文通过扩展形状图理论, 提出一种使用嵌套形状图逻辑的方法来形式化描述复杂数据结构程序, 并对该方法进行了正确性证明, 最终成功验证操作系统内核中关于任务创建与调度, 消息队列创建与操作相关的代码.     

Linux 2.6内核的内核对象机制分析

文中介绍了Linux2.6内核中管理设备及其驱动程序的内核对象机制,重点分析了该机制的主要数据结构、工作原理和操作函数。提出了基于嵌入应用时简化目录结构的方法。     

基于多标签的内核配置图及其应用

Linux内核提供了灵活的内核配置项机制,便于针对不同的应用场景进行个性化定制.但内核配置项的数量巨大且增长快速,配置项的默认值在不同内核版本中经常改变,即使专业的内核团队设置配置项也面临很多挑战.针对上述问题,提出基于多标签的内核配置图,该图包含内核配置项间的依赖关系、功能标签、性能标签、安全标签和配置项使能率.此外,该图提供了可视化功能,更加直观、高效、人性化.该内核配置图在内核配置项异常值检测、内核启动优化、内核裁剪、内核安全增强、内核性能优化、内核配置项智能问答等场景均可应用.且将内核配置图应用到检索场景,实现了面向内核配置项的检索框架KCIR(kernel config information retrieval),该框架基于内核配置图对查询语句和内核配置项描述文本进行了扩展,实验评估表明KCIR和传统检索框架相比,检索效果有显著提升,验证了内核配置图在实际应用中的有效性和实用性.     

基于申威架构的PCIe热插拔的实现

PCIe热插拔是服务器实现高可靠性(Reliability)、高可用性(Availability)、高服务性(Serviceabili-ty)(简称RAS特性)的一个重要功能。基于申威3231处理器的PCIe硬件设计,遵循PCIe热插拔协议规范,探索了热插拔技术软硬件接口的实现机制。利用Linux内核PCIe热插拔子系统的软件栈,验证了接口设计的正确性,满足了服务器国产化特殊应用场景的需求。     

Automatic program debugging for intelligent tutoring systems

Program debugging is an important part of the domain expertise required for intelligent tutoring systems that teach programming languages. This article explores the process by which student programs can be automatically debugged in order to increase the instructional capabilities of these systems. The research presented provides a methodology and implementation for the diagnosis and correction of nontrivial recursive programs. In this approach, recursive programs are debugged by repairing induction proofs in the Boyer-Moore logic. The induction proofs constructed and debugged assert the computational équivalence of student programs to correct exemplar solutions. Exemplar solutions not only specify correct implementations but also provide correct code to replace buggy student code. Bugs in student code are repaired with heuristics that attempt to minimize the scope of repair. The automated debugging of student code is greatly complicated by the tremendous variability that arises in student solutions to nontrivial tasks. This variability can be coped with, and debugging performance improved, by explicit reasoning about computational semantics during the debugging process. This article supports these claims by discussing the design, implementation, and evaluation of Talus, an automatic debugger for LISP programs, and by examining related work in automated program debugging. Talus relies on its abilities to reason about computational semantics to perform algorithm recognition, infer code teleology, and to automatically detect and correct nonsyntactic errors in student programs written in a restricted, but nontrivial, subset of LISP. Solutions can vary significantly in algorithm, functional decomposition, role of variables, data flow, control flow, values returned by functions, LISP primitives used, and identifiers used. Solutions can consist of multiple functions, each containing multiple bugs. Empiricial evaluation demonstrates that Talus achieves high performance in debugging widely varying student solutions to challenging tasks.     

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.     

通过抽象程序证明复杂具体程序

本文描述了证明抽象程序和具体程序满足一致性关系的方法.抽象程序使用抽象数据结构（ADTs）如set、list、map及其上的操作.具体程序使用类C语言中的类型.抽象程序和具体程序一致性证明需要用户给出抽象变量和具体变量的关系,抽象程序程序点和具体程序程序点的对应关系.基于对应关系,抽象程序和具体程序一致性证明可以分解,从而容易并可能自动证明.     

超大规模集成电路可调试性设计综述

随着硬件复杂度的不断提高和并行软件调试的需求不断增长,可调试性设计已经成为集成电路设计中的重要内容.一方面,仅靠传统的硅前验证已经无法保证现代超大规模复杂集成电路设计验证的质量,因此作为硅后验证重要支撑技术的可调试性设计日渐成为大规模集成电路设计领域的研究热点.另一方面,并行程序的调试非常困难,很多细微的bug无法直接用传统的单步、断点等方法进行调试,如果没有专门的硬件支持,需要耗费极大的人力和物力.全面分析了现有的可调试性设计,在此基础上归纳总结了可调试性设计技术的主要研究方向并介绍了各个方向的研究进展,深入探讨了可调试性结构设计研究中的热点问题及其产生根源,给出了可调试性结构设计领域的发展趋势.     

基于QBF的循环不变式构造技术

构造循环不变式是程序验证的核心问题之一。主流的循环不变式构造方法通常假设程序中的变量在无限数域上取值,然而程序执行过程中变量都是用有限长度的位向量来表示,无限数域上的循环不变式在有限数域的程序中可能不再是不变式,反之亦然。针对这一问题,本文给出一种基于QBF求解的构造有限数域上循环不变式的方法。该方法可用于构造类型丰富的不变式,包括线性(或多项式)等式(或不等式)不变式,支持加、减、乘、除、移位、位操作等,允许不变式中出现量词。本文也例证了该方法在程序终止性证明、循环上界分析、程序正确性证明等方面的应用价值。     

Using true concurrency to model execution of parallel programs

Parallel execution of a programR (intuitively regarded as a partial order) is usually modeled by sequentially executing one of the total orders (interleavings) into which it can be embedded. Our work deviates from this serialization principle by usingtrue concurrency to model parallel execution. True concurrency is represented via completions ofR tosemi total orders, called time diagrams. These orders are characterized via a set of conditions (denoted byCt), yielding orders or time diagrams which preserve some degree of the intended parallelism inR. Another way to express semi total orders is to use re-writing or derivation rules (denoted byCx) which for any programR generates a set of semi-total orders. This paper includes a classification of parallel execution into three classes according to three different types ofCt conditions. For each class a suitableCx is found and a proof of equivalence between the set of all time diagrams satisfyingCt and the set of all terminalCx derivations ofR is devised. This equivalence between time diagram conditions and derivation rules is used to define a novel notion of correctness for parallel programs. This notion is demonstrated by showing that a specific asynchronous program enforces synchronous execution, which always halts, showing that true concurrency can be useful in the context of parallel program verification.     

PVM并行程序验证系统的原理与实现

本文主要介绍ＰＶＭ并行程序验证系统的基本原理和实现技术。首先,我们扼要分析ＰＶＭ程序的构成与特点,然后阐述验证系统的理论模型和验证算法;最后,讨论开发过程中的若干关键技术,本系统的研制可为产行程序的自动转换和分析验证提供了一个可视化的运行环境。     

程序断言的半自动生成及证明逻辑

如何生成程序断言对于软件验证十分重要。传统方法要求既要对程序结构有深入地把握又要做繁复的Hoare三元式推演工作。为了摆脱这些琐碎事宜,将致力于探讨一种半自动的断言生成方法。为便于理解,讨论主要以XYZ/VERI系统为论述背景。XYZ/VERI 系统是一面向时序逻辑程序语言如XYZ/SE 的类Hoare逻辑交互式验证系统。该工作一定意义上完善了其验证功能。     

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...