Skip to main content
SpringerLink
Log in
Book cover

Mobile Agents and Security pp 61–91Cite as

Safe, Untrusted Agents Using Proof-Carrying Code

  • Chapter
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1419))

Abstract

Proof-Carrying Code (PCC) enables a computer system to determine, automatically and with certainty, that program code provided by another system is safe to install and execute without requiring interpretation or run-time checking. PCC has applications in any computing system in which the safe, efficient, and dynamic installation of code is needed. The key idea is to attach to the code an easily-checkable proof that its execution does not violate the safety policy of the receiving system. This paper describes the design and a typical implementation of Proof-Carrying Code, where the language used for specifying the safety properties is first-order predicate logic. Examples of safety properties described in this paper are memory safety and compliance with data access policies, resource usage bounds, and data abstraction boundaries.

This research was sponsored in part by the Advanced Research Projects Agency CSTO under the title “The Fox Project: Advanced Languages for Systems Software,” ARPA Order No. C533, issued by ESC/ENS under Contract No. F19628-95-C-0050.

The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the Advanced Research Projects Agency or the U.S. Government.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Brian Bershad, Stefan Savage, Przemyslaw Pardyak, Emin Gun Sirer, David Becker, Marc Fiuczynski, Craig Chambers, and Susan Eggers. Extensibility, safety and performance in the SPIN operating system. In Symposium on Operating System Principles, pages 267–284, December 1995.

    Google Scholar 

  2. Robert Boyer and J. Strother Moore. A Computational Logic. Academic Press, 1979.

    Google Scholar 

  3. R.M. Burstall and P.J. Landin. Programs and their proofs: an algebraic approach. Machine Intelligence, (4), 1969.

    Google Scholar 

  4. R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R.W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986.

    Google Scholar 

  5. Thiery Coquand and Gerard Huet. Constructions: A higher order proof system for mechanizing mathematics. In Proc. European Conf. on Computer Algebra (EUROCAL’85), LNCS 203, pages 151–184. Springer-Verlag, 1985.

    Google Scholar 

  6. D.C. Luckham et al. Stanford Pascal verifier user manual. Technical Report STAN-CS-79-731, Dept. of Computer Science, Stanford Univ., March 1979.

    Google Scholar 

  7. David Detlefs. An overview of the Extended Static Checking system. In Proceedings of the First Formal Methods in Software Practice Workshop, 1996.

    Google Scholar 

  8. Edsger W. Dijkstra. Guarded commands, nondeterminancy and formal derivation of programs. Communications of the ACM, 18:453–457, 1975.

    Article  MathSciNet  Google Scholar 

  9. Michael Gordon. HOL: A machine oriented formulation of higher-order logic. Technical Report 85, University of Cambridge, Computer Laboratory, July 1985.

    Google Scholar 

  10. James Gosling, Bill Joy, and Guy L. Steele. The Java Language Specification. The Java Series. Addison-Wesley, Reading, MA, USA, 1996.

    MATH  Google Scholar 

  11. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143–184, January 1993.

    Article  MathSciNet  Google Scholar 

  12. Steven McCanne and Van Jacobson. The BSD packet filter: A new architecture for user-level packet capture. In The Winter 1993 USENIX Conference, pages 259–269. USENIX Association, January 1993.

    Google Scholar 

  13. Sun Microsystems. The Java Virtual Machine specification. Available as ftp://ftp.javasoft.com/docs/vmspec.ps.zip, 1995.

  14. George C. Necula and Peter Lee. Efficient representation and validation of logical proofs. Technical Report CMU-CS-97-172, Computer Science Department, Carnegie Mellon University, October 1997.

    Google Scholar 

  15. George C. Necula and Peter Lee. The design and implementation of a certifying compiler. In ACM SIGPLAN’98 Conference on Programming Language Design and Implementation, June 1998.

    Google Scholar 

  16. Greg Nelson and Derek Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245–257, October 1979.

    Article  Google Scholar 

  17. John R. Ousterhout. Tcl and the Tk Toolkit. Addison Wesley, 1994.

    Google Scholar 

  18. S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748–752, Saratoga, NY, June 1992. Springer-Verlag.

    Google Scholar 

  19. Frank Pfenning. Elf: A meta-language for deductive systems (system description). In Alan Bundy, editor, 12th International Conference on Automated Deduction, LNAI 814, pages 811–815, Nancy, France, June 26–July 1, 1994. Springer-Verlag.

    Google Scholar 

  20. R. Wahbe, S. Lucco, T. E. Anderson, and S. L. Graham. Efficient software-based fault isolation. In 14th ACM Symposium on Operating Systems Principles, pages 203–216. ACM, December 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, 15217, USA

    George C. Necula & Peter Lee

Authors
  1. George C. Necula
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Peter Lee
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science Department, University of California, Santa Barbara, CA, 93106-5110, USA

    Giovanni Vigna

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Necula, G.C., Lee, P. (1998). Safe, Untrusted Agents Using Proof-Carrying Code. In: Vigna, G. (eds) Mobile Agents and Security. Lecture Notes in Computer Science, vol 1419. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-68671-1_5

Download citation

  • DOI: https://doi.org/10.1007/3-540-68671-1_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64792-8

  • Online ISBN: 978-3-540-68671-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation