at 14:00
Tel-Aviv University - Computer Science Colloquium
Sunday, December 19, 14:15-15:15
at 14:00
Room 309
Schreiber Building
Mobile ambients show the way to the next generation internet
languages where not only code (like the applets in Java) may
move between sites but where actual computations may traverse
the internet under their own control. Static analysis is called
for to obtain decidable approximations to the behaviour of such
computations in all possible execution contexts. The spirit of
the flow logic approach is similar to that of type systems and
logic specifications but aims at transferring state-of-the-art
techniques from data flow analysis, set constraints and abstract
interpretation to the more dynamic and concurrent scenario
offered by mobile ambients.
In the talk we develop a simple flow logic for mobile ambients
showing which ambients may end up inside what other ambients.
Based on this we validate a proposed firewall as being impenetrable
by all agents not knowing the right passwords. Despite the fact
that there are infinitely many such agents, we are able to identify
a "hardest attacker" (in the manner of hardest problems in a
complexity class) and to prove that the inability of the "hardest
attacker" to penetrate the firewall implies the inability of all
agents to penetrate the firewall unless they know the passwords.
We conclude by presenting on-going work for how to obtain a flow
logic specifying a transition system; by interpreting modal logic
formulae over such transition systems we can express temporal and
spatial properties of mobile ambients, following a recent trend by
Luca Cardelli and Andrew Gordon.
For colloquium schedule, see http://www.math.tau.ac.il/~zwick/colloq.html