3 Validation and Verification

Validation refers to a set of tests that can be performed on any file to check that the file format, metadata, and CIL are self-consistent. These tests are intended to ensure that the file conforms to the mandatory requirements of this specification. The behavior of conforming implementations of the CLI when presented with non-conforming files is unspecified.

Verification refers to a check of both CIL and its related metadata to ensure that the CIL code sequences do not permit any access to memory outside the program's logical address space. In conjunction with the validation tests, verification ensures that the program cannot access memory or other resources to which it is not granted access.

ANNOTATION

Verification is performed on a valid CLI file to ensure that its operation is memory safe. By contrast, validation determines whether the bits of a CIL (Common Intermediate Language) file conform to the CLI standard, or whether the file is, in terms of the CLI, nonsense. As stated, Partition III specifies the rules for creating valid and verifiable CIL from source code. It also lists, as informative material, rules that can be used in the design of a validating tool and, in fact, are used in the Microsoft implementation. These rules are listed as informative rather than normative (part of the standard) because it was felt that they could all be derived from the rules for valid use of CIL instructions. Nevertheless, these informative rules make it much easier to create a validation tool.

Although this discussion states that the goal of verification is type safety, it is more accurate to say that the goal of verification is memory safety. The type system used with the verifier is not the user's type system but a simpler one. For example, the verifier's type system does not distinguish signed from unsigned types. The verifier enforces type safety according to a much smaller type system, one designed to guarantee memory safety.

Partition III specifies the rules for both valid and verifiable use of CIL instructions. Partition III also provides an informative description of rules for validating the internal consistency of metadata (the rules follow, albeit indirectly, from the specification in this Partition), as well as containing a normative description of the verification algorithm. A mathematical proof of soundness of the underlying type system is possible, and provides the basis for the verification requirements. Aside from these rules this standard does not specify:

• At what time (if ever) such an algorithm should be performed

• What a conforming implementation should do in case of failure of verification

The graph in Figure 3-1 makes this relationship clearer (see next paragraph for a description).

Figure 3-1. Relationship between Valid and Verifiable CIL

In Figure 3-1 the outer circle contains all code permitted by the ilasm syntax. The next circle represents all code that is valid CIL. The dotted inner circle represents all typesafe code. Finally, the black innermost circle contains all code that is verifiable. (The difference between typesafe code and verifiable code is one of provability: code which passes the VES verification algorithm is, by definition, verifiable; but that simple algorithm rejects certain code, even though a deeper analysis would reveal it as genuinely typesafe). Note that even if a program follows the syntax described in Partition V, the code may still not be valid, because valid code shall adhere to restrictions presented in this document and in Partition III.

Verification is a very stringent test. There are many programs that will pass validation but will fail verification. The VES cannot guarantee that these programs do not access memory or resources to which they are not granted access. Nonetheless, they may have been correctly constructed so that they do not access these resources. It is thus a matter of trust, rather than mathematical proof, whether it is safe to run these programs. A conforming implementation of the CLI may allow unverifiable code (valid code that does not pass verification) to be executed, although this may be subject to administrative trust controls that are not part of this standard. A conforming implementation of the CLI shall allow the execution of verifiable code, although this may be subject to additional implementation-specified trust controls.