Secure Programming via Visibly Pushdown Safety Games
William R. Harris, Somesh Jha, and Thomas Reps
Several recent operating systems provide system calls that
allow an application to explicitly manage the privileges of modules with
which the application interacts. Such privilege-aware operating systems
allow a programmer to a write a program that satisfies a strong security
policy, even when it interacts with untrusted modules. However, it is
often non-trivial to rewrite a program to correctly use the system calls
to satisfy a high-level security policy. This paper concerns the
policy-weaving problem, which is to take as input a program, a desired
high-level policy for the program, and a description of how system calls affect
privilege, and automatically rewrite the program to invoke the system
calls so that it satisfies the policy. We present an algorithm that solves
the policy-weaving problem by reducing it to finding a winning modular
strategy to a visibly pushdown safety game, and applies a novel
game-solving algorithm to the resulting game. Our experiments demonstrate
that our algorithm can efficiently rewrite practical programs for a
practical privilege-aware system.
(Click here to access the paper:
PDF.)
University of Wisconsin