Abstract interpretation for mobile code security

To resolve the security problems of Java mobile code, we adapted the technique of type-level abstract interpretation to verify the security of mobile code statically. Instead of data types, the mobile code is executed abstractly at the level of security-level in our approach. Based on maintaining a distribution map of security-levels of the data in mobile code´s data containers, our approach detects data-leaking just before the mobile code tries to send sensitive data out of the host. By this way our approach could make less misjudgment that verifies secure mobile programs as malicious and be more efficient than the works in Bernardeschi C et al, (2002) and Avvenuti, M et al, (2003).