Verification of Machine Codes Using An Effect Type System

We devise a mechanism to verify the safety of machine codes. We design a stack based machine etySECK whose code part is annotated with types and effects. And we propose an effect type system to verify properties of etySECK programs. Our system analyzes memory effects as a property of programs and we can extend our system to analyze other effects. 1 Effect-Typed Abstract Machine: etySECK The etySECK machine is a variant of Landin’s SECD [1, 2, 3, 4] machine with type and effect annotations. The syntax and the semantics of the machine is described in Figure 1 and 2, respectively. Since the machine supports functional values, compilation from functional languages to this machine is not difficult. Throughout this paper, we use dot(.) as a list constructing operator and use a single value for a list of length one. 1.1 Syntax A machine configuration consists of six components – a stack, a heap, an environment, a sequence of commands, a continuation and a set of effects of memory behaviors. The stac