检索结果-内蒙古大学图书馆

Garbage Collector Verification for proof-carrying code

Journal of Computer Science & Technology 2007年第3期22卷 426-437页

作者：林春晓陈意云李隆华蓓 Department of Computer Science and Technology University of Science and Technology of China

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.

关键词： program verification garbage collector proof-carrying code program safety

来源：评论

学校读者我要写书评

暂无评论

A portable virtual machine target for proof-carrying code

引用

SCIENCE OF COMPUTER PROGRAMMING 2005年第3期57卷 275-294页

作者： Franz, M Chandra, D Gal, A Haldar, V Probst, CW Reig, F Wang, N Univ Calif Irvine Donald Bren Sch Informat & Comp Sci Irvine CA 92697 USA Univ Nottingham Sch Comp Sci Nottingham NG7 2RD England

Virtual machines and proof-carrying code provide two techniques that have been used independently to provide safety for mobile code. Both these techniques have strengths and limitations. Existing virtual machines, such as the Java VM, have several drawbacks. First, the effort required for safety verification is considerable. Second, and more subtly, the need to provide such verification by the code consumer inhibits the amount of optimization that can be performed by the code producer. This in turn makes just-in-time compilation surprisingly expensive. proof-carrying code, on the other hand, has its own set of limitations, among which are the size of proofs and the fact that the certified code is no longer machine independent. By combining the two techniques, we are able to overcome these limitations. Our hybrid safe-code solution uses a virtual machine that has been designed specifically to support proof-carrying code, while simultaneously providing efficient just-in-time compilation and target-machine independence. In particular, our approach reduces the complexity of the required proofs, resulting in fewer proof obligations that need to be discharged at the target machine. (c) 2005 Elsevier B.V. All rights reserved.

关键词： virtual machines proof-carrying code safe mobile code dynamic (just-in-time) compilation

来源：评论

学校读者我要写书评

暂无评论

A proof-carrying code Approach to Certificate Auction Mechanisms 1

引用

10th International Symposium on Formal Aspects of Component Software (FACS)

作者： Bai, W. Tadjouddine, E. M. Payne, T. R. Guan, S. U. Univ Liverpool Dept Comp Sci Liverpool L69 3BX Merseyside England Xian Jiaotong Liverpool Univ Dept Comp Sci & Software Engn Suzhou Peoples R China

ISBN: (数字)9783319076027

ISBN: (纸本)9783319076027;9783319076010

Whilst it can be highly desirable for software agents to engage in auctions, they are normally restricted to trading within known auctions, due to the complexity and heterogeneity of the auction rules within an e-commerce system. To allow for agents to deal with previously unseen protocols, we present a proof-carrying code approach using COQ wherein auction protocols can be specified and desirable properties be proven. This enables software agents to automatically certify claimed auction properties and assist them in their decision-making. We have illustrated our approach by specifying both the English and Vickrey auctions;have formalized different bidding strategies for agents;have certified that up to the valuation is the optimal strategy in English auction and truthful bidding is the optimal strategy in Vickrey auction for all agents. The formalization and certification are based on inductive definitions and constructions from within COQ. This work contributes to solving the problem of open societies of software agents moving between different institutions and seeking to make optimal decisions and will benefit those engaged in agent-mediated e-commerce.

关键词： Coq proof-carrying code Certification e-commerce Software agents

来源：评论

学校读者我要写书评

暂无评论

Integrating a Certified Memory Management Runtime with proof-carrying code 07

Integrating a Certified Memory Management Runtime with Proof...

引用

22nd ACM Symposium on Applied Computing

作者： Hamid, Nadeem Abdul Berry Coll Mt Berry GA 30149 USA

ISBN: (纸本)9781595934802

Software systems today axe built from collections of interacting components written in different languages at varying levels of abstraction from the machine hardware. The ability to integrate certified components from different levels of a software architecture is a necessary part of the process of developing a dependable and secure computing infrastructure. In this paper we present a prototype system in the context of proof-carrying code that allows for the integration of safety proofs derived from a high-level type system with a certified, low-level memory management runtime library.

关键词： proof-carrying code certified memory management

来源：评论

学校读者我要写书评

暂无评论

A portable virtual machine target for proof-carrying code

A portable virtual machine target for proof-carrying code

引用

1st Workshop on Interpreters, Virtual Machines and Emulators (IVME 03)

关键词： virtual machines proof-carrying code safe mobile code dynamic (just-in-time) compilation

来源：评论

学校读者我要写书评

暂无评论

The Weird Machines in proof-carrying code

The Weird Machines in Proof-Carrying Code

引用

35th IEEE-Computer-Society Workshop on Security and Privacy (SP)

作者： Vanegue, Julien Bloomberg LP New York NY 10022 USA

ISBN: (纸本)9781479951031

We review different attack vectors on proof-carrying code (PCC) related to policy, memory model, machine abstraction, and formal system. We capture the notion of weird machines in PCC to formalize the shadow execution arising in programs when their proofs do not sufficiently capture and disallow the execution of untrusted computations. We suggest a few ideas to improve existing PCC systems so they are more resilient to memory attacks.

关键词： codes security of data PCC systems formal system machine abstraction memory attacks memory model proof-carrying code untrusted computations weird machines Abstracts Computational modeling Program processors Registers Safety Security Semantics FPCC Machines PCC Weird PRIMARY COMPONENT COOLING 1-piperidinocyclohexanecarbonitrile machine Program processors machinery Data Security Registers Computational modeling Semantics codes Consumer safety safety semiotics Security

