Title :
Declarative, Temporal, and Practical Programming with Capabilities
Author :
Harris, W.R. ; Jha, Somesh ; Reps, Tom ; Anderson, Jon ; Watson, R.N.M.
Author_Institution :
Univ. of Wisconsin-Madison, Madison, WI, USA
Abstract :
New operating systems, such as the Capsicum capability system, allow a programmer to write an application that satisfies strong security properties by invoking security-specific system calls at a few key points in the program. However, rewriting an application to invoke such system calls correctly is an error-prone process: even the Capsicum developers have reported difficulties in rewriting programs to correctly invoke system calls. This paper describes capweave, a tool that takes as input (i) an LLVM program, and (ii) a declarative policy of the possibly-changing capabilities that a program must hold during its execution, and rewrites the program to use Capsicum system calls to enforce the policy. Our experiments demonstrate that capweave can be applied to rewrite security-critical UNIX utilities to satisfy practical security policies. capweave itself works quickly, and the runtime overhead incurred in the programs that capweave produces is generally low for practical workloads.
Keywords :
Unix; program compilers; program verification; rewriting systems; security of data; software tools; Capsicum capability system; Capsicum developers; Capsicum system calls; LLVM program; capweave; declarative policy; declarative programming; error-prone process; operating systems; practical programming; program rewriting; runtime overhead; security policy; security-critical UNIX utilities; security-specific system calls; temporal programming; Instruments; Operating systems; Security; Semantics; Servers; Uniform resource locators; Weaving; capabilities; safety games;
Conference_Titel :
Security and Privacy (SP), 2013 IEEE Symposium on
Conference_Location :
Berkeley, CA
Print_ISBN :
978-1-4673-6166-8
Electronic_ISBN :
1081-6011