A Quantified Model of Security Policies, with an Application for Injection-Attack Prevention

This dissertation generalizes traditional models of security policies, from specifications of whether programs are secure, to specifications of how secure programs are. This is a generalization from qualitative, black-and-white policies to quantitative, gray policies. Included are generalizations from traditional definitions of safety and liveness policies to definitions of gray-safety and gray-liveness policies. These generalizations preserve key properties of safety and liveness, including that the intersection of safety and liveness is a unique allow-all policy and that every policy can be written as the conjunction of a single safety and a single liveness policy. It is argued that the generalization provides several benefits, including that it serves as a unifying framework for disparate approaches to security metrics, and that it separates—in a practically useful way—specifications of how secure systems are from specifications of how secure users require their systems to be. To demonstrate the usefulness of the new model, policies for mitigating injection attacks (including both code- and noncode-injection attacks) are explored. These policies are based on novel techniques for detecting injection attacks that avoid many of the problems associated with existing mechanisms for preventing injection attacks