Model-Checking In-Lined Reference Monitors
2010; Springer Science+Business Media; Linguagem: Inglês
10.1007/978-3-642-11319-2_23
ISSN1611-3349
AutoresMeera Sridhar, Kevin W. Hamlen,
Tópico(s)Software Testing and Debugging Techniques
ResumoA technique for elegantly expressing In-lined Reference Monitor (IRM) certification as model-checking is presented and implemented. In-lined Reference Monitors (IRM’s) enforce software security policies by in-lining dynamic security guards into untrusted binary code. Certifying IRM systems provide strong formal guarantees for such systems by verifying that the instrumented code produced by the IRM system satisfies the original policy. Expressing this certification step as model-checking allows well-established model-checking technologies to be applied to this often difficult certification task. The technique is demonstrated through the enforcement and certification of a URL anti-redirection policy for ActionScript web applets.
Referência(s)