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

Bytecode Analysis for proof carrying code

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2005年第1期141卷 19-34页

作者： Wildmoser, Martin Chaieb, Amine Nipkow, Tobias Tech Univ Munich Inst Informat Munich Germany

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.

关键词： proof carrying code bytecode safety policy type analyzer Isabelle/HOL

来源：评论

学校读者我要写书评

暂无评论

Assurance carrying code for Software Supply Chain 32

Assurance Carrying Code for Software Supply Chain

引用

32nd IEEE International Symposium on Software Reliability Engineering (ISSRE)

作者： Matsuno, Yutaka Yamagata, Yoriyuki Nishihara, Hideaki Hosokawa, Yuichiro Nihon Univ Coll Sci & Technol Tokyo Japan Natl Inst Adv Ind Sci & Technol Cyber Phys Secur Res Ctr Tokyo Japan Gunma Prefectural Womens Univ Dept Liberal Arts Tamamura Gunma Japan

ISBN: (纸本)9781665426039

Modern software systems are composed of software components supplied by a software supply chain, and it has become difficult to maintain the dependability of the software supply chain. To address this problem, we introduce assurance carrying code, a framework in which every software component in a software supply chain has its own assurance case. When integrating a software component into a supply chain, the stakeholders check (manually or automatically) the assurance case to determine whether or not the software component is dependable for the supply chain. We introduce a pattern language for Goal Structuring Notation (GSN) formalized by lambda-calculus, which is used in a theory of functional programming languages theory.

关键词： assurance cases proof carrying code formal languages lambda -calculus

来源：评论

学校读者我要写书评

暂无评论

Silver Bullet Talks with Greg Morrisett

引用

IEEE SECURITY & PRIVACY 2010年第5期8卷 6-9页

作者： Mcgraw, Gary Cigital

Gary McGraw interviews Greg Morrisett, the Allen B. Cutting Professor of Computer Science and associate dean for computer science and engineering at Harvard University. His current work is on applications of advanced type systems, model checkers, proof-carrying code, and inline reference monitors for building efficient and provably secure systems. He's also working on languages for sensor networks. Hear the full podcast of the interview at ***/security/podcasts/ or ***/silverbullet/. The Web extra is the full transcript of the interview.

关键词： Gary Mc Graw Greg Morrisett Advanced Type Systems Model Checkers proof carrying code Inline Reference Monitors

来源：评论

学校读者我要写书评

暂无评论

Programs from proofs of Predicated Dataflow Analyses 15

Programs from Proofs of Predicated Dataflow Analyses

引用

30th ACM Symposium on Applied Computing (SAC)

作者： Jakobs, Marie-Christine Wehrheim, Heike Univ Paderborn Dept Comp Sci Paderborn Germany

ISBN: (纸本)9781450331968

"Programs from proofs" is a generic method which generates new programs out of correctness proofs of given programs. The technique ensures that the new and given program are behaviorally equivalent and that the new program is easily verifiable, thus serving as an alternative to proof-carrying code concepts. So far, this generic method has one instantiation that verifies type-state properties of programs. In this paper, we present a whole range of new instantiations, all based on dataflow analyses. More precisely, we show how an imprecise but fast dataflow analysis can be enhanced with a predicate analysis as to yield a precise but expensive analysis. Out of the safety proofs of this analysis, we generate new programs, again behaviorally equivalent to the given ones, which are "easily verifiable" in the sense that now the dataflow analysis alone can yield precise results. An experimental evaluation practically supports our claim of easy verification.

关键词： Programs from proofs proof carrying code Verification Program transformation

来源：评论

学校读者我要写书评

暂无评论

cardT^AP:: Automated deduction on a smart card 11th

card<i>T<SUP>A</SUP>P</i>:: Automated deduction on a smart c...

引用

11th Australian Joint Conference on Artificial Intelligence (AI 98)

作者： Slater, A Goré, R Posegga, J Vogt, H Australian Natl Univ Automated Reasoning Project Canberra ACT 0200 Australia Australian Natl Univ Dept Comp Sci Canberra ACT 0200 Australia Deutsch Telekom AG Technolzentrum IT Secur D-64307 Darmstadt Germany

ISBN: (纸本)3540651381

We present the first implementation of a theorem prover which runs on a smart card. The prover is written in Java and implements a dual tableau calculus.(1) Due to the limited resources available on current smart cards, the prover is restricted to propositional classical logic. It can be easily extended to full first-order logic. The potential applications for our prover lie within the context of security related functions based on trusted devices such as smart cards.

关键词： automated deduction tableaux leanTAP security java proof carrying code

来源：评论

学校读者我要写书评

暂无评论

A security framework for executables in a ubiquitous computing environment

A security framework for executables in a ubiquitous computi...

引用

IEEE Global Telecommunications Conference (GLOBECOM 04)

作者： Llewellyn-Jones, D Merabti, M Shi, Q Askwith, B Liverpool John Moores Univ Sch Comp & Math Sci Liverpool L3 3AF Merseyside England

ISBN: (纸本)0780387945

The vision of ubiquitous computing presents us with unique difficulties in terms of maintaining security. Many of these relate to privacy or quality of service issues, but underpinning these are the requirement for secure execution of code. We present a novel framework for utilising a hybrid method of code analysis combined with component composition techniques. The aim has been to allow sandboxing techniques to maintain security dynamically in a ubiquitous computing environment. We argue that whilst security issues for ubiquitous computing are particularly acute, characteristics of the environment can also be harnessed advantageously to fulfil these security requirements.

关键词： security ubiquitous computing pervasive computing network security component composition direct code analysis proof carrying code certification sandbox

来源：评论

学校读者我要写书评

暂无评论

Enforceable Security Policies

引用

ACM Transactions on Information and System Security 2000年第1期3卷 30-50页

作者： Schneider, Fred B. Cornell University Ithaca NY Upson Hall United States

A precise characterization is given for the class of security policies enforceable with mechanisms that work by monitoring system execution, and automata are introduced for specifying exactly that class of security policies. Techniques to enforce security policies specified by such automata are also discussed. © 2000, ACM. All rights reserved.

关键词： EM security policies inlined reference monitors proof carrying code safety properties SASI Security security automata security policies

来源：评论

学校读者我要写书评

暂无评论

Memory Requirements of Java Bytecode Verification on Limited Devices

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2005年第1期132卷 95-111页

作者： Klohs, Karsten Kastens, Uwe Univ Paderborn Dept Comp Sci Paderborn Germany

Bytecode verification forms the corner stone of the Java security model that ensures the integrity of the runtime environment even in the presence of untrusted code. Limited devices, like Java smart cards, lack the necessary amount of memory to verify the type-safety of Java bytecode on their own. proof carrying code techniques compute, outside the device, tamper-proof certificates which simplify bytecode verification and pass them along with the code. Rose has developed such an approach for a small subset of the Java bytecode language. In this paper, we extend this approach to real world Java software and develop a precise model of the memory requirements on the device. We use a variant of interval graphs to model liveness of memory regions in the checking step. Based on this model, memory-optimal checking strategies are computed outside the device and attached to the certificate. The underlying type system of the bytecode verifier has been augmented with multi-dimensional arrays and recognizes references to uninitialized Java objects. Our detailed measurements, based on real world Java libraries, demonstrate that the approach offers a substantial improvement in size of certificate over the similar approach taken by the KVM verifier. Worst case memory consumption on the device is examined as well and it turns out that the refinements based on our model save a significant amount of memory.

关键词： proof carrying code Bytecode Verification Limited Devices Java Card

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：