AG 1, AG 2, AG 4   Info

Expert Audience

-- Not specified --

Saarbrücken

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.

Joint work with Hanne Riis Nielson.

--email hidden

passcode not visible

logged in users only