Transcript Runtime Verification using LARVA

POLYLARVA
Technology Agnostic
Runtime Verification
A System’s Behaviour
Testing
Model Checking
Runtime Verification
Inputs to Runtime Verification
System
•No more than 10 users can
be logged onto the system at
any one time
•A user cannot execute more
than 3 failed transactions in
one session
•A user which has been idle
for more than 5 minutes
should be logged out
Creating a Runtime Monitor
Creating a Runtime Monitor
Creating a Runtime Monitor
Creating a Runtime Monitor
Creating a Runtime Monitor
The LARVA Architecture
LARVA – JAVA Specific
Property to be verified : New accounts can be added for a User if the User settings allow
It. Otherwise this should be disallowed.
before ( User u1) : (call(* User.addAccount(..)) && target(u1)
&& !cflow(adviceexecution())) {
Monitor monitor_instance = getMonitorInstance(u1);
monitor_instance.call(thisJoinPoint.getSignature().toString(),
8/*addAccount*/);
}
LARVA – JAVA Specific
Property to be verified : New accounts can be added for a User if the User settings allow
It. Otherwise this should be disallowed.
if
((_occurredEvent(_event,8/*addAccount*/))
&& (!u .canAddAccounts ())){
_state_id_account = 5;//moving to state
cannotadd
_goto_account(_info);
}
LARVA – JAVA Specific
Property to be verified : New accounts can be added for a User if the User settings allow
It. Otherwise this should be disallowed.
if
((_occurredEvent(_event,8/*addAccount*/))
&& (!u .canAddAccounts ())){
_state_id_account = 5;//moving to state
cannotadd
_goto_account(_info);
}
Goals for PolyLARVA
1) Improve LARVA framework to become a
customisable monitoring architecture supporting
potentially numerous platforms and technologies
System
(Any Language)
Generated
Monitor
Notifies monitor when specific
Events take place
Evaluates monitoring logic
The PolyLARVA Specification Language
• The PolyLarva specification language proposed
is an ECA (Event-Condition-Action) rule-based
language
rule name : event \ condition  action
ruleAddAccnt: addAccount(u2, a) \ isTooManyAccts ->
logTooMany;
The PolyLARVA Specification Language
ruleAddAccnt: addAccount(u2, a) \ isTooManyAccts ->
logTooMany;
states {
int accountCnt
}
conditions{
isTooManyAccts = {accountCnt > 5;}
}
The PolyLARVA Specification Language
ruleAddAccnt: addAccount(u2, a) \ isTooManyAccts ->
logTooMany;
states {
int accountCnt
}
conditions{
isTooManyAccts = {accountCnt > 5;}
}
actions {
logTooMany = {System.out.println("Account limit
of 5 exceeded.");}}
}
Evaluating Conditions & Actions
ruleAddUser: addUser( ) \ usercount > 5  logTooManyUsers
Monitor
Keep Integer count of users in system usercount
Increment counter on new user
addition.
Compare this counter against a set
limit on every new user addition
Log warning message
addUser()
System
Evaluating Conditions & Actions
ruleAddUser: addAccount( User u ) \ u.canAddAccounts() logNewAccount
u.canAddAccounts()
Monitor
System
addAccount(User u)
canAddAccounts is a property of a
User Instance
Monitor must refer to system to obtain
evaluation of condition
Evaluating Conditions & Actions
ruleAddUser: addAccount( User u ) \ u.canAddAccounts() logNewAccount
u.canAddAccounts()
Monitor
canAddAccounts is a property of a
User Instance
Monitor must refer to system to obtain
evaluation of condition
System
System vs Monitor
Conditions & Actions
Monitor
System
Monitor Side
System Side
Can be evaluated by monitor – no
reference to system specific properties
Must be evaluated on the system –
reference variables and methods declared
in system code
Must be written in JAVA code
Must be written in system language
conditions {
monitorSide {
isTooManyAccts = {accountCnt > 5;}
}
}
conditions {
systemSide {
cannotAddAccts =
{return !user.canAddAcounts();}
}
}
The PolyLARVA Architecture
Phase 1: Creation of JAVA code which covers the monitor logic for validating properties
The PolyLARVA Architecture
Phase 2: Creation of code which will be used to instrument the system code
Creation of ‘Aspect’ code
The PolyLARVA Architecture
Phase 2: Creation of code which will be used to instrument the system code
Creation of code that adds monitor logic on system side
The PolyLARVA Architecture Communication
Communication between Monitor and Instrumented System via Sockets
The PolyLARVA Language Specific
Compiler
Generation of ‘Aspect’ Code
Aspect Code
• The Runtime Monitor must be aware of any events,
relevant to monitoring, that occur on the system
• Aspect Programming is ideal for use in Runtime
Monitoring systems
• Can support a large number of programming
languages , though not all
Generation of JAVA ‘Aspect’ Code
Aspect Code
Event Specification
addAccount(User u2, Account a) = {execution Account a.new(User u2)}
Context_Aspect.aj
before(Account a,User u2):target(a) && execution(Account.new(..))
&& args (u2)&& !cflow(adviceexecution()){
LarvaCommClient.getClientConnection().sendMessage(
LarvaCommClient.ASPECT_EVENT, 5,
UniqueIDGenerator.getIdentifier(a)+","+
UniqueIDGenerator.getIdentifier(u2)+",");
}
What if our system program is written
in PERL?
Aspect Code
Event Specification
addAccount(User u2, Account a) = {execution Account a.new(User u2)}
Context_Aspect.pl
PERL Aspect Code
[uses Aspect.pm]
Uses socket connection
to communicate with
monitor
Generation of Monitor ‘Helper’ Code
(System Side)
Helper Code
conditions{
systemSide {
cannotAddAccts =
}
} %%conditions
{!user.canAddAcounts();}
System side code
copied verbatim to
generated code.
Helper code becomes
part of System.
PolyLARVA – A Flexible Runtime
Monitoring System
QDDC
JAVA
C++
C#
PERL
...
Counterexample
Formulas
LUSTRE
DATEs

RuleBased
PolyLARVA – A Flexible Runtime
Monitoring System
QDDC
JAVA
C++
C#
PERL
...

Counterexample
Formulas

LUSTRE

DATEs

RuleBased
PolyLARVA – A Flexible Runtime
Monitoring System
QDDC
JAVA
C++
C#
PERL
...

Counterexample
Formulas

LUSTRE

DATEs

RuleBased

PolyLARVA – A Flexible Runtime
Monitoring System
QDDC
JAVA
C++
C#
PERL
...

Counterexample
Formulas

LUSTRE

DATEs

RuleBased




...
Future Work on PolyLARVA Runtime
Monitor
• Implementation of other Language Specific
Compilers
• Implementation of translator for specification
in DATEs format to new PolyLarvaspecification
• Analysis of specification script for optimisation
of rules
• Ability to save and load Monitor state
• Any more?
POLYLARVA Technology Agnostic Runtime Verification
THE END