Declarative aspect-oriented security policies for in-lined reference monitors
Kevin W. Hamlen, Micah Jones · 2011
Aspect-oriented in-lined reference monitor frameworks provide an elegant and increasingly popular means of enforcing security policies on untrusted code through automated rewriting. However, it is often difficult to prove that the resulting instrumented code is secure with respect to the intended policy, especially when that policy is described in terms of arbitrary imperative code insertions. The dissertation presents a fully declarative policy language, powerful enough to enforce real-world security policies yet simple enough for automated verification systems to correctly reason about them. It also presents an analysis tool that detects policy inconsistencies, a service-oriented framework for instrumenting untrusted code, and a full-scale abstract interpretation and model-checking system that verifies the safety of rewritten programs.