基于类型化内存地址的安全策略的设计与实现

提出了一种检查代码安全的类型安全策略，详细描述了该策略的逻辑表示、形式化描述和基于该策略的证明方法，最后给出一个基于该策略的定理证明器HBTSTP．策略的核心思想是给每个合法的内存地址赋予类型，使用符号表达式记录内存的状态变化，对于需要读写内存的指令，调用证明器进行类型检查，查看目标地址是否符合类型安全来确定该读写操作是否安全．     

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

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

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

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

一种用于Java程序验证编译的标签类型

在基于语言考虑代码安全性的工作中,往往需要将高级语言程序翻译成类型化低级语言的程序进行类型检查.许多高级语言具有类型调度结构,在向低级语言的编译过程中需要用标签机制来实现.针对具有多继承接口的Java程序包含的一种特殊的类型调度结构,提出了一种新的标签类型.包含这种标签类型的低级语言能够有效地实现Java程序中的接口调用.这种对接口调用的编译方法被用在一个以类型化低级语言为验证语言的Java字节码即时编译器中.     

Win32汇编语言程序设计

Windows环境下,Win32汇编语言是一种功能强大的编程语言,用它能够开发出大型的软件.本文简单地介绍了Win32汇编语言程序设计方法和使用Visual C 6.0编译Win32汇编语言程序的步骤.     

安全类型系统在编译技术中的应用研究

类型系统是一种设计和研究程序设计语言的形式化方法和工具。本文提出了一种新的用安全类型系统增强编译程序安全性的方法;给出了类型系统的形式化定义,引入了安全类型和安全类型系统的概念,并给出了安全类型系统的子类型规则和安全类型规则;最后讨论了安全类型系统在编译技术中的应用。     

分布式计算系统信息流安全

程序信息流安全是信息安全的一个重要研究方向.基于类型的静态分析可以保证程序信息流安全.鉴于分布式移动计算系统中进程之间的通讯会引起严重的信息泄密,本文研究了进程之间的通讯对系统信息流安全的影响,通过对高阶函数式编程语言进行扩充,加入通讯原语,得到分布式移动计算语言ConcurML,它能很好地模拟网络连接的动态性和代码移动性.并给出了动态语义和静态语义的形式描述,所设计的两级信息流类型系统使用类型和效果技术,结合了多态这样的类型特征,能有效地保证进程之间的通讯不会导致信息泄密.     

用汇编语言测量任意程序的运行时间

用汇编语言编写的程序代码少,执行时间短,本文介绍的方法用汇编语言测量程序的运行时间是评价算法的时间复杂度的一种依据,是测试软件可靠性的重要因素之一。给出了用汇编语言实现的源程序。     

计算机程序设计中C#和汇编语言混合程序设计研究

C#和汇编语言被广泛地应用于计算机各类软件的编程中,是两种具有不同特征的编程语言.在计算机程序设计中,C#和汇编语言混合编程,通过发挥各自的优势,实现两种语言之间的转化,可以提升软件运行效率,实现两种语言共通.主要对计算机程序设计中C#和汇编语言混合程序设计进行了研究,希望能够为计算机程序设计提供一些帮助.     

汇编语言与C语言的混合程序设计技术研究

C语言和汇编语言是应用在计算机程序设计中两类具有不同特征的编程语言.在实际的软件开发中,C语言固然有汇编语言所不具备的优越性能,但是当具有对硬件直接的操作或提高软件稳定性等需求时,往往采用这两类语言的混合编程的方式.基于对汇编语言与C语言设计方法的介绍,阐述了3种汇编语言与C语言混合编程的方式,并对这两种编程语言混合编程所存在的关键性问题进行了分析.     

Verifying Termination and Reduction Properties about Higher-Order Logic Programs

