Modeling Web Services by Iterative Reformulation of Functional and
Non-Functional Requirements
Jyotishman Pathak, Samik Basu and Vasant Honavar
Abstract:
We propose an approach for incremental modeling of composite Web
services. The technique takes into consideration both the functional and nonfunctional
requirements of the composition. While the functional requirements
are described using symbolic transition systems augmented
with state variables, function invocations, and guards; non-functional requirements
are quantified using thresholds. The approach allows users to specify an
abstract and possibly incomplete specification of the desired service (goal) that
can be realized by selecting and composing a set of pre-existing services. In the
event that such a composition is unrealizable, i.e. the composition is not functionally
equivalent to the goal or the non-functional requirements are violated,
our system provides the user with the causes for the failure, that can be used to
appropriately reformulate the functional and/or non-functional requirements of
the goal specification.
Full Paper
Parallel Web Service Composition in MoSCoE: A Choreography-based Approach
Jyotishman Pathak, Samik Basu, Robyn Lutz and Vasant Honavar
Abstract:
We present a goal-driven approach to model a choreographer
for realizing composite Web services. In this framework,
the users start with an abstract, and possibly incomplete
functional specification of a desired goal service. This
specification is used to compose a choreographer that allows
communication between the client and the set of available
component services, and is functionally equivalent to
the goal service. However, if such a composition cannot be
realized, the proposed approach identifies the cause(s) for
the failure of composition. This information can be used
by the user to minimally reformulate the goal to reduce the
gap between the desired functionality. The process can be
iterated until a feasible composition is realized or the user
decides to abort. The approach ensures that (i) a choreographer,
if one is produced by our composition algorithm,
in fact realizes the user-specified goal functionality; and (ii)
the algorithm is guaranteed to find a composition that meets
the user needs as captured in the goal specifications (whenever
such a composition exists.
Full Paper
Selecting and Composing Web Services through Iterative Reformulation of Functional
Specifications
Jyotishman Pathak, Samik Basu, Robyn Lutz and Vasant Honavar
Abstract:
We propose a specification-driven approach to Web service
composition. The proposed framework allows users
to start with a high-level, possibly incomplete specification
of a desired (goal) service that is to be realized using
a subset of the available component services. These services
are represented by the system using transition systems
augmented with guards over variables with infinite domains
and are used to determine a strategy for their composition
that would realize the goal service. In the event that the
goal service cannot be realized using the available services,
the system identifies the cause(s) for such failure which can
then be used by the developer to reformulate the goal specification.
Thus, the system supportsWeb service composition
through iterative refinement of the functional specifications.
We present a prototype implementation in tabled-logic programming
environment that illustrates the key features of
the proposed approach.
Full Paper
Modeling Web Service Composition using Symbolic Transition Systems
Jyotishman Pathak, Samik Basu and Vasant Honavar
Abstract:
Web services are software entities which provide a set of
functionalities that can be accessed over the Web. In general,
the valuations of variables appearing in various functions
provided by the service are not known before execution.
Consequently, to analyze the behavior of a service, all
possible valuations need to be considered, making the whole
system infinite-state. Against this background, we propose a
framework for modeling and composing Web services where
desired (goal) and pre-existing (component) services exhibit
infinite-state behavior. Our approach finitely represents such
services using Symbolic Transition Systems (STSs) which
are transition systems augmented with guards over infinitedomain
variables. We develop a sound and complete logical
approach for identifying the existence of composition of
available component-STSs, such that the resulting composition
is “simulated” by the goal-STS. In the event that the goal
service cannot be realized from the existing components, our
technique can also identify the cause for the failure and guide
the user to achieve appropriate refinement of the goal specification,
thereby paving the way for incremental development
of composite services.
Bibtex Entry:
@inproceedings{PBH:AAAI06,
author = {Jyotishman Pathak and Samik Basu and Vasant Honavar},
title = {Modeling Web Service Composition using Symbolic Transition Systems},
booktitle = {AAAI Workshop on AI-Driven Technologies for Service-Oriented Computing},
year = {2006}}
Full Paper
MoSCoE: A Framework for Modeling Web Service Composition and Execution
Jyotishman Pathak, Samik Basu, Robyn Lutz and Vasant Honavar
Abstract:
Development of sound approaches and software tools
for specification, assembly, and deployment of composite
Web services from independently developed components
promises to enhance collaborative software design
and reuse. In this context, the proposed research
introduces a new incremental approach to service composition,
MoSCoE (Modeling Web Service Composition
and Execution), based on the three steps of abstraction,
composition and refinement. Abstraction refers to the
high-level description of the service desired (goal) by the
user, which drives the identification of an appropriate
composition strategy. In the event that such a composition
is not realizable, MoSCoE guides the user through
successive refinements of the specification towards a realizable
goal service that meets the user requirements.
Bibtex Entry:
@inproceedings{PBLH:ICDE06,
author = {Jyotishman Pathak and Samik Basu and Robyn Lutz and Vasant Honavar},
title = {MoSCoE: A Framework for Modeling Web Service Composition and Execution},
booktitle = {Workshop at IEEE International Conference on Data Engineering},
year = {2006}}
Full Paper
Quotient-based Control Synthesis for Non-Deterministic Plants with
Mu-Calculus Specifications
Samik Basu and Ratnesh Kumar
Abstract:
We study the control of a nondeterministic discrete event system (DES)
subject to a control specification expressed in the propositional
mu-calculus, under complete observation of events. Given a plant
automaton model and a mu-calculus specification we provide a set of
rules that computes the ``quotient'' of the specification against the
plant, which is another mu-calculus formula such that a supervisor
exists if and only if the quotiented formula is satisfiable. Thus the
control problem is reduced to one of mu-calculus satisfiability. We
also present a tableau-based satisfiability solving algorithm that
identifies a model for the quotiented formula. The resulting model
serves as a supervisor. The complexity of supervisor existence
verification as well as model synthesis is single exponential in the
size of the plant as well as the size of the specification formula.
BibTex Entry:
@inproceedings{BK06,
author = {Samik Basu and Ratnesh Kumar},
title = {Quotient-based Control Synthesis for Non-Deterministic Plants with
Mu-Calculus Specifications}
booktitle = {Conference on Decision and Control}
year = {2006}
}
Full Paper
Finite Bisimulation of Reactive Untimed Infinite State Systems Modeled as Automata with
Variables
Ratnesh Kumar, Changyan Zhou and Samik Basu
Abstract:
Some discrete event systems such as software
are typically infinite state systems, and a commonly used
technique for performing formal analysis such as automated
verification is based on their finite abstractions. In this paper,
we consider a model for reactive untimed infinite state systems
called input-output extended finite automaton (I/O-EFA), which
is an automaton extended with discrete variables such as inputs,
outputs, and data. Using I/O-EFA as a model many valuepassing
processes can be represented by finite graphs. We study
the problem of finding a finite abstraction that is bisimilar
to a given I/O-EFA. We present a sufficient condition under
which the underlying transition system of an I/O-EFA admits a
finite bisimilar quotient. This sufficient condition is existential
as it relies on the existence of a suitable partition of the
state space. We then identify a class of I/O-EFAs for which a
partition satisfying our sufficient condition can be constructed
by inspecting the structure of the given I/O-EFA.
BibTex Entry:
@inproceedings{BK06,
author = {Ratnesh Kumar and Changyan Zhou and Samik Basu},
title = {Finite Bisimulation of Reactive Untimed Infinite State Systems Modeled as Automata with
Variables},
booktitle = {American Control Conference}
year = {2006}
}
Full Paper
Local Module Checking for CTL specifications
Samik Basu, Partha S. Roop and Roopak Sinha
Abstract:
Model checking is a well known technique for the verification of
finite state models using temporal logic specification. While model
checking is suitable for transformational systems (also called closed
systems), it is unsuitable for open systems (also known as
reactive systems) where the nondeterminism in the environment must be
considered during verification. Module checking is an approach
for the verification of open systems which have both closed (internal)
and open (environment or external) states. It has been demonstrated in
[Kupferman et al 2001] that the complexity of module checking branching time
logic CTL is EXPTIME-complete. The approach to module checking is
global and the method tries to establish that the property in question
holds over all possible environments.
This papers develops a local approach to CTL module checking using
tableau rules. The proposed approach tries to determine a single
environment under which the negation of the property is satisfied over
the given module. Such a strategy, thus, leads to a local approach to
module checking where we only explore states that are relevant to
proving that the negation of the property can be satisfied over the
given module using an appropriate witness (environment) that the
algorithm also generates. While the worst case complexity of our
algorithm is identical to the earlier complexity, we demonstrate that
practical implementation of the proposed approach is feasible and
yields much better results than the global approach.
Bibtex Entry:
@inproceedings{BRS:FESCA06,
author = {Samik Basu and Partha S. Roop and Roopak Sinha},
title = {Local Module Checking for CTL Specifications},
booktitle = {Workshop on Formal Foundations of Embedded Software and Component-Based Software Architectures},
year = {2006}}
Full Paper
Parameterized Verification of Pi-Calculus Systems
Ping Yang, Samik Basu and C.R. Ramakrishnan
Abstract: In this paper we present an automatic verification
technique for pa- rameterized systems where the subsystem behavior is
modeled using the - calculus. At its core, our technique treats each
process instance in a system as a property transformer. Given a
property that we want to verify of an N-process system, we use a
partial model checker to infer the property (stated as a for- mula in
a sufficiently rich logic) that must hold of an (N - 1)-process
system. If the sequence of formulas thus constructed
converges, and the limit is satisfied by the deadlocked process, we
can conclude that the N-process system satisfies . To this end, we
develop a partial model checker for the -calculus that uses an
expressive value-passing logic as the property language. We also
develop a number of optimizations to make the model checker efficient
enough for routine use, and a light-weight widening operator to
accelerate convergence. We demon- strate the effectiveness of our
technique by using it to verify properties of a wide variety of
parameterized systems that are beyond the reach of existing
techniques.
BibTex Entry:
@inproceedings{YBR06,
author = {Ping Yang and Samik Basu and C.R. Ramakrishnan},
title = {Parameterized Verification of Pi-Calculus Systems},
booktitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems ({TACAS})},
address = {Vienna, Austria},
month = {April},
year = {2006}
}
Full Paper
Compositional Analysis for Verification of Parameterized Systems
Samik Basu and C.R. Ramakrishnan
Abstract: Many safety-critical systems that have been
considered by the verification community are parameterized by the
number of concurrent components in the system, and hence describe an
infinite family of systems. Traditional model checking techniques can
only be used to verify specific instances of this family. In this
paper, we present a technique based on compositional model checking
and program analysis for automatic verification of infinite families
of systems. The technique views a parameterized system as an
expression in a process algebra (CCS) and interprets this expression
over a domain of formulas (modal mu-calculus), considering a process
as a property transformer. The transformers are constructed using
partial model checking techniques. At its core, our technique solves
the verification problem by finding the limit of a chain of
formulas. We present a widening operation to find such a limit for
properties expressible in a subset of modal mu-calculus. We describe
the verification of a number of parameterized systems using our
technique to demonstrate its utility.
BibTex Entries:
@inproceedings{BR03,
author = {Samik Basu and C. R. Ramakrishnan},
title = {Compositional Analysis for Verification of Parameterized Systems},
booktitle = {Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems ({TACAS})},
address = {Warsaw, Poland},
month = {April},
series = {Lecture Notes in Computer Science},
volume = {2619},
publisher = {Springer},
pages = {315--330},
year = {2003}
}
Full Paper
@article{BR:TCS06,
author = {Samik Basu and C. R. Ramakrishnan},
title = {Compositional Analysis for Verification of Parameterized Systems},
journal = {Theoretical Computer Science (TCS)},
volume = {354},
number = {2},
pages = {211--229},
year = {2006}
}
Full Paper
Resource Constrained Model Checking for Push-down Systems
Samik Basu, K. Narayan Kumar, Robert L. Pokorny and C.R. Ramakrishan
Abstract: A number of recent papers present efficient
algorithms for LTL model checking for recursive programs with finite
data structures. A common feature in all these works is that they
consider infinitely long runs of the program without regard to the
size of the program stack. Runs requiring unbounded stack are often a
result of abstractions done to obtain a finite-data recursive program.
In this paper, we introduce the notion of resource-constrained model
checking where we distinguish between stack-diverging runs and
finite-stack runs. It should be noted that finiteness of stack-like
resources cannot be expressed in LTL.
We develop resource-constrained model checking in terms of good cycle
detection in a finite graph called RC-automaton, which is constructed
from a given push-down system (PDS) and a Buchi automaton. We make
the formulation of the model checker ``executable'' by encoding it
directly as Horn clauses. We present a local algorithm to detect a
good cycle in an RC-automaton. Furthermore, by describing the
construction of RC-automaton as a logic program and evaluating it
using tabled resolution, we do model checking without materializing
the push-down system or the induced RC-automaton. Preliminary
experiments indicate that the local model checker is at least as
efficient as existing model checkers for push-down systems.
BibTex Entry:
@inproceedings{BKPR02,
author = {Samik Basu and K. Narayan Kumar and L. Robert Pokorny and C. R. Ramakrishnan},
title = {Resource-Constrained Model Checking of Recursive Programs},
booktitle = {Eighth International Conference on Tools and Algorithms for the Construction and Analysis of Systems ({TACAS})},
address = {Grenoble, France},
month = {April},
series = {Lecture Notes in Computer Science},
volume = {2280},
publisher = {Springer},
pages = {236--250},
year = {2002}
}
Full Paper
Local and Symbolic Bisimulation using Tabled Constraint Logic Programming
Samik Basu, C.R. Ramakrishan, I.V. Ramakrishnan, M. Mukund and R.M. Verma
Abstract: Bisimulation is a fundamental notion that
characterizes behavioral equivalence of concurrent systems. In this
paper, we study the problem of encoding efficient bisimulation
checkers for finite- as well as infinite-state systems as logic
programs. We begin with a straightforward and short (less than 10
lines) encoding of finite-state bisimulation checker as a tabled logic
program. In a goal-directed system like XSB, this encoding yields a
local bisimulation checker: one where state space exploration
is done only until a dissimilarity is revealed. More importantly, the
logic programming formulation of local bisimulation can be extended to
do symbolic bisimulation for checking the equivalence of
infinite-state concurrent systems represented by symbolic
transition systems. We show how the two variants of symbolic
bisimulation (late and early equivalences) can be formulated as a
tabled constraint logic program in a way that precisely brings out
their differences. Finally, we show that our symbolic bisimulation
checker actually outperforms non-symbolic checkers even for relatively
small finite-state systems.
BibTex Entry:
@inproceedings{BMRRV01,
author = {Samik Basu and Madhavan Mukund and C. R. Ramakrishnan and I. V. Ramakrishnan and Rakesh M. Verma},
title = {Local and Symbolic Bisimulation Using Tabled Constraint Logic Programming},
booktitle = {International Conference on Logic Programming ({ICLP})},
address = {Paphos, Cyprus},
month = {November},
series = {Lecture Notes in Computer Science},
volume = {2237},
publisher = {Springer},
pages = {166--180},
year = {2001}
}
Full Paper
Model Checking the Java Meta-locking Algorithm
Samik Basu, Scott A. Smolka and Orson R. Ward
Abstract: We apply the XMC tabled-logic-programming-based model
checker to the Java meta-locking algorithm. Meta-locking is a highly
optimized technique for ensuring mutually exclusive access by threads
to object monitor queues, and therefore plays an essential role in
allowing Java to offer concurrent access to objects. Our abstract
specification of the meta-locking algorithm is fully parameterized,
both on M, the number of threads, and N, the number of objects. Using
XMC, we show that for a variety of values of M and N, the algorithm
indeed provides mutual exclusion and freedom from
lockout. Collectively, our results provide strong testimony to the
correctness of the meta-locking algorithm.
BibTex Entry:
@inproceedings{BSW00,
author = {Samik Basu and Scott A. Smolka and Orson R. Ward},
title = {Model Checking the Java Meta-locking Algorithm},
booktitle = {IEEE International Conference and Workshop on Engineering of Computer Based Systems ({ECBS})}
address = {Edinburgh, Scotland},
month = {April},
publisher = {IEEE Computer Society},
pages = {342--350},
year = {2000}
}
Full Paper
FocusCheck: A Tool for Model Checking and Debugging Sequential C Programs
Curtis W. Keller, Diptikalyan Saha, Samik Basu and Scott A. Smolka
Abstract:We present the FocusCheck model-checking tool for the
verification and easy debugging of assertion violations in sequential
C programs. The main functionalities of the tool are the ability to:
(a) identify all minimum-recursion, loop-free counter-examples in a C
program using on-the-fly abstraction techniques; (b) extract
focus-statement sequences (FSSs) from counter-examples, where a focus
statement is one whose execution directly or indirectly causes the
violation underlying a counter-example; (c) detect and discard
infeasible counter-examples via feasibility analysis of the
corresponding FSSs; and (d) isolate program segments that are most
likely to harbor the erroneous statements causing the
counter-examples. FocusCheck is equipped with a smart graphical user
interface that provides various views of counter-examples in terms of
their FSSs, thereby enhancing usability and readability of
model-checking results.
BibTex Entry:
@inproceedings{KBSS05,
author = {Curtis W. Keller and Diptikalyan Saha and Samik Basu and Scott A. Smolka},
title = {FocusCheck: A Tool for Model Checking and Debugging Sequential C Programs},
booktitle = {Eleventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems {TACAS}},
address = {Edinburgh, UK},
publisher = {Springer},
volume = {3440},
year = {2005},
pages = {563-569}}
Full Paper
Localizing Program Errors for Cimple Debugging
Samik Basu, Diptikalyan Saha and Scott A. Smolka
Abstract: We present automated techniques for the explanation
of counter-examples, where a counter-example should be
understood as a sequence of program statements. Our approach is based
on variable dependency analysis and is applicable to programs written
in Cimple, an expressive subset of the C programming language.
Central to our approach is the derivation of a focus-statement
sequence (FSS) from a given counter-example: a subsequence of the
counter-example containing only those program statements that directly
or indirectly affect the variable valuation leading to the program
error behind the counter-example. We develop a ranking procedure for
FSSs where FSSs of higher rank are conceptually easier to understand
and correct than those of lower rank. We also analyze constraints over
uninitialized variables in order to localize program errors to
specific program segments; this often allows the user to subsequently
take appropriate debugging measures. We have implemented our
techniques in the FocusCheck model checker, which efficiently checks
for assertion violations in Cimple programs on a per-procedure basis.
The practical utility of our approach is illustrated by its successful
application to a fast, linear-time median identification algorithm
commonly used in statistical analysis and in the Resolution Advisory
module of the Traffic Collision Avoidance System.
BibTex Entry:
@inproceedings{BSS04,
author = {Samik Basu and Diptikalyan Saha and Scott A. Smolka},
title = {Localizing Programs Errors for Cimple Debugging},
booktitle = {International Conference on Formal Techniques for Networked and Distributed Systems ({FORTE})},
address = {Madrid, Spain},
month = {September},
publisher = {Springer-Verlag},
volume = {3235},
pages = {79--96},
year = {2004}
}
Full Paper
Generation of All Counter-Examples for Push-Down Systems
Samik Basu, Diptikalyan Saha, Yow-Jian Lin and Scott A. Smolka
Abstract: We present a new, on-the-fly algorithm that given a
push-down model representing a sequential program with (recursive)
procedure calls and an extended finite-state automaton representing
(the negation of) a safety property, produces a succinct, symbolic
representation of all counter-examples; i.e., traces of system
behaviors that violate the property. The class of what we call
minimum-recursion loop-free counter-examples can then be
generated from this representation on an as-needed basis and presented
to the user. Our algorithm is also applicable, without modification,
to finite-state system models. Simultaneous consideration of multiple
counter-examples can minimize the number of model-checking runs needed
to recognize common root causes of property violations. We illustrate
the use of our techniques via application to a Java-Tar utility and an
FTP-server program, and discuss a prototype tool implementation which
offers several abstraction techniques for easy-viewing of generated
counter-examples.
BibTex Entry:
@inproceedings{BSS04,
author = {Samik Basu and Diptikalyan Saha and Yow-Jian Lin and Scott A. Smolka},
title = {Generation of All Counter-Examples for Push-Down Systems},
booktitle = {International Conference on Formal Techniques for Networked and Distributed Systems ({FORTE})},
address = {Berlin, Germany},
month = {September},
publisher = {Springer-Verlag},
volume = {2767},
pages = {79--94},
year = {2003}
}
Full Paper
Taxonomy of Intrusion Response Systems
Natalia Stakhanova, Samik Basu and Johnny Wong
Abstract:
Recent advances in the field of intrusion detection brought new requirements
to intrusion prevention and response. Traditionally, the response to an
attack is manually triggered by an administrator. However, increased
complexity and speed of the attack-spread during recent years show acute
necessity for complex dynamic response mechanisms. Although intrusion
detection systems are being actively developed, research efforts in
intrusion response are still isolated. In this work we present a taxonomy
of intrusion response systems, together with a review of current trends
in intrusion response research. We also provide a set of essential features as a
requirement for an ideal intrusion response system.
BibTex Entry:
@article{SBW:Taxo06,
author = {Natalia Stakhanova, Samik Basu and Johnny Wong},
title = {Taxonomy of Intrusion Response Systems},
journal = {International Journal of Information and Computer Security},
volume = {1},
number = {1/2},
pages = {169--184},
year = {2007} }
Full Paper
Automated Caching of Behavioral Patterns for Efficient Run-time Monitoring
Natalia Stakhanova, Samik Basu, Robyn Lutz and Johnny Wong
Abstract:
Run-time monitoring is a powerful approach for dynamically
detecting faults or malicious activity of software systems.
However, there are often two obstacles to the implementation
of this approach in practice: (1) that developing
correct and/or faulty behavioral patterns can be a
difficult, labor-intensive process, and (2) that use of such
pattern-monitoring must provide rapid turn-around or response
time. We present a novel data structure, called extended
action graph, and associated algorithms to overcome
these drawbacks. At its core, our technique relies
on effectively identifying and caching specifications from
(correct/faulty) patterns learned via machine-learning algorithm.
We describe the design and implementation of our
technique and show its practical applicability in the domain
of security monitoring of sendmail software.
Full Paper
Trust Framework for P2P Networks Using Peer-Profile Based Anomaly Technique
Natalia Stakhanova, Samik Basu, Johnny Wong and Oleg Stakhanov
Abstract: Popularity of peer-to-peer (P2P) networks exposed a
number of security vulnerabilities including the problem of finding
reliable communication partners. In this paper, we present an
integrated trust framework for P2P networks that quantifies the
trustworthiness of a peer using reputation-based trust mechanism and
anomaly detection technique. We describe anomaly detection procedure
that analyzes peer activity on the network and flags potentially
malicious behavior by detecting deviation from peer profile. We study
the performance of our trust framework using simulation and compare it
with the existing reputation-based system which does not employ an
anomaly detection mechanism.
BibTex Entry:
@inproceedings{SBWS05,
author = {Natalia Stakhanova and Samik Basu and Johnny Wong and Oleg Stakhanov},
title = {Trust Framework for P2P Networks Using Peer-Profile Based Anomaly Technique},
booktitle = {25th International Conference on Distributed Computing Systems Workshops},
year = {2005},
pages = {203-209}}
Full Paper
Proxi-Annotated Control Flow Graphs: Deterministic Context-Sensitive Monitoring for Intrusion Detection
Samik Basu and Prem Uppuluri
Abstract: Model or specification based intrusion detection, has
been effective in detecting known and unknown host based attacks with
few false alarms [Ko96,PS01]. In this approach, a model of the
program behavior is developed either manually using a high level
specification language or automatically by static/dynamic analysis of
a program. The actual program behavior is then monitored, and its
deviation from the modeled behavior is flagged as an attack. In this
paper we discuss a novel model generated using static analysis of
executables (binary code). A program's behavior is modeled using
system calls that the program makes. At its core, our approach
instruments the executables by inserting operations on auxiliary
variables, referred to as proxi variables. Programs are then
monitored using the control flow graph (CFG) based model obtained
automatically from the instrumented code. We show that the resultant
model, called proxi-annotated control flow graph, is as precise
as previous approaches which use context sensitive push-down models
and infact, enhances the runtime efficiency of such models, by
determinizing the CFGs. We show the flexibility of our technique to
handle different variations of recursion in a program
efficiently. This results in better treatment of monitoring programs
where the recursion depth is not pre-determined.
BibTex Entry:
@inproceedings{BU04,
title = {Proxi-Annotated Control Flow Graphs: Deterministic Context-Sensitive Monitoring for Intrusion Detection},
author = {Samik Basu and Prem Uppuluri},
booktitle = {International Conference on Distributed Computing & Internet Technology ({ICDCIT})},
address = {India},
publisher = {Springer},
month = {December},
year = {2004}
}
Full Paper
LASE: Layered Approach for Sensor Security and Efficiency
Prem Uppuluri and Samik Basu
Abstract: In the recent times, sensor security and reliability
has become an important concern due to the growing applicability of
sensor-based networking infrastructure. Traditionally sensor network
security ensures secure inter-communication via encryption protocols,
i.e., ensures security of data in transit. Unlike these efforts, we
present here a novel multi-layer framework to protect confidentiality
and integrity of data residing in sensors thereby ensuring sensors,
deployed in inaccesible terrains, resistant to intruder-attacks.
BibTex Entry:
@inproceedings{UB04,
title = {LASE: Layered Approach for Sensor Security and Efficiency},
author = {Prem Uppuluri and Samik Basu},
booktitle = {IEEE International Conference on Parallel Processing Workshops ({ICPPW})},
address = {Montreal, Canada},
month = {August},
pages = {346--353},
year = {2004}
}
Full Paper
Model-Carrying Code: A Practical Approach for Safe Execution of Untrusted Applications
R. Sekar, V.N. Venkatakrishnan, Samik Basu, Sandeep Bhatkar and Daniel C. DuVarney
Abstract:
This paper presents a new approach call model-carrying code (MCC) for safe
execution of untrusted code. At the heart of MCC is the idea that untrusted code
comes equipped with a concise high-level model of its security-relevant behavior.
This model helps bridge the gap between high-level security policies and low-level
binary code, thereby enabling analyses which would otherwise be impractical. For instance
users can use a fully automated verification procedure to determine if the code satisfies
their security policies. Alternatively, an automated procedure can sift through
a catalog of acceptable policies to identify one that is compatible with the
model. Once a suitable policy is selected MCC guarantees that the policy will not be
violated by the code. Unlike previous approaches, the MCC framework enables code
producers and consumers to collaborate in order to achieve safety. Moreover, it
provides support to policy selection as well as enforcement. Finally, MCC makes no
assumptions regarding the inherent risks accociated with untrusted code. It simply
provides the tools that enable a consumer to make informed decisions about the
risks that he/she is willing to tolerate so as to benefit from the functionality offered
by untrusted application.
BibTex Entry:
@inproceedings{SVBBD03,
author = {R. Sekar and V.N. Venkatakrishnan and Samik Basu and Sandeep Bhatkar and Daniel C. DuVarney},
title = {Model-carrying code: a practical approach for safe execution of untrusted applications},
booktitle = {Proceedings of the nineteenth ACM symposium on Operating systems principles},
year = {2003},
isbn = {1-58113-757-5},
pages = {15--28},
location = {Bolton Landing, NY, USA},
doi = {http://doi.acm.org/10.1145/945445.945448},
publisher = {ACM Press}
}
Full Paper