[Mono-list] Verification runtime support
Hinne Hettema (DSL AK)
Wed, 3 Jul 2002 07:49:44 +1200
I've done some work looking at what needs to happen for verification and
what is currently in the code--attached are some thoughts (ramblings rather)
on what needs to happen to make this work.
I'm interested to bring the code verification forward, but would appreciate
comments on these ideas, to figure out whether I'm off or on the right
Key is the difference between
o (Syntactically) Correct Code
o Valid Code
o Typesafe Code
o Verifiable Code
Verification ensures that code is safe to execute.
Tests performed by the validator:
o Syntax checks (compiler?)
o Metadata checks
In addition, the verifier checks that
o All uses of data are consistent with their declarations (needs access to
o Every method is called with the correct number of parameters
o Each parameter is of the correct type
o Local variables are never used unless initialised along every control flow
path that leads to the attempted use (no memory is read without having
previously been written to).
Partition III of the ECMA proposed standard outlines the verification
in section 1.8. This is a rehash of this text:
The algorithm shall attempt to associate a valid stack state with every CIL
instruction. A stack state is the number of slots on the stack as well as
type for each of them. The initial stack state is empty.
Verification assumes that the CLI zeroes all memory other than the
stack before this memory is made available to other programs.
The algorithm has to simulate all possible control flow paths through the
abd ensure that a legal stack state exists for every CIL instruction. Only
assignments are used.
Termination occurs successfully if all paths have been simulated.
if an invalid stack state was found or when "additional tests specifiedi in
clause fail" (what is this supposed to mean?)
Stack states may have to be joined and the algorithm specifies valid joins.
As I read this, this essentially specifies a dataflow algorithm.
A possible order for verification is
1. Validation tests (metadata) -- some of these are already in the code
2. Type tests (uses are consistent with declarations)
3. Initialisation tests with a dataflow algorithm
If this is what needs to happen, some observations on the current code would
-- We only call code verification from the interpreter but not yet from the
-- The current verification code looks at (some) metadata and pointers on
the stack, but doesn't do any type checking or dataflow analysis