A Klaim specification of the
Handover protocol: logic-based
and type-based analysis
Michele Loreti and Daniele Gorla
Dipartimento di Sistemi e Informatica
University of Firenze
http://music.dsi.unifi.it/
Klaim: Kernel Language for Agent
Interaction and Mobility



Linda based communication model:
 Asynchronous communication;
 Via tuple space.
Explicit use of localities:
 Multiple distributed tuple spaces.
Possibility of code mobility.
Linda Communication Model

Tuples (“foo”, 10+5, !x)



Formal Fields
Actual Fields
Pattern Matching:


Formal fields match any field of the same type
Actual fields match if identical
(“foo”, 10+5, true) matches (!s, 15, !b)
Klaim Nodes



Name (Locality)
Tuple Space
Processes
s1
P
TS
Handover Protocol
MSC
BS2
BS1
rc
rc
rc
rc
rc
rc
MS
The Klaim Implementation
Processes...
Interesting Properties



Every sent message is delivered;
No message is delivered when an
Handover is occurring;
Messages are sent throw the correct
Base Station.
Features of the Klaim Logic
Is a variant of HML (with recursion)
Modal operators   and [ ] are
indexed with predicates that:





Describe the actual use of resources;
Express spatial properties;
State formulae for describing
resources distribution
Formulae:


Every sent message is delivered:
No message is delivered when an
Handover is occurring:
Context specification


Core part of the system is specified in
Klaim;
Context is specified with an ad-hoc
formalism: n[N]
Nets and Contexts



A net N approximates a context n, w.r.t N1, if
N does not perform more accesses to N1 than
n.
A net N agrees a context n w.r.t. N1, if N
behaves like n w.r.t. N1.
approximation and agreement are formally
defined in term of a behavioural equivalence
(a preorder) between Klaim net.
Contexts and Properties

(informal)
If  specify properties about nodes that
belong to N1, then:

If N approximates n w.r.t. N1, and (n)[N1]
satisfies  then N1||N satisfies 
(where

 is positive)
If N agrees n w.r.t. N1, then n [N1] satisfies
 iff N1||N satisfies 
Type system for Klaim
Types for Resource Access Control

We control via types the possible operation, i.e.
i,r,o,e,n (capabilities) P is formed by the non-empty subsets of capabilities
A node is s ::d P, where d is the security policy of the
node (i.e. what P can perform once executed in s)
Formally,
For example :

Well--typedness ) no illegal operations at run-time.



Dynamic Acquisition of Rights



We want the possibility of a dynamic
reconfiguration of policies
But capabilities cannot be forged, i.e.
processes/nodes cannot autonomously create
rights not owned
Solution:

access rights can be passed through the net via
communication We require that who passes the
capability must own it (statically or dynamically)
Example of Dynamic Acquisition
Dynamic Consumption of Rights

If rights are wastable resources, once a
capability has been used/passed its
owner looses it
Dynamic Consumption of Rights

If rights are wastable resources, once a
capability has been used/passed its
owner looses it
Dynamic Consumption of Rights


In a dynamic setting, the use of
capability sets in types is not
appropriate (we have to count). Hence
we use multisets
Formally:
Process Rights


Up to now, nodes acquire/loose rights
We allow single processes to
acquire/loose rights



we tag processes with the rights owned
if a process acquires rights, the tag is
increased
if a process uses rights, the tag is
decreased
Example of Process Rights
Variations on Dynamic Reconfiguration

We can choose various models for
acquisition/consumption:




Nodes have dynamic policies, while process have
no rights
Processes have dynamic policies, while nodes just
static ones
Both nodes and processes have dynamic policies
The second solution is a good compromise
between efficiency and flexibility.
The Handover Revisited



During an handover the user should not stop
its activity (i.e. the handover must be
transparent for a user)
In particular, the credit of an user must be
mantained and the information on it must be
properly passed during the handover
This scenario is well realized via our type
theory
The Handover Revisited (2)
Assumptions:
 the information on the credit of a user
is held by the Base Station associate to
that user
 it is slotted in credit units and is
represented by the messages the BS
can take from the MS and pass to the
MSC
Revised code...
The system...
Policies...
Case Study: The Active Base Station
Final remarks...



Two different approaches to mobile and
distributed languages;
Presented example can be extended to
be a real application;
Detailed papers are available at:
http://music.dsi.unifi.it
Descargar

Document