Inside Java™ 2 Platform Security: Architecture, API Design, and Implementation, Second Edition

2.3. Bytecode Verification and Type Safety

Although a trustworthy compiler can ensure that Java language source code does not violate safety rules, someone could use a rigged compiler to produce code that does violate them. A Java technology–enabled Web browser that can import code fragments from anywhere does not know whether a code fragment comes from a trustworthy compiler. Thus, before executing any code fragment, the runtime system subjects it to a series of tests.

The tests range from verifying that the format of the fragment is correct to passing it through a simple theorem prover to establish that the code plays by the rules. Approximately, the code is checked to ensure that

• It does not do illegal data conversions, such as converting ...