We describe two checkers for verifying termination and reduction properties about higher-order logic programs. The reduction checker verifies that the result of a program execution is structurally smaller than (or equal to) the inputs to the program. The termination checker guarantees that the inputs of the recursive calls are structurally smaller than the inputs of the original call, taking into account reduction properties. At the heart of both checkers lies an inference system to reason about structural properties, which are described by higher-order subterm relations. This approach provides a logical foundation for proving properties such as termination and reduction and factors the effort required for each one of them. Moreover, it allows the study of proof-theoretical properties, soundness, and completeness and different optimizations. The termination and reduction checker are implemented as part of the Twelf system and have been used on a wide variety of examples, including proofs about typed assembly language and those in the area of proof-carrying code.     

A Syntactic Approach to Foundational Proof-Carrying Code

Proof-carrying code (PCC) is a general framework for verifying the safety properties of machine-language programs. PCC proofs are usually written in a logic extended with language-specific typing rules; they certify safety but only if there is no bug in the typing rules. In foundational proof-carrying code (FPCC), on the other hand, proofs are constructed and verified by using strictly the foundations of mathematical logic, with no type-specific axioms. FPCC is more flexible and secure because it is not tied to any particular type system and it has a smaller trusted base. Foundational proofs, however, are much harder to construct. Previous efforts on FPCC all required building sophisticated semantic models for types. Furthermore, none of them can be easily extended to support mutable fields and recursive types. In this article, we present a syntactic approach to FPCC that avoids all of these difficulties. Under our new scheme, the foundational proof for a typed machine program simply consists of the typing derivation plus the formalized syntactic soundness proof for the underlying type system. The former can be readily obtained from a type-checker, while the latter is known to be much easier to construct than the semantic soundness proofs. We give a translation from a typed assembly language into FPCC and demonstrate the advantages of our new system through an implementation in the Coq proof assistant.     

Type inference and strong static type checking for Promela

The Spin model checker and its specification language Promela have been used extensively in industry and academia to check the logical properties of distributed algorithms and protocols. Model checking with Spin involves reasoning about a system via an abstract Promela specification, thus the technique depends critically on the soundness of this specification. Promela includes a rich set of data types including first-class channels, but the language syntax restricts the declaration of channel types so that it is not generally possible to deduce the complete type of a channel directly from its declaration. We present the design and implementation of Etch, an enhanced type checker for Promela, which uses constraint-based type inference to perform strong type checking of Promela specifications, allowing static detection of errors that Spin would not detect until simulation/verification time, or that Spin may miss completely. We discuss theoretical and practical problems associated with designing a type system and type checker for an existing language, and formalise our approach using a Promela-like calculus. To handle subtyping between base types, we present an extension to a standard unification algorithm to solve a system of equality and subtyping constraints, based on bounded substitutions.     

Syntactic Type Soundness Results for the Region Calculus

The region calculus of Tofte and Talpin is a polymorphically typed lambda calculus with annotations that make memory allocation and deallocation explicit. It is intended as an intermediate language for implementing Hindley-Milner typed functional languages such as ML without traditional trace-based garbage collection. Static region and effect inference can be used to annotate a statically typed ML program with memory management primitives. Soundness of the calculus with respect to the region and effect system is crucial to guarantee safe deallocation of regions, i.e., deallocation should only take place for objects which are provably dead. The original soundness proof by Tofte and Talpin requires a complex co-inductive safety relation. In this paper, we present two small-step operational semantics for the region calculus and prove their type soundness with respect to the region and effect system. Following the standard syntactic approach of Wright, Felleisen, and Harper, we obtain simple inductive proofs. The first semantics is store-less. It is simple and elegant and gives rise to perspicuous proofs. The second semantics provides a store-based model for the region calculus. Albeit slightly more complicated, its additional expressiveness allows us to model operations on references with destructive update. A pure fragment of both small-step semantics is then proven equivalent to the original big-step operational approach of Tofte and Talpin. This leads to an alternative soundness proof for their evaluation-style formulation.     