来源：评论

学校读者我要写书评

暂无评论

Probabilistic proof-carrying code

Probabilistic Proof-carrying Code

引用

作者： Sharkey, Michael Ian Uottawa

学位级别：master

proof-carrying code is an application of software verification techniques to the problem of ensuring the safety of mobile code. However, previous proof-carrying code systems have assumed that mobile code will faithfully execute the instructions of the program. Realistic implementations of computing systems are susceptible to probabilistic behaviours that can alter the execution of a program in ways that can result in corruption or security breaches. We investigate the use of a probabilistic bytecode language to model deterministic programs that are executed on probabilistic computing systems. To model probabilistic safety properties, a probabilistic logic is adapted to out bytecode instruction language, and soundness is proven. A sketch of a completeness proof of the logic is also shown

关键词： proof-carrying code Lua verification

来源：评论

学校读者我要写书评

暂无评论

Certificate size reduction in abstraction-carrying code

引用

THEORY AND PRACTICE OF LOGIC PROGRAMMING 2012年第3期12卷 283-318页

作者： Albert, Elvira Arenas, Puri Puebla, German Hermenegildo, Manuel Univ Complutense Madrid Sch Comp Sci E-28040 Madrid Spain Tech Univ Madrid Sch Comp Sci E-28660 Madrid Spain Madrid Inst Adv Studies Software Dev Technol IMDE Madrid Spain

carrying code (ACC) has recently been proposed as a framework for mobile code safety in which the code supplier provides a program together with an abstraction (or abstract model of the program) whose validity entails compliance with a predefined safety policy. The abstraction plays thus the role of safety certificate and its generation is carried out automatically by a fixpoint analyzer. The advantage of providing a (fixpoint) abstraction to the code consumer is that its validity is checked in a single pass (i.e., one iteration) of an abstract interpretation-based checker. A main challenge to make ACC useful in practice is to reduce the size of certificates as much as possible while at the same time not increasing checking time. The intuitive idea is to only include in the certificate information that the checker is unable to reproduce without iterating. We introduce the notion of reduced certificate which characterizes the subset of the abstraction which a checker needs in order to validate (and re-construct) the full certificate in a single pass. Based on this notion, we instrument a generic analysis algorithm with the necessary extensions in order to identify the information relevant to the checker. Interestingly, the fact that the reduced certificate omits (parts of) the abstraction has implications in the design of the checker. We provide the sufficient conditions which allow us to ensure that (1) if the checker succeeds in validating the certificate, then the certificate is valid for the program (correctness) and (2) the checker will succeed for any reduced certificate which is valid (completeness). Our approach has been implemented and benchmarked within the CiaoPP system. The experimental results show that our proposal is able to greatly reduce the size of certificates in practice.

关键词： proof-carrying code abstraction-carrying code static analysis reduced certificates mobile code

来源：评论

学校读者我要写书评

暂无评论

Automated techniques for provably safe mobile code

引用

THEORETICAL COMPUTER SCIENCE 2003年第2期290卷 1175-1199页

作者： Colby, C Crary, K Harper, R Lee, P Pfenning, F Carnegie Mellon Univ Dept Comp Sci Pittsburgh PA 15213 USA Inksomi Corp San Francisco CA 94105 USA

We present a general framework for provably safe mobile code. It relies on a formal definition of a safety policy and explicit evidence for compliance with this policy which is attached to a binary. Concrete realizations of this framework are proof-carrying code, where the evidence for safety is a formal proof generated by a certifying compiler, and typed assembly language, where the evidence for safety is given via type annotations propagated throughout the compilation process in typed intermediate languages. Validity of the evidence is established via a small trusted type checker, either directly on the binary or indirectly on proof representations in a logical framework. (C) 2002 Elsevier Science B.V. All rights reserved.

关键词： type systems type safety certifying compilers typed assembly language proof-carrying code

来源：评论

学校读者我要写书评

暂无评论

Modular verification of concurrent assembly code with dynamic thread creation and termination 05

Modular verification of concurrent assembly code with dynami...

引用

10th ACM SIGPLAN International Conference on Functional Programming (ICFP)

作者： Feng, XY Shao, Z Yale Univ Dept Comp Sci New Haven CT 06520 USA

ISBN: (纸本)9781595930644

proof-carrying code (PCC) is a general framework that can, in principle, verify safety properties of arbitrary machine-language programs. Existing PCC systems and typed assembly languages, however, can only handle sequential programs. This severely limits their applicability since many real-world systems use some form of concurrency in their core software. Recently Yu and Shao proposed a logic-based "type" system for verifying concurrent assembly programs. Their thread model, however, is rather restrictive in that no threads can be created or terminated dynamically and no sharing of code is allowed between threads. In this paper, we present a new formal framework for verifying general multi-threaded assembly code with unbounded dynamic thread creation and termination as well as sharing of code between threads. We adapt and generalize the rely-guarantee methodology to the assembly level and show how to specify the semantics of thread "fork" with argument passing. In particular, we allow threads to have different assumptions and guarantees at different stages of their lifetime so they can coexist with the dynamically changing thread environment. Our work provides a foundation for certifying realistic multi-threaded programs and makes an important advance toward generating proofcarrying concurrent code.

关键词： concurrency verification proof-carrying code rely-guarantee dynamic thread creation

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：