• Nu S-Au Găsit Rezultate

Runtime Verification

N/A
N/A
Protected

Academic year: 2022

Share "Runtime Verification "

Copied!
43
0
0

Text complet

(1)

Curs 7 – 22 Noiembrie 2010 Adrian Iftene [email protected]

(2)

Recapitulation courses 5-6

AOP

Runtime verification

MOP

AOP

Runtime Verification

MOP

2

(3)

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)

4

Java Code Aspect

public class Student { public aspect StudentAspect {

ajc compiling

public class WeavedStudent {

(5)

Concern

Crosscutting concern

Aspect

Join Points

Pointcuts

Advice

Introductions (Inter-type declaration)

(6)

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

(7)

How do you explain the result below?

(8)

8

(9)
(10)

10

(11)

+ 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)

12

(13)
(14)

14

(15)

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)

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.

(17)

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)

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

(19)

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)

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

(21)
(22)

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

(23)

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)

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

(25)
(26)

26

PEDL (Primitive Event Definition Language) – abstraction

MEDL (Meta Event Definition Language) – abstract transformation

SADL (Steering Action Definition Language) –

feedback

(27)

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)

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

(29)

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)

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 ) )

) ) ) )

) )

(31)

Monitoring-Oriented Programming

(32)

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

(33)

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)

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

(35)

/*@

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)

36

Authentication before use

Execution 1, correct

authenticate

begin end

use

begin end

Execution 2, incorrect

(37)

class Resource { /*@

class-scoped SafeUse() {

event authenticate : after(exec(* authenticate())) event use : before(exec(* access()))

ptltl : use -> <*> authenticate }

@*/

void authenticate() {...}

void access() {...}

...

}

(38)

38

Enforce authentication before use

Execution 1, correct

authenticate

begin end

use

begin end

Execution 2, incorrect but corrected

Call

authenticate()

(39)

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)

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

(41)

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)

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

(43)

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

Referințe

DOCUMENTE SIMILARE

The worst-case analysis yields an upper bound on the running time of an algorithm over all input instances.. Let T (i), i = 1, ..., k, the running time of the execution of line

According to our algorithm described above, the money cost needed to complete the project is based on the execution time for each task, the number of employees assigned to that task

Significant applications of texture analysis include medical image analysis [140], analysis of satellite images [141], segmentation, content-based image retrieval [142],

To handle multiple data types, the definition of what constitutes a legal parse tree has a few additional criteria beyond those required for standard genetic programming, which are:

The working method was used in human medicine by Gamal (2004) and Gheban (2005) and was adapted in phytopathology in this study with the purpose of quanti- fying growth

Thus, there are articles who analyse if and how fundamental analysis and technical analysis can predict prices variations, other studies who investigate the

event privateKeyLoad after(ASPECipher cipher, PrivateKey pKey) : call(public void loadPrivateKey(PrivateKey) throws *Exception ) &amp;&amp; args(pKey) &amp;&amp; target (cipher)

 An important class of model checking methods are specified using temporal logic formulas.  Temporal logic – a formula is not true or false in a static way in