Proof-carrying code is a technique that can be used to execute untrusted code safely. A code consumer specifies requirements and safety rules which define the safe behavior of a system, and a code producer packages each program with a formal proof that the program satisfies the requirements. The consumer uses a fast proof validator to check that the proof is correct, and hence the program is safe. In this report, we discuss applications for which proof-carrying code is appropriate, explain the mechanics of proof-carrying code, compare it with other security techniques and propose research directions for the method.

Pre-2018 CSE ID: CS1999-0633

We show that bounded-depth Frege systems with counting principles modulo m can polynomially simulate Nullstellensatz refutations modulo m. This establishes new upper bounds for proofs of certain tautologies in bounded-depth Frege with counting axioms systems. When combined with another result of the authors, this simulation establishes a size (as opposed to a degree) separation between Nullstellensatz and polynomial calculus refutations.

Pre-2018 CSE ID: CS2001-0686

We present an adaptive strategy to recover two secrets from an adversary which uses linear size queries and is computationally efficient. To obtain an intersecting family containing the two n bit secrets, 4n+3 queries are made, and time O(n^2) and space O(n) are consumed.

Pre-2018 CSE ID: CS2001-0687

For each $k \geq 1$, we give a famiily of unsatisfiable sets of clauses which have polynomial size ${\mbox{Res}}(k+1)$ refutations, but which require ${\mbox{Res}}(k)$ refutations of $2^{n^{\epsilon_k}}$. This improves the superpolynomial- separation between resolution and ${\mbox{Res}}(2)$ given by Bonet and Galesi to exponential. As a corollary, we obtain an exponential separation between depth 0 Frege and depth 1 Frege, improving upon the superpolynomial separation given by the weak pigeonhole principle.

Pre-2018 CSE ID: CS2002-0697