Curs 7 – 22 Noiembrie 2010 Adrian Iftene [email protected]
Recapitulation courses 5-6
◦ AOP
◦ Runtime verification
◦ MOP
AOP
Runtime Verification
MOP
2
A crosscutting concern is a concern that needs to be applied in many different compilation
modules
◦ “All exceptions must be logged”
◦ “Capture all sql statements produced by the application”
◦ “Cache all data that is rarely changed”
◦ “Record all changes to the account for historical purposes”
◦ “Timing, authentication, and persistence”
4
Java Code Aspect
public class Student { public aspect StudentAspect {
ajc compiling
public class WeavedStudent {
Concern
Crosscutting concern
Aspect
Join Points
Pointcuts
Advice
Introductions (Inter-type declaration)
6
pointcut name([parameters]): designator(ajoinpoint);
Designators: execution, call, initialization, handler, this, args, target
Advice:
type ([parameters]) : joinpointid (param list) { … }
Type can be: before, after (returning, throwing) and around
How do you explain the result below?
8
10
+ 444956 1290102216340 void Example1.showTime()
+ 444956 1290102216344 long java.lang.System.currentTimeMillis() - 444956 1290102216344 long java.lang.System.currentTimeMillis()
+ 444956 1290102216344 DateFormat java.text.DateFormat.getTimeInstance() - 444956 1290102216359 DateFormat java.text.DateFormat.getTimeInstance() + 444956 1290102216360 String java.text.DateFormat.format(Date)
- 444956 1290102216360 String java.text.DateFormat.format(Date)
+ 444956 1290102216360 StringBuilder java.lang.StringBuilder.append(String) - 444956 1290102216360 StringBuilder java.lang.StringBuilder.append(String) + 444956 1290102216360 String java.lang.StringBuilder.toString()
- 444956 1290102216360 String java.lang.StringBuilder.toString() + 444956 1290102216360 void java.io.PrintStream.println(String) - 444956 1290102216360 void java.io.PrintStream.println(String) - 444956 1290102216360 void Example1.showTime()
12
14
With PostSharp, you can easily write and apply
custom attributes that add new behaviors to your code - tracing, thread management, exception handling, data binding, and much more
Write an Aspect
16
Just annotate relevant methods with the aspect:
You can also apply the aspects to many classes and methods in a single line, without even touching the source code of these classes.
Verification: comprises all techniques for showing that a system satisfies its specification
Runtime Verification: Runtime verification deals with those techniques that allow checking
whether a system under scrutiny satisfies or violates a given safety property
It aims to be lightweight verification technique
complementing verification techniques such as
model checking or testing
18
Runtime verification (RV) is concerned with monitoring and analysis of software or
hardware system executions
Involves three basic techniques:
◦ theorem proving (using mathematics)
◦ model checking (with automated verification)
◦ Testing
The field is referred as runtime verification,
runtime monitoring, runtime checking, runtime
reflection, runtime analysis, dynamic analysis,
symbolic dynamic analysis, trace analysis, log
file analysis
Run of systems produces lots of observations
What we can verify?
◦ Is it correct?
◦ Does it have the necessary performance, reliability, scalability, security?
◦ Output is correct accordingly with the input?
◦ The hardware components are used properly?
◦ Usability is respected?
Each of these questions is a property that
needs to be checked
20
Direct observation for simple traces of events
◦ Programmer, tester on a small data volume
◦ Comparison between expected and obtained
Custom checker
◦ Start from simple scripts (Perl, Python, Java script)
◦ We can check the correspondence between values, if the values belonging to a domain, the QoS
◦ We can use monitors, logs, aspects
Checker for a suitable property specification language
◦ Can be formal: use the formal semantics for checking the satisfaction
22
DeLap, M., et al., “Is runtime verification applicable to cheat detection?”, Proc. ACM NetGames '04, pp. 134- 138, 2004
The main idea: Game implementation bugs are extensively exploited by cheaters, especially in massively multiplayer games
With JavaMaC runtime verification the authors show how they identify a transaction bug
Bodden, E.: J-LO, the Java Logical Observer - A tool for runtime-checking temporal assertions
24
Designed at U. Penn since 1998
Components:
◦ Architecture for run-time verification
◦ Languages for monitoring properties and trace abstraction
◦ Steering in response to alarms
Prototype implementation
◦ Implementation of checking algorithms
◦ Recognition of high-level events
For Java programs: automatic instrumentation
26
PEDL (Primitive Event Definition Language) – abstraction
MEDL (Meta Event Definition Language) – abstract transformation
SADL (Steering Action Definition Language) –
feedback
J-LO , the Java Logical Observer , is a tool for runtime-checking temporal assertions in Java 5 applications
Temporal properties can be specified using a linear time logic (LTL) over AspectJ pointcuts
Specification takes place right in the source code in the form of Java 5 annotations
The work is based on a Haskell-prototype
28
At design time - The software architect should
formulate temporal interdependencies (TID) between events in a formal way, best in LTL (linear temporal logic)
At implementation time - the programmers annotate their source code with LTL. They use J-LO as an
additional tool in their build chain to instrument the application under test.
At testing time - the instrumented application will emit an error message whenever one of the temporal assertions is falsified or verified
At deployment time - J-LO is simply removed from the build chain
Syntax Arity Semantics
X 1 LTL operator Next * F 1 LTL operator Finally G 1 LTL operator Globally U 2 LTL operator Until R 2 LTL operator Release
! 1 logical not
&& 2 logical and
|| 2 logical or
-> 2 logical implies: f1 -> f2 = !f1 || f2
<-> 2 logical if and only if: f1 <-> f2 = (f1 -> f2) &&
(f2 -> f1)
30
For each object of a type T, after a constructor has been called, its tearDown method is called before it is garbage collected and no method is called
afterwards on this object T t1, T t2:
G( (
exit( call( T.new(..) ) ) returning t1 ) -> (
F( (
entry( call( * T.tearDown() ) && target(t2) && if( t1==t2 ) ) ) && (
G( !(
entry( call( * T.*() ) && target(t2) && if( t1==t2 ) )
) ) ) )
) )
Monitoring-Oriented Programming
32
The observation mechanism extracts property relevant and filtered system states at designated points, e.g., when property-specific events happen
The verification mechanism checks the obtained
abstract trace against the (monitor corresponding to the) property and triggers desired actions in case of violations or validations
Example: for global property “always (x > 0)”
Observation mechanism – is related to updates of the variable x and the relevant state information (or
snapshot) to extract is the value of x => a sequence of values of x
Verification mechanism - checks whether the value of x is larger than zero
=> Observation and verification are independent
34
/*@
scope = class logic = ERE
{
[static int counter = 0; int writes = 0;]
event open : end(call(* open(..))) {writes = 0;};
event write : end(call(* write(..))) {writes ++;} ; event close : end(call(* close(..)));
formula : (open write+ close)*
}
violation handler{ @RESET; }
validation handler{ synchronized(getClass()){
File.log((++counter) + ":" + writes); } }
@*/
MOP specification for file profiling
/*@
scope = global logic = ERE
SafeEnum (Vector v, Enumeration+ e) { [String location = "";]
event create<v,e>: end(call(Enumeration+.new(v,..))) with (e);
event updatesource<v>: end(call(* v.add*(..))) \/
end(call(* v.remove*(..))) \/ ...
{location = @LOC;}
event next<e>: begin(call(* e.nextElement()));
formula : create next* updatesource+ next
}
validation handler { System.out.println("Vector updated at "
+ @MONITOR.location); }
36
Authentication before use
Execution 1, correct
authenticate
begin end
use
begin end
Execution 2, incorrect
class Resource { /*@
class-scoped SafeUse() {
event authenticate : after(exec(* authenticate())) event use : before(exec(* access()))
ptltl : use -> <*> authenticate }
@*/
void authenticate() {...}
void access() {...}
...
}
38
Enforce authentication before use
Execution 1, correct
authenticate
begin end
use
begin end
Execution 2, incorrect but corrected
Call
authenticate()
Enforce authentication before use
class Resource { /*@
class-scoped SafeUse() {
event authenticate : after(exec(* authenticate())) event use : before(exec(* access()))
ptltl : use -> <*> authenticate
violation { @this.authenticate(); } }
@*/
void authenticate() {...}
void access() {...}
40
JavaMOP is an MOP development tool for Java
JavaMOP follows a client-server architecture
◦ The client part includes the interface modules and the JavaMOP specification processor
◦ The server part contains a message dispatcher and logic-plugins for Java
The specification processor employs AspectJ for monitor integration => JavaMOP translates
outputs of logic-plugins into AspectJ code
Map SafeEnum_v_map = makeMap();
pointcut SafeEnum_updatesource0(Vector v) : call(* Vector.add*(..))&& target(v);
after (Vector v) : SafeEnum_updatesource0(v) { Map m = SafeEnum_v_map;
Object obj = null;
obj = m.get(v);
if (obj != null){
Iterator monitors = ((List)obj).iterator();
while (monitors.hasNext()) {
SafeEnumMonitor monitor=(SafeEnumMonitor)monitors.next();
monitor.updatesource(v);
if (monitor.suceeded()) {//validation handler }
}//end of while
42
1st conference on Runtime Verification: http://www.rv2010.org/
J-LO: http://www.sable.mcgill.ca/~ebodde/rv//JLO/index.html
SOA: http://msdn.microsoft.com/en-us/library/aa480021.aspx
AOP Introduction: http://sewiki.iai.uni-
bonn.de/_media/teaching/labs/xp/2007b/aop_intro.pdf
Strategies in AOP:
http://www.guzzzt.com/files/coding/aspect_strategies.pdf
DeLap, M., et al.: Is Runtime Verification Applicable to Cheat Detection?
http://www.comp.nus.edu.sg/~bleong/hydra/related/delap04runtim e.pdf
Sokolsky, O.: Run-time verification, 2006,
http://www.cis.upenn.edu/~alur/CIS673/mac.pdf
Chen, F., Roșu, G. MOP: An Efficient and Generic Runtime Verification Framework. OOPSLA’07, ACM press, pp 569-588, 2007
Ghoshal, S., Manimaran, S., Rosu, G., Serbanuta, T., Stefanescu, G.:
Monitoring IVHM Systems using a Monitor-Oriented Programming Framework, 2008
http://shemesh.larc.nasa.gov/LFM2008/slides/Session2/Rosu.ppt