Verification for Host Confidentiality by Abstract Interpretation in Mobile Code Systems

To resolve the security problems of Java mobile programs, we adapted the technique of type-level abstract interpretation usually applied to verify the bytecode correctness to check the mobile program statically whether it impairs the host confidentiality. Instead of data types, our approach abstractly executes the mobile program at the level of security-level. Based on maintaining a distribution map of security-levels of the data in the mobile program´s data containers, our approach detects data-leaking caused by the mobile program just before it tries to send sensitive data out of the host. By this way our approach could make fewer misjudgments that verifies secure mobile programs as malicious ones and be more efficient than the works in R. Barbuti et al., (2002), C. Bernardeschi et al. (2002), and M. Avvenuti et al. (2003)