Aspect-Oriented Runtime Monitor Certification

摘要

In-lining runtime monitors into untrusted binary programs via aspect-weaving is an increasingly popular technique for efficiently and flexibly securing untrusted mobile code. However, the complexity of the monitor implementation and in-lining process in these frameworks can lead to vulnerabilities and low assurance for code-consumers. This paper presents a machine-verification technique for aspect-oriented in lined reference monitors based on abstract interpretation and model checking. Rather than relying upon trusted advice, the system verifies semantic properties expressed in a purely declarative policy specifica tion language. Experiments on a variety of real-world policies and Java applications demonstrate that the approach is practical and effective.