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;
(c) Springer-Verlag.)
University of Wisconsin