Clara: Proving safety and security properties by evaluating runtime monitors ahead of time

In this talk we focus on the Clara system for evaluating runtime monitors ahead of time. Clara statically evaluates runtime monitors expressed as "aspects" in the aspect-oriented programming language AspectJ. Monitors expressed as aspects are easy to write, read, maintain and analyze. This allows Clara to use syntactic, pointer-based and control-flow-based analysis techniques to partially evaluate runtime monitors already at compile-time.

Partial ahead-of-time evaluation is a powerful concept: For many programs, Clara can prove the absence of property violations on all possible executions. For other programs, Clara typically restricts the program instrumentation for runtime monitoring to a necessary minimum, speeding up the runtime monitoring process by orders of magnitude. In this talk we cover previous work on applying Clara to validate safety properties of large-scale Java programs, but we also introduce our current and planned lines of work on using Clara to enforce access-control and information-flow policies.