A Formal Monitoring-based Framework
for Software Development and Analysis
Feng Chen
Marcelo D'Amorim
Grigore Rosu
University of Illinois at Urbana-Champaign
1
Motivation :
Increase Software Reliability
Traditional formal verification methods
High confidence, do not always scale up well
Testing
Scalable, but adhoc, no correctness guarantees
What do we really want … ?
A.Prove a program correct?
B.Correct execution!
A => B … but isn’t the price too big?
2
Overview
•
•
•
•
•
Monitoring Software Systems
Monitoring-Oriented Programming (MOP)
Java-MOP
An HTTP-Server Example
Conclusion and Future Work
3
Avoiding Complexity while
Ensuring Safety by Monitoring
(Example by Lui Sha - Simplex)
Joe is a student in an algorithms class
Final exam is to develop a sorting algorithm
If incorrect then Joe fails the class
If provably correct but inefficient then he gets B
If both correct and efficient then he gets A
Hm, heap sort is efficient but hard to
prove correct; insertion sort is trivial to
prove correct but it is not efficient
4
Joe’s Solution
Heap
sort
Monitor if
vector is
sorted
O(n log(n))
yes
no
Insertion
sort
O(n2)
provably
correct
O(n)
Joe has an efficient and provably correct sorting algorithm!
He avoided proving heap sort correct, which is hard!
5
Monitoring in Engineering
Most engineering disciplines take monitoring
as basic design principle
Fire alarms in buildings
Fuses in electronics
Watchdogs in hardware
Why not to do the same in software eng.?
Monitoring-oriented programming
6
Monitoring-Oriented Programming (MOP)
Proposed at RV 2003
Monitoring already used in software development
Design By Contract, Runtime Verification (MaC, PaX, …)
MOP underlying motivations and challenges
• Can one generically and formally capture the
various approaches to monitoring and runtime
verification in a unified manner?
• Monitoring should be a design and software
development principle. Write programs having
monitoring in mind!
7
What are the foundational
principles of monitoring programs?
Program
3. Recovery
Specification
S1 S2
.....
Sn
1. Observation
2. Checking
8
Goal of MOP
The different approaches to RV rely on implicit,
carefully chosen instance of the 3 principles
1.
2.
3.
Observation
Checking
Recovery
MOP aims at separation and individual advancement
of the three principles
Three ways to look at MOP
1.
2.
3.
Merging specification and implementation
Extending languages with logic-based statements
A light weighted formal method
9
MoP Example:
A traffic light monitor
Following monitor can appear in a Java program
...
/*@ logic=FTLTL {
predicate red = tlc.state.getColor() == 1;
predicate green = tlc.state.getColor() == 2;
predicate yellow = tlc.state.getColor() == 3;
formula : []( green -> (! red U yellow));
Violation handler : … any code
}
@*/
...
It is pre-compiled into actual Java code
...
switch(bttFsmState) {
case -1 : break;
case 1 : bttFsmState = tlc.state.getColor()==3 ?
tlc.state.getColor()==2 ?
tlc.state.getColor()==1
break;
case 2 : bttFsmState = tlc.state.getColor()==3 ?
tlc.state.getColor()==1
break;
}
if(bttFsmState == 0) { … the “recovery” code …}
}
...
1 :
? 0 : 2 : 1;
1 :
? 0 : 2;
10
MoP Features and
Design Principles
11
Extending Languages with Logics
• Do not modify host languages
– Able to reuse heritage systems
– Evolve with languages and compilers
• Specifications can be
– Annotations in the source code
• Especially for checkpoints
– In separated specification files
• Separation of concerns
• Improved reusability
12
MOP Specification Syntax
Definition
/************** Heading starts ****************/
[attribute]* <Type> <Name> logic= <Logic
Name> {
/************* Body starts ********************/
... Specification Body ...
/************* Handler starts *****************/
[Violation Handler: ...handling the violation...]
[Validation Hander: ...handling the validated...]
}
Example
class-inv logic = ERE {
var int flag = -1;
event suspend: called(void suspend()) {flag = 1;};
event resume: called(void resume()) {flag = 2;};
formula: (suspend resume)*
Violation Handler:
if (flag == 2) {
System.out.println("resume() called before
suspend()
in HttpClient! Adding client back to queue ...");
synchronized(suspendedClients){
suspendedClients.add(thisObject);
}
} else {
System.out.println("suspend() called twice before
resume() in HttpClient!");
}
13
}
MOP Specification Syntax
• Attributes
– static, inline/outline, sync/async
• Types of specifications:
– class invariants, interface constraints, method
pre-post conditions, checkpoints.
• User-defined handlers
– Violation and/or validation handlers
• Not all combinations always possible
14
Sorting Example
method (HeapSort(int[] a))
logic=JML {
ensures isOrdered(a);
Violation handler:
InsertionSort(a);
}
…
if (! isOrdered(a)){
InsertionSort(a);
}
…
15
Security Example
class-inv logic=ERE {
event auth = authentication();
event use = accessResource();
formula: (! auth)* use;
Validation handler:
authentication();
}
switch ($state) {
case 0 : $state = use ? 1 : ! auth ? 0 : -1;
break;
}
if ($state == 1)
authentication();
16
Extensible Logic Framework
17
Workflow of MOP
18
Logic Plug-ins
• No silver-bullet logic to express any requirements
• To add a new MOP requirements formalism, all
one needs to do is to provide a logic plug-in
– Logic plug-in consists of a language shell and a logic
engine; several logic plug-ins can share a logic engine
• The I/O of the logic plug-in is standardized to
facilitate extensibility
• Logic plug-in encodes a monitor synthesis
algorithm: formula -> monitor
• WWW repository of logic plug-ins
fsl.cs.uiuc.edu/mop
19
Current Logic plug-ins
• Linear Temporal Logic (LTL)
– Past Time LTL
– Future Time LTL
• Extended Regular Expressions (ERE)
• Design By Contract: Jass, JML (partly)
• To be supported:
– RTL, MTL, …
– Users can easily add new logics via provided
standardized interface
20
Future time LTL plug-in
Input:
[] (green -> (! red) U yellow)
Output:
Algorithm jointly
with Havelund
(RV’01)
Declaration.
int state;
Initialization.
state = 1;
Monitoring Body.
switch (state) {
case 1 : state = yellow ? 1 : green ? (red ? -1 : 2) : 1;
case 2 : state = yellow ? 1 : red ? -1 : 2;
}
Failure Condition.
state == -1
21
Past time LTL plug-in
Input:
start(P) -> [Q, end(R \/ S))
Output:
Algorithm jointly
with Havelund
(TACAS’02)
Declaration.
boolean now[3], pre[3]
Initialization.
now[3] = R || S;
now[2] = Q;
now[1] = P;
Monitoring Body.
now[3] = R || S;
now[2] = (pre[2] || Q) && (now[3] || (! pre[3]));
now[1] = P;
Failure Condition.
now[1] && (! pre[1]) && (! now[2])
22
Extended RE plug-in
Input:
~((~ empty)(green red)(~ empty))
Output:
Algorithm jointly
with Sen (RV’03)
Declaration.
int state;
Initialization.
state = 0;
Monitoring Body.
switch (state){
case 0 : state = (yellow || red) ? 0 : green? 1 : -1;
case 1 : state = green ? 1 : yellow ? 0 : -1;
}
Failure Condition.
state == -1
23
Java-MOP
A prototype supporting part of the desired
MOP features in Java
24
Java-MOP Overview
• Provides GUI and command-line interfaces
– Online interface: http://fsl.cs.uiuc.edu/mop
• Supports FTLTL, PTLTL, ERE, Jass, JML
• Uses AspectJ for monitor integration
– Limitations
• Can only monitor scalar fields of classes for class
invariants
• The event generation and analysis are not atomic
25
Java-MOP Architecture
26
Java-MOP at Work
A buggy HTTP server
- taken from an IBM repository of
buggy concurrent Java programs
27
28
Request access to the server
No
Yes
Granted?
1
work
Get a client from the waiting queue,
and resume it
3
Put itself into the waiting queue
2
suspend itself
Exit
29
Clienti
Clientj
SuspendedClients
Clienti
1
add
Stopped
2
suspend
Has been
removed from
the waiting
queue!
3
remove &
resume
Exit
30
A bad trace
31
The Bug
• Caused by “unexpected” thread interleaving
– Not easy to analyze and test
• Root cause
– Violation of the basic assumption for suspend()
and resume(): (suspend() resume())*
• Can we fix it on-the-fly in case of violation?
• Yes: put the client back into the queue to
allow another client to resume it later.
32
33
Trace with Monitor
34
Conclusion and Future Work
• MOP: a uniform logic-independent monitoring
framework.
• Java-MOP: a prototype for Java
• Incorporate more logics/paradigms, especially
those that are widely accepted
– Complete JML, RTL, MTL, …
– WWW repository of logic plug-ins
• Turn Java-MOP into a mature tool
– Currently a prototype
– Use it on real and large applications
• Support more programming languages
35
Descargar

Towards Monitoring-Oriented Programming