Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement
Matthew Fredrikson, Richard Joiner, Somesh Jha, Thomas Reps, Phillip Porras, Hassen Saïdi, and Vinod Yegneswaran
Stateful security policies—which specify restrictions on behavior in
terms of temporal safety properties—are a powerful tool for
administrators to control the behavior of untrusted programs.
However, the runtime overhead required to enforce them on real
programs can be high. This paper describes a technique for
rewriting programs to incorporate runtime checks so that all
executions of the resulting program either satisfy the policy, or halt
before violating it. By introducing a rewriting step before runtime
enforcement, we are able to perform static analysis to optimize the
code introduced to track the policy state. We developed a novel
analysis, which builds on abstraction-refinement techniques, to derive
a set of runtime policy checks to enforce a given policy—as well as
their placement in the code. Furthermore, the abstraction refinement
is tunable by the user, so that additional time spent in analysis
results in fewer dynamic checks, and therefore more efficient code.
We report experimental results on an implementation of the algorithm
that supports policy checking for JavaScript programs.
(Click here to access the paper:
PDF;
(c) Springer-Verlag.)