MPI-INF Logo
Campus Event Calendar

Event Entry

New for: D2, D3

What and Who

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

Eric Bodden
TU Darmstadt
Talk
AG 1, AG 3, AG 5, SWS, AG 2, AG 4, RG1, MMCI  
AG Audience
English

Date, Time and Location

Thursday, 9 June 2011
11:30
45 Minutes
E1 4
019
Saarbr├╝cken

Abstract

A runtime monitor observes events during a program's execution and validates these events against the specification of a safety or security property. When detecting a property violation, the monitor can log the violation or even prevent the violating event from actually occurring. As we show, the latter allows the enforcement of access-control or information-flow policies.


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.

Contact

gk-sek
--email hidden

Video Broadcast

Yes
Kaiserslautern
passcode not visible
logged in users only

gk-sek, 06/03/2011 01:11 PM -- Created document.