Checking secure information flow in Java']Java bytecode by code transformation and standard bytecode verification

A method is presented for checking secure information flow in Java bytecode, assuming a multilevel security policy that assigns security levels to the objects. The method exploits the type-level abstract interpretation of standard bytecode verification to detect illegal information flows. We define an algorithm transforming the original code into another code in such a way that a typing error detected by the Verifier on the transformed code corresponds to a possible illicit information How in the original code. We present a prototype tool that implements the method and we show an example of application. Copyright (C) 2004 John Wiley Sons, Ltd.