@INPROCEEDINGS{hamid04:rtpcc,
AUTHOR = {Nadeem Abdul Hamid and Zhong Shao},
TITLE = {Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code},
BOOKTITLE = {Proceedings 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004)},
PUBLISHER = {Springer},
SERIES = {LNCS},
VOLUME = {3223},
MONTH = SEP,
YEAR = 2004,
LOCATION = {Park City, Utah},
PAGES = {118--135},
PS = {rtpcc.ps.gz},
PDF = {rtpcc.pdf},
URL = {http://www.springerlink.com/link.asp?id=ybrk3xcg1nky0mrl},
COQ = {rtpcc.coq.tar.gz},
NOTE = {(c) 2004 Springer},
ABSTRACT = {In this paper, we introduce a Foundational Proof-Carrying
Code (FPCC) framework for constructing certified
code packages from typed assembly language that will
interface with a similarly certified runtime
system. Our framework permits the typed assembly
language to have a ``foreign function'' interface,
in which stubs, initially provided when the program
is being written, are eventually compiled and linked
to code that may have been written in a language
with a different type system, or even certified
directly in the FPCC logic using a proof
assistant. We have increased the potential
scalability and flexibility of our FPCC system by
providing a way to integrate programs compiled from
different source type systems. In the process, we
are explicitly manipulating the interface between
Hoare logic and a syntactic type system.
To our knowledge, this is the first account of combining such
certification proofs from languages at different
levels of abstraction. While type systems such as
TAL facilitate reasoning about many programs, they
are not sufficient for certifying the most low-level
system libraries. Hoare logic-style reasoning, on
the other hand, can handle low-level details very
well but cannot account for embedded code pointers
in data structures, a feature common to higher-order
and object-oriented programming. We outline for the
first time a way to allow both methods of
verification to interact, gaining the advantages of
both and circumventing their shortcomings.}
}
@INPROCEEDINGS{hamid02:safpcc,
AUTHOR = {Nadeem Abdul Hamid and Zhong Shao and Valery Trifonov and Stefan Monnier and Zhaozhong Ni},
TITLE = {A Syntactic Approach to Foundational Proof-Carrying Code},
BOOKTITLE = {Proceedings 17th Annual IEEE Symposium on Logic In
Computer Science (LICS'02)},
PUBLISHER = {IEEE},
MONTH = JUL,
YEAR = 2002,
LOCATION = {Copenhagen, Denmark},
PAGES = {89--100},
PS = {safpcc.ps.gz},
PDF = {safpcc.pdf},
COQ = {safpcc.coq.tar.gz},
NOTE = {(c) 2002 IEEE},
ABSTRACT = {
Proof-Carrying Code (PCC) is a general framework for verifying
the safety properties of machine-language
programs. PCC proofs are usually written in a logic
extended with language-specific typing rules. In
Foundational Proof-Carrying Code (FPCC), on the
other hand, proofs are constructed and verified
using strictly the foundations of mathematical
logic, with no type-specific axioms. FPCC is more
flexible and secure because it is not tied to any
particular type system and it has a smaller trusted
base.
Foundational proofs, however, are much harder to
construct. Previous efforts on FPCC all required
building sophisticated semantic models for types. In
this paper, we present a syntactic approach to FPCC
that avoids the difficulties of previous work. Under
our new scheme, the foundational proof for a typed
machine program simply consists of the typing
derivation plus the formalized syntactic soundness
proof for the underlying type system. We give a
translation from a typed assembly language into FPCC
and demonstrate the advantages of our new system via
an implementation in the Coq proof assistant.
}
}
@ARTICLE{hamid03:safpcc,
AUTHOR = {Nadeem Abdul Hamid and Zhong Shao and Valery Trifonov and Stefan Monnier and Zhaozhong Ni},
TITLE = {A Syntactic Approach to Foundational Proof Carrying-Code},
JOURNAL = {Journal of Automated Reasoning (Special issue on Proof-Carrying Code)},
VOLUME = {31},
NUMBER = {3-4},
MONTH = DEC,
YEAR = 2003,
PAGES = {191--229},
PS = {safpccjar.ps.gz},
PDF = {safpccjar.pdf},
COQ = {safpcc.coq.tar.gz},
NOTE = {(c) 2003 Kluwer Academic Publishers},
ABSTRACT = {
Proof-Carrying Code (PCC) is a general framework for
verifying the safety properties of machine-language
programs. PCC proofs are usually written in a logic
extended with language-specific typing rules; they
certify safety but only if there is no bug in the
typing rules. In Foundational Proof-Carrying Code
(FPCC), on the other hand, proofs are constructed
and verified using strictly the foundations of
mathematical logic, with no type-specific
axioms. FPCC is more flexible and secure because it
is not tied to any particular type system and it has
a smaller trusted base.
Foundational proofs, however, are much harder to
construct. Previous efforts on FPCC all required
building sophisticated semantic models for
types. Furthermore, none of them can be easily
extended to support mutable fields and higher-order
polymorphism. In this article, we present a
syntactic approach to FPCC that avoids all of these
difficulties. Under our new scheme, the foundational
proof for a typed machine program simply consists of
the typing derivation plus the formalized syntactic
soundness proof for the underlying type system. The
former can be readily obtained from a type-checker
while the latter is known to be much easier to
construct than the semantic soundness proofs. We
give a translation from a typed assembly language
into FPCC and demonstrate the advantages of our new
system via an implementation in the Coq proof
assistant.
}
}
@INPROCEEDINGS{yu03:cdsa,
AUTHOR = {Dachuan Yu and Nadeem Abdul Hamid and Zhong Shao},
TITLE = {Building Certified Libraries for {PCC}: Dynamic Storage Allocation},
BOOKTITLE = {Proceedings 12th European Symposium on Programming
(ESOP 2003)},
PUBLISHER = {Springer},
SERIES = {LNCS},
VOLUME = {2618},
MONTH = APR,
YEAR = 2003,
LOCATION = {Warsaw, Poland},
PAGES = {363--379},
PS = {cdsa.ps.gz},
PDF = {cdsa.pdf},
COQ = {cdsacode.tar.gz},
NOTE = {(c) 2003 Springer},
ABSTRACT = {
Proof-Carrying Code (PCC) allows a code producer to provide to a host
a program along with its formal safety proof. The proof attests a
certain safety policy enforced by the code, and can be mechanically
checked by the host. While this language-based approach to code
certification is very general in principle, existing PCC systems have
only focused on programs whose safety proofs can be automatically
generated. As a result, many low-level system libraries (e.g., memory
management) have not yet been handled.
In this paper, we explore a complementary approach in which general
properties and program correctness are semi-automatically certified.
In particular, we introduce a low-level language CAP for building
certified programs and present a certified library for dynamic storage
allocation.}
}
@TECHREPORT{yu03:cdsatr,
AUTHOR = {Dachuan Yu and Nadeem Abdul Hamid and Zhong Shao},
TITLE = {Building Certified Libraries for {PCC}: Dynamic
Storage Allocation},
INSTITUTION = {Dept. of Computer Science, Yale University},
ADDRESS = {New Haven, CT},
NUMBER = {YALEU/DCS/TR-1247},
MONTH = MAY,
YEAR = 2003,
PS = {cdsatr.ps.gz},
PDF = {cdsatr.pdf},
COQ = {cdsacode.tar.gz},
ABSTRACT = {
Proof-Carrying Code (PCC) allows a code producer to provide to a host
a program along with its formal safety proof. The proof attests a
certain safety policy enforced by the code, and can be mechanically
checked by the host. While this language-based approach to code
certification is very general in principle, existing PCC systems have
only focused on programs whose safety proofs can be automatically
generated. As a result, many low-level system libraries (e.g., memory
management) have not yet been handled.
In this paper, we explore a complementary approach in which general
properties and program correctness are semi-automatically certified.
In particular, we introduce a low-level language CAP for building
certified programs and present a certified library for dynamic storage
allocation.}
}
@ARTICLE{yu04:cdsa-scp,
AUTHOR = {Dachuan Yu and Nadeem Abdul Hamid and Zhong Shao},
TITLE = {Building Certified Libraries for {PCC}: Dynamic Storage Allocation},
JOURNAL = {Science of Computer Programming},
VOLUME = 50,
NUMBER = {1-3},
MONTH = MAR,
YEAR = 2004,
PAGES = {101--127},
NOTE = {(c) 2004 Elsevier},
PDF = {cdsa-scp.pdf},
COQ = {cdsacode.tar.gz},
ABSTRACT = {
Proof-Carrying Code (PCC) allows a code producer to provide to a host
a program along with its formal safety proof. The
proof attests to a certain safety policy enforced by
the code, and can be mechanically checked by the
host. While this language-based approach to code
certification is very general in principle, existing
PCC systems have only focused on programs whose
safety proofs can be automatically generated. As a
result, many low-level system libraries (e.g.,
memory management) have not yet been handled. In
this paper, we explore a complementary approach in
which general properties and program correctness are
semi-automatically certified. In particular, we
introduce a low-level language, CAP, for building
certified programs and present a certified library
for dynamic storage allocation.
}
}
@PHDTHESIS{hamid05:phd,
AUTHOR = {Nadeem Abdul Hamid},
TITLE = {A Syntactic Approach to Foundational Proof-Carrying Code},
SCHOOL = {Yale University},
YEAR = 2005,
MONTH = MAY,
ADDRESS = {New Haven, CT},
PS = {nadeem-thesis-11_12.ps.gz},
PDF = {nadeem-thesis-11_12.pdf},
NOTE = {Draft version Nov 2004}
}
@INPROCEEDINGS{hamid05:rgn-acmse,
AUTHOR = {Nadeem Abdul Hamid},
TITLE = {Certified Memory Management for Proof-Carrying Code: A Region-Based
Type System and Runtime Library (Extended Abstract)},
BOOKTITLE = {43rd ACM Southeast Conference},
MONTH = MAR,
YEAR = 2005,
LOCATION = {Kennesaw, Georgia},
NOTE = {(Poster presentation)},
PDF = {rgnacmse.pdf}
}
This file has been generated by bibtex2html 1.77