Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 George Necula's Papers
XFI: Software Guards for System Address Spaces. Ulfar Erlingsson, Martin Abadi, Michael Vrable, Mihai Budiu, George Necula. In Proceedings of Operating System Design and Implementation (OSDI'06), Seattle, 2006.
JVer: A Java Verifier. A.
Chander, D. Espinosa, N. Islam, P. Lee, G. Necula. In Proceedings of the
Conference on Computer Aided Verification (CAV’05), 2005.
Data Slicing: Separating the
Heap into Independent Regions. Jeremy Condit, George C. Necula. In
Proceedings of the Conference on Compiler Construction (CC’05),
2005. Paper received European Association for Programming Languages and
Systems Award.
Mining Temporal Specifications
for Error Detection. Westley Weimer, George C. Necula. In Proceedings
of the Conference on Tools and Applications for the Construction and
Analysis of Systems (TACAS’05), 2005.
CCured: Type-Safe Retrofitting
of Legacy Software, George C. Necula, Jeremy Condit, Matthew Harren,
Scott McPeak, Westley Weimer. In ACM Transactions on Programming Languages
and Systems (TOPLAS), Vol 27, No 3, May 2005.
The Open Verifier Framework for
Foundational Verifiers, Bor-Yuh Evan Chang, Adam Chlipala, George C.
Necula, Robert R. Schneck. In Proceedings of the ACM SIGPLAN Workshop
on Types in Language Design and Implementation (TLDI’05),
2005.
Join Algorithms for the Theory
of Uninterpreted Functions, Sumit Gulwani, Ashish Tiwari, George C.
Necula. In Proceedings of the Conference on Foundations of Software
Technology and Theoretical Computer Science (FSTTCS’04), 2004.
Capriccio: Scalable
Threads for Internet Services, Rob von Behren, Jeremy Condit, Feng
Zhou, George C. Necula, Eric Brewer. In Proceeding of Symposium on
Operating System Principles, SOSP03, October 2003.
CCured in the Real World.
Jeremy Condit, Mathew Harren, Scott McPeak, George C. Necula, Westley
Weimer. In Proceedings of the ACM SIGPLAN 2003 Conference on Programming
Language Design and Implementation (PLDI03), June 2003.
Temporal Safety Proofs for Systems
Code. Thomas Henzinger, Ranjit Jhala, Rupak Majumdar, George Necula,
Gregoire Sutre, Westley Weimer. In Proceedings of the 14th International
Conference on Computer Aided Verification (CAV'02), Copenhagen, July
2002.
CCured: Type-Safe Retrofitting
of Legacy Code. George C. Necula, Scott McPeak, Westley Weimer. In Proceedings
of the 29th ACM Symposium on Principles of Programming Languages (POPL02),
London, January 2002.
Proof-Carrying Code. Design and
Implementation. George C. Necula. In H. Schwichtenberg and R.
Steinbruggen (eds.), Proof and System Reliability (lecture notes for a
summer course in Marktoberdorf, 2001).
Oracle-Based Checking of
Untrusted Software. George C. Necula, S. P. Rahul. In
Proceedings of the 28th ACM Symposium on Principles of Programming
Languages (POPL01), London, January 2001.
A Proof-Carrying Code Architecture for
Java, Christopher Colby, Peter Lee, George C. Necula. In Proceedings
of the 12th International Conference on Computer Aided Verification
(CAV00), Chicago, 15 July 2000.
A Certifying Compiler for
Java, Christopher Colby, Peter Lee, George C. Necula, Fred Blau, Ken
Cline, Mark Plesko. In Proceedings of the 2000 ACM SIGPLAN Conference on
Programming Language Design and Implementation (PLDI00), Vancouver,
British Columbia, Canada, June 18-21, 2000.
Translation Validation for an
Optimizing Compiler, George C. Necula. In Proceedings of the
2000 ACM SIGPLAN Conference on Programming Language Design and
Implementation (PLDI00), Vancouver, British Columbia, Canada, June 18-21,
2000.
This paper was reprinted in “20 years of
ACM/SIGPLAN Conference on Programming Language Design and Implementation
(1979-1999): A Selection”, 2003. See the authors retrospective.
Compiling
with Proofs. George C. Necula, Carnegie Mellon University, September
1998.
An annotated bibliography on
Proof-Carrying Code
Note: This is not up to date anymore. Now it should contain also
many papers by other authors.
Note:
this bibliography is now out of date and does not include papers written by
other researchers. The following
papers are ordered by their technical difficulty, starting with the gentlest
introductions to the Proof-Carrying Code technique and ending with a detailed
implementation guide. These papers address different aspects of Proof-Carrying
Code, ranging from its foundations in type-theory and logic, to its
applications in software systems. I recommend first the application papers
since the papers dealing with type-theory and logic might seem too technical to
the reader that is not experienced in these areas. However, even in the most
technical of the papers, we have tried to get across the purely practical and
engineering motivations for most of the formal developments, and so, they might
make an interesting reading even for the non-specialist
For the busy reader, here is a one-page
introduction to Proof-Carrying Code: "Research
on Proof-Carrying Code for Untrusted-Code Security". George C.
Necula and Peter Lee. In Proceedings of the 1997 IEEE Symposium on Security and
Privacy, Oakland, 1997.
Another short paper about Proof-Carrying Code,
with an emphasis on its applications for mobile-code security: "Research on Proof-Carrying Code on Mobile-Code Security".
George C. Necula and Peter Lee. In Proceedings of the Workshop on Foundations
of Mobile Code Security, Monterey, 1997.
Abstract: This paper
received the "Best Paper
Award" at OSDI'96. This is
the gentler introduction to Proof-Carrying Code and its applications in
systems. As a case study, we analyze in this paper the use of PCC for
ensuring the safety of network packet filters. We show that PCC can be
used even for hand-optimized packet filters written in assembly language.
As a result the runtime performance of PCC packet filters is the best
attainable on a given architecture. Measurements show that this approach
yields filters that are about an order of magnitude faster than
interpreted Berkeley Packet Filters and about 30% faster than filters
"sandboxed" filters using Software Fault Isolation. The cost of
PCC filters lies in proof checking. Measurements show that proof-checking
is fast and its one-time cost is usually amortized over a few thousand
network packets.
If you want to read about more applications
on the spirit of network packet filters, then you can read the expanded version of the OSDI'96 paper. Keep in
mind, however, that some of the later papers might describe PCC slightly
differently, as our own understanding of it has improved.
Next paper is the
standard reference for PCC. "Proof-Carrying
Code ". George C. Necula. Presented at POPL97, January 1997.
· Abstract: This paper describes Proof-Carrying Code from a more
formal and language-theoretic perspective. On the application side, this paper
describes the use of PCC as a basis for verifying the type safety of
hand-optimized assembly language programs. This is useful for the safe
interaction of native code libraries with code written in a type-safe language.
· Abstract: This paper presents a compiler from a type-safe
subset of the C language to optimized DEC Alpha machine code. The novel feature
of the compiler is that it contains a certifier that automatically
checks the type safety and memory safety of any assembly language program
produced by the compiler. The result of the certifier is either a formal proof
of type safety or a counterexample pointing to a potential violation of the
type system by the assembly-language target program. The ensemble of the
compiler and the certifier is called a certifying compiler.
Several advantages
of certifying compilation over previous approaches can be claimed. The notion
of a certifying compiler is significantly easier to employ than a formal compiler
verification, in part because it is generally easier to verify the correctness
of the result of a computation than to prove the correctness of the computation
itself. Also, the approach can be applied even to highly optimizing compilers,
as demonstrated by the fact that our compiler generates target code, for a
range of realistic C programs, which is competitive with both the cc and gcc
compilers with all optimizations enabled. The certifier also drastically
improves the effectiveness of compiler testing because, for each test case, it
statically signals compilation errors that might otherwise require many
executions to detect. Finally, this approach is a practical way to produce the
safety proofs for a Proof-Carrying Code system, and thus may be useful in a
system for safe mobile code.
This is the most
technical paper on PCC. It describes the framework that is used in PCC to
represent and to verify the safety proofs: Efficient
Representation and Validation of Proofs George C. Necula, Peter Lee, June
1998, presented at LICS'98.
· Abstract: This paper presents a logical framework derived from
the Edinburgh Logical Framework (LF) that can be used to obtain compact
representations of proofs and efficient proof checkers. These are essential
ingredients of any application that manipulates proofs as first-class objects, such
as a Proof-Carrying Code system, in which proofs are used to allow the easy
validation of properties of safety-critical or untrusted code.
Our framework,
which we call LFi, inherits from LF the capability to encode various logics in
a natural way. In addition, the LFi framework allows proof representations
without the high degree of redundancy that is characteristic of LF
representations. The missing parts of LFi proof representations can be
reconstructed during proof checking by an efficient reconstruction algorithm.
We also describe an algorithm that can be used to strip the unnecessary parts
of an LF representation of a proof. The experimental data that we gathered in
the context of a Proof-Carrying Code system shows that the savings obtained
from using LFi instead of LF can make the difference between practically
useless proofs of several megabytes and manageable proofs of tens of kilobytes.
This paper is an
abbreviated version of a longer (70 pages) technical
report. Read it if you want to see the detailed (15 pages) proofs of
soundness of the efficient proof-checking algorithm that is used in PCC.
This longer paper
describes many of the implementation details of our PCC prototype. It also
describes the use of PCC for enforcing resource-usage bounds in addition to
memory and type-safety. Safe, Untrusted Agents
using Proof-Carrying Code George C. Necula, Peter Lee. October 1997, in
LNCS 1419: Special Issue on Mobile Agent Security.
· Abstract: This paper is intended to be both a comprehensive
implementation guide for a Proof-Carrying Code system and a case study for
using PCC in a mobile agent environment. Specifically, the paper describes the
use of PCC for enforcing memory safety, access control and resource usage
bounds for untrusted agents that access a database.