Report: PDF | PS
We propose to apply static analysis to the problem of confining untrusted code. Most existing systems, including Java stack inspection, tackle this problem using the abstraction of "privileges." Privileges are often too coarse-grained to express what users really want to allow. For instance, a root mail daemon may need to execute code as other users to apply filters, but it shouldn't run one user's filter as a different user. Trying to make privileges more specific only leads to an infinite regress; there is always some program that users find acceptable due to more subtle properties of its interactions with the system.
The real problem here is a common one: conflation of policy and mechanism. End users don't care how security is achieved as long as it is achieved. We propose making it the responsibility of the end-user to specify a security policy and the responsibility of the code producer to show that it is satisfied, in the style of Proof-Carrying Code. PCC has previously been applied mostly to memory safety and other low-level policies. We would like to try using it with higher-level policies like those in most privilege-based systems, while still maintaining the same small TCB.
We would like to prototype a system that is somewhat like a static analysis version of Janus. An end user specifies security policies in the form of logical pre- and postconditions on system functions. Before he runs a new untrusted binary, he runs it through a Proof-Carrying Code system that can verify that it obeys the policy. The big difference is that trusted Janus modules combine policies with the mechanisms for checking them. We want to let code producers use whatever mechanisms they want for satisfying policies. To this end, binaries may come with custom verification information that can be used without trusting it. Static verification also lets us present the end user with a one-time policy decision to execute all of a program, instead of allowing nasty surprises where a program's execution is halted midway because it breaks the security policy.