The Virtual Execution System is responsible for ensuring its security, and the security model (see the Security Specification) is built on a notion of trust levels. For some trust levels the security model requires that the code be proven typesafe. This is implemented by the VES using a verification algorithm that can examine the IL code for a method, perform a control flow analysis that uses the information from type signatures, and show that:
A perfect verification algorithm (one that declares an implementation verified if and only if it is typesafe) is provably impossible to implement. Instead, we provide a conservative verification algorithm that runs efficiently and only declares an implementation verified if it is typesafe. By observing a set of rules, a compiler can ensure that the IL code it generates will be verified. Not all languages will follow these rules, however, since the language semantics may require more sophisticated proof techniques than are implemented in the verification process to show the type safety of the IL they generate.
Because a verification algorithm is built into the NGWS runtime JIT compiler, it must run on a method-by-method basis. This process cannot prove the third property that is required to ensure type safety of programs:
This property is ensured by a combination of the class loader, verification process, and the NGWS frameworks. The loader ensures that type signatures are consistent between the use and implementation of every method and field. The verification process ensures that this consistency is maintained within verified code. And the NGWS frameworks (which are not subject to verification at runtime) also preserve the same consistency.
As a pragmatic matter, not all code will be verified, so the VES by itself cannot guarantee type safety.