New operating systems with security-specific system calls, such as the Capsicum capability system, allow programmers to write applications that satisfy strong security properties with significantly less effort than full verification. However, the amount of effort required is still high enough that even the Capsicum developers have reported difficulties in writing correct programs for their system.

In this work, we present an algorithm that automatically rewrites a program for Capsicum so that it satisfies a given security policy by finding a winning strategy to an automata-theoretic safety game. We have implemented our algorithm as a tool, and we present experimental results that demonstrate that our algorithm can be applied to rewrite practical programs to satisfy practical security properties. Capsicum, combined with our algorithm, thus represents a sweet spot in the trade-off between the strength of policies that an operating system can enforce, and the ease of programming for such a system.

(Click here to access the paper: PDF.)