Integrating a certified memory management runtime with proof-carrying code
Pages 1526 - 1533
Abstract
Software systems today are 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.
References
[1]
A. W. Appel. Foundational proof-carrying code. In Proceedings 16th Annual IEEE Symposium on Logic in Computer Science (LICS'01), pages 247--258, June 2001.
[2]
K. Crary and S. Sarkar. A metalogical approach to foundational certified code. Technical Report CMU-CS-03-108, School of Computer Science, Carnegie Mellon University, Pittsburg, PA, Jan. 2003.
[3]
N. A. Hamid. A Syntactic Approach to Foundational Proof-Carrying Code. PhD thesis, Yale University, New Haven, CT, May 2005.
[4]
N. A. Hamid and Z. Shao. Interfacing hoare logic and type systems for foundational proof-carrying code. In Proceedings 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004), volume 3223 of LNCS, pages 118--135. Springer-Verlag, Sept. 2004.
[5]
N. A. Hamid, Z. Shao, V. Trifonov, S. Monnier, and Z. Ni. A syntactic approach to foundational proof carrying-code. Journal of Automated Reasoning (Special issue on Proof-Carrying Code), 31(3--4):191--229, Dec. 2003.
[6]
G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language. In Proceedings 25th ACM Symposium on Principles of Programming Languages, pages 85--97. ACM Press, Jan. 1998.
[7]
G. C. Necula. Proof-carrying code. In Proceedings 24th ACM Symposium on Principles of Programming Languages, pages 106--119. ACM Press, Jan. 1997.
[8]
G. C. Necula and P. Lee. Safe kernel extensions without run-time checking. In Proceedings 2nd USENIX Symp. on Operating System Design and Impl., pages 229--243, 1996.
[9]
Z. Ni and Z. Shao. Certified assembly programming with embedded code pointers. In Proceedings 33rd ACM Symposium on Principles of Programming Languages, pages 320--333. ACM Press, Jan. 2006.
[10]
C. Paulin-Mohring. Inductive definitions in the system Coq---rules and properties. In M. Bezem and J. Groote, editors, Proceedings TLCA, volume 664 of LNCS. Springer-Verlag, 1993.
[11]
J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings 17th Annual IEEE Symposium on Logic in Computer Science (L ICS'02), pages 55--74. IEEE Computer Society, July 2002.
[12]
The Coq Development Team. The Coq proof assistant reference manual. Coq release v8.0, 2004.
[13]
D. Walker, K. Crary, and G. Morrisett. Typed memory management via static capabilities. ACM Trans. Prog. Lang. Syst., 22(4):701--771, 2000.
[14]
A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38--94, 1994.
[15]
D. Yu, N. A. Hamid, and Z. Shao. Building certified libraries for PCC: Dynamic storage allocation. Science of Computer Programming, 50(1--3):101--127, 2004.
Index Terms
- Integrating a certified memory management runtime with proof-carrying code
Recommendations
Certified memory management for proof-carrying code: a region-based type system and runtime library
ACMSE '05 vol 2: Proceedings of the 43rd annual ACM Southeast Conference - Volume 2Proof-Carrying Code (PCC) is a generic framework intended to facilitate safe execution of code from an unknown or untrusted source. The basic idea of PCC, as the name implies, is that a piece of executable code comes packaged with a proof of its safety ...
Code-carrying theory
SAC '08: Proceedings of the 2008 ACM symposium on Applied computingCode-Carrying Theory (CCT) is an alternative to the Proof-Carrying Code (PCC) approach to secure delivery of code. With PCC, code is accompanied by assertions and a proof of correctness or of other required properties. The code consumer does not accept ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
March 2007
1688 pages
ISBN:1595934804
DOI:10.1145/1244002
- Conference Chairs:
- Yookun Cho,
- Roger L. Wainwright,
- Hisham M. Haddad,
- Sung Y. Shin,
- Program Chair:
- Yong Wan Koo
Copyright © 2007 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 11 March 2007
Check for updates
Author Tags
Qualifiers
- Article
Conference
SAC07
Sponsor:
Acceptance Rates
Overall Acceptance Rate 1,650 of 6,669 submissions, 25%
Upcoming Conference
SAC '25
- Sponsor:
- sigapp
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 126Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 23 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in