AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
Our goal is to reduce the size of the trusted computing base of systems that run machine code from untrusted sources

Foundational Proof-Carrying Code

Boston, MA, pp.247-256, (2003)

Cited by: 430|Views144
EI WOS

Abstract

Abstract: Proof-carrying code is a framework for the mechanical verification of safety properties of machine language programs, but the problem arises of quis custodiat ip-sos custodes-who will verify the verifier itself? Foundational proof-carrying code is verification from the smallest possible set of axioms, using the simplest possible...More

Code:

Data:

Introduction
  • When you obtain a piece of software – a shrinkwrapped application, a browser plugin, an applet, an OS kernel extension – you might like to ascertain that it’s safe to execute: it accesses only its own memory and respects the private variables of the API to which it’s linked.
  • If a compiler can produce Typed Assembly Language (TAL) [14], just by type-checking the low-level representation of the program the authors can guarantee safety – but only if there’s no bug in the typing rules, or in the typechecker, or in the assembler that translates TAL to machine language
  • These components are significantly smaller and simpler than a Java JIT and JVM.
  • Proof-carrying code (PCC) [15] constructs and verifies a mathematical proof about the machine-language program itself, and this guarantees safety – but only if there’s no bug in the verification-condition generator, or in the logical axioms, or the typing rules, or the proof-checker.
Highlights
  • When you obtain a piece of software – a shrinkwrapped application, a browser plugin, an applet, an OS kernel extension – you might like to ascertain that it’s safe to execute: it accesses only its own memory and respects the private variables of the API to which it’s linked
  • Since our approach to Proof-carrying code shifts most of the work to the human prover of static, machine-checkable lemmas about the programming language’s type system, we find it imperative to use the same software engineering practices in implementing proofs as are used in building any large system
  • Our goal is to reduce the size of the trusted computing base of systems that run machine code from untrusted sources
Conclusion
  • The authors' goal is to reduce the size of the trusted computing base of systems that run machine code from untrusted sources.
  • This is an engineering challenge that requires work on many fronts.
  • The time is ripe to apply all of these advances as engineering tools in the construction of safe systems
Funding
  • ∗This research was supported in part by DARPA award F30602-991-0519 and by National Science Foundation grant CCR-9974553
Reference
  • Andrew W. Appel. Hints on proving theorems in Twelf. www.cs.princeton.edu/ ̃appel/twelf-tutorial, February 2000.
    Findings
  • Andrew W. Appel and Edward W. Felten. Models for security policies in proof-carrying code. Technical Report TR-636-01, Princeton University, March 2001.
    Google ScholarFindings
  • Andrew W. Appel and Amy P. Felty. A semantic model of types and machine instructions for proof-carrying code. In POPL ’00: The 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 243–25ACM Press, January 2000.
    Google ScholarLocate open access versionFindings
  • Andrew W. Appel and David McAllester. An indexed model of recursive types for foundational proof-carrying code. Technical Report TR-629-00, Princeton University, October 2000.
    Google ScholarFindings
  • Andrew W. Appel, Kedar N. Swadi, and Roberto Virga. Efficient substitution in hoare logic expressions. In 4th International Workshop on Higher-Order Operational Techniques in Semantics (HOOTS 2000). Elsevier, September 2000. Electronic Notes in Theoretical Computer Science 41(3).
    Google ScholarLocate open access versionFindings
  • Juan Chen and Andrew W. Appel. Dictionary passing for polytypic polymorphism. Technical Report CS-TR-63501, Princeton University, March 2001.
    Google ScholarFindings
  • Christopher Colby, Peter Lee, George C. Necula, Fred Blau, Ken Cline, and Mark Plesko. A certifying compiler for Java. In Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’00). ACM Press, June 2000.
    Google ScholarLocate open access versionFindings
  • Karl Crary and Stephanie Weirich. Flexible type analysis. In ACM SIGPLAN International Conference on Functional Programming Languages, September 1999.
    Google ScholarLocate open access versionFindings
  • Cormac Flanagan and James B. Saxe. Avoiding exponential explosion: Generating compact verification conditions. In POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 193–205. ACM Press, January 2001.
    Google ScholarLocate open access versionFindings
  • Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143–184, January 1993.
    Google ScholarLocate open access versionFindings
  • Robert Harper and Greg Morrisett. Compiling polymorphism using intensional type analysis. In Twenty-second Annual ACM Symp. on Principles of Prog. Languages, pages 130–141, New York, Jan 1995. ACM Press.
    Google ScholarLocate open access versionFindings
  • Neophytos G. Michael and Andrew W. Appel. Machine instruction syntax and semantics in higher-order logic. In 17th International Conference on Automated Deduction, June 2000.
    Google ScholarLocate open access versionFindings
  • Stefan Monnier, Bratin Saha, and Zhong Shao. Principled scavenging. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’01), page to appear, June 2001.
    Google ScholarLocate open access versionFindings
  • Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. ACM Trans. on Programming Languages and Systems, 21(3):527–568, May 1999.
    Google ScholarLocate open access versionFindings
  • George Necula. Proof-carrying code. In 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 106–119, New York, January 1997. ACM Press.
    Google ScholarLocate open access versionFindings
  • George Ciprian Necula. Compiling with Proofs. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, September 1998.
    Google ScholarFindings
  • Frank Pfenning. Elf: A meta-language for deductive systems. In A. Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction, pages 811– 815, Nancy, France, June 1994. Springer-Verlag LNAI 814.
    Google ScholarLocate open access versionFindings
  • Frank Pfenning and Carsten Schurmann. System description: Twelf — a meta-logical framework for deductive systems. In The 16th International Conference on Automated Deduction. Springer-Verlag, July 1999.
    Google ScholarLocate open access versionFindings
  • Norman Ramsey and Mary F. Fernandez. Specifying representations of machine instructions. ACM Trans. on Programming Languages and Systems, 19(3):492–524, May 1997.
    Google ScholarLocate open access versionFindings
  • Mads Tofte and Jean-Pierre Talpin. Implementation of the typed call-by-value λ-calculus using a stack of regions. In Twenty-first ACM Symposium on Principles of Programming Languages, pages 188–201. ACM Press, January 1994.
    Google ScholarLocate open access versionFindings
  • David Walker, Karl Crary, and Greg Morrisett. Typed memory management via static capabilities. ACM Trans. on Programming Languages and Systems, 22(4):701–771, July 2000.
    Google ScholarLocate open access versionFindings
  • Daniel C. Wang and Andrew W. Appel. Type-preserving garbage collectors. In POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 166–178. ACM Press, January 2001.
    Google ScholarLocate open access versionFindings
Your rating :
0

 

Tags
Comments
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn
小科