Heap-Bounded Assembly Language

We present a first-order linearly typed assembly language, HBAL, that allows the safe reuse of heap space for elements of different types. Linear typing ensures the single pointer property, disallowing aliasing but allowing safe, in-place-update compilation of programming languages. We prove that HBAL is sound for a low-level untyped model of the machine, using a satisfiability relation that captures when a location correctly models a value of some type. This interpretation is closer to the machine than previous abstract machines used for typed assembly language models, and we separate typing of the store from an untyped operational semantics of programs, as would be required for proof-carrying code. Our ultimate aim is to design a family of assembly languages that have high-level typing features for expressing resource-bound constraints. We want to link the assembly-level with high-level languages expressing similar constraints, to provide end-to-end guarantees and a viable framework for proof-carrying code. HBAL is a first exemplifying step in this direction. It is designed as a target low-level language for Hofmann's LFPL language. Programs written in LFPL run in a bounded amount of heap space, and this property carries over when they are compiled to HBAL: the resulting program does not allocate store or assume an external garbage collector. Following LFPL, we include a special diamond resource type that stands for a unit of heap space of uncommitted type.     

Specification and verification of object-oriented programs using supertype abstraction

We present a formal specification language and a formal verification logic for a simple object-oriented programming language. The language is applicative and statically typed, and supports subtyping and message-passing. The verification logic relies on a behavioral notion of subtyping that captures the intuition that a subtype behaves like its supertypes. We give a formal definition for legal subtype relations, based on the specified behavior of objects, and show that this definition is sufficient to ensure the soundness of the verification logic. The verification logic reflects the way programmers reason informally about object-oriented programs, in that it allows them to use static type information, which avoids the need to consider all possible run-time subtypes.The work of both authors was supported in part by the National Science Foundation under Grant CCR-8716884, and in part by the Defense Advanced Research Projects Agency (DARPA) under Contract N00014-89-J-1988. While a graduate student at MIT, Leavens was also supported in part by a GenRad/AEA Faculty Development Fellowship, and at ISU he has been partially supported by the ISU Achievement Foundation and by the National Science Foundation under Grant CCR-9108654     

汇编语言与C语言的混合程序设计技术

讨论汇编语言与C语言的混合程序设计技术。在大规模的程序设计中,汇编语言程序与高级语言程序相结合,充分发挥各自的优点,实现两种语言之间的混合编程,是解决实际问题的有效方法。在实际的程序设计中,C语言主程序可以调用汇编语言子程序,汇编语言主程序可以调用C语言子程序,也可以在C语言程序中嵌入汇编语言语句。在汇编语言与C语言的混合编程中,参数的传递、模块的连接以及调用关系的确定是值得注意的关键问题。     

A Formally Verified Compiler Back-end

This article describes the development and formal verification (proof of semantic preservation) of a compiler back-end from Cminor (a simple imperative intermediate language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its soundness. Such a verified compiler is useful in the context of formal methods applied to the certification of critical software: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.     

Bisimilarity for the Region Calculus

A region calculus is a programming language calculus with explicit instrumentation for memory management. Every value is annotated with a region in which it is stored and regions are allocated and deallocated in a stack-like fashion. The annotations can be statically inferred by a type and effect system, making a region calculus suitable as an intermediate language for a compiler of statically typed programming languages.Although a lot of attention has been paid to type soundness properties of different flavors of region calculi, it seems that little effort has been made to develop a semantic framework. In this paper, we present a theory based on bisimulation, which serves as a coinductive proof principle for showing equivalences of polymorphically region-annotated terms. Our notion of bisimilarity is reminiscent of open bisimilarity for the -calculus and we prove it sound and complete with respect to Morris-style contextual equivalence.As an application, we formulate a syntactic equational theory, which is used elsewhere to prove the soundness of a specializer based on region inference. We use our bisimulation framework to show that the equational theory is sound with respect to contextual equivalence.