Validating Firewalls in Mobile Ambients

摘要: The ambient calculus is a of computation that allows active processes (mobile ambients) to move between sites. A firewall said be protective whenever it denies entry attackers not possessing the required passwords. We devise polynomial time algorithm for rejecting proposed firewalls are guaranteed protective. This based on control flow analysis recording what may turn up inside other processes; in particular, we develop syntax-directed system specifying acceptability an analysis, prove all acceptable analyses semantically sound, and demonstrate each process admits least analysis.