Toward a foundational typed assembly language.
We present the design of a typed assembly language called TALT that supports heterogeneous tuples, disjoint sums, and a general account of addressing modes. TALT also implements the von Neumann model in which programs are stored in memory, and supports relative addressing. Type safety for execution and for garbage collection are shown by machine-checkable proofs. TALT is the first formalized typed assembly language to provide any of these features.
Introduction
The proliferation of low-cost computing hardware and the ubiquity of the Internet has created a
situation where a huge amount of computing power is both idle and-in principle-accessible to
developers. The goal of exploiting these idle computational resources has existed for years, and,
beginning with SETI@Home [27] in 1997, a handful of projects have successfully made profitable
use of idle computational resources on the Internet. More recently, this paradigm, now called grid
computing, has elicited serious interest among academics [5, 15] and in industry as a general means
of conducting low-cost supercomputing.
Despite the increasing interest in grid computing, a remaining obstacle to its growth is the
(understandable) reluctance of computer owners to download and execute software from developers
they do not know or trust, and may not have even heard of. This has limited the practical use of
grid computing to the small number of potential users that have been able to obtain the trust of
thousands of computer owners they do not know.
The ConCert project at CMU [9] is seeking to overcome this obstacle by developing a system for
trustless dissemination of software. In the ConCert framework, a machine owner installs a "steward"
program that ensures the safety of any downloaded software. When a new grid application is
obtained for execution (other parts of the ConCert framework determine when and how this takes
place), that application is expressed in the form of certified code, in which the executable code
is accompanied by a certificate proving that the code is safe. The steward then verifies that the
certificate is valid before permitting the code to be executed.
The form of certified code used in the prototype ConCert system [7] is Typed Assembly Language
(TAL) [19, 18], as implemented in the TALx86 system [17], which was developed primarily
at Cornell. TALx86 specializes TAL to the Intel IA-32 architecture 1 [14], and enhances it with a
number of constructs not supported in the theoretical system.
Although certified code eliminates the need to trust the developers of grid applications, there
remains the need to trust the soundness of the steward. For TALx86 (other production-quality
certified code systems such as the Java VM [16] or Proof-Carrying Code (PCC) [8] are similar),
the need for trust stems from four issues:
1. TALx86's safety is justified informally (by analogy to TAL and other work), not by any
rigorous proof.
2. The safety of TAL (and TALx86 by analogy) is given in terms of an abstract machine.
Although this abstract machine is very low-level for a type system, in a few ways it is still
somewhat high-level compared to the concrete architecture, and obscures some important
issues thereof.
3. The safety proofs that exist are given in written form, and consequently checking their veracity
is error-prone and can be done only by experts.
4. One must trust that the TALx86 type checking software correctly implements its type system.
To a certain extent, the need to trust the steward under these conditions is not a serious obstacle.
Machine owners routinely trust the safety of a great variety of applications and have far less
formal basis for doing so. Moreover, a certain amount of trust is required in any case, since
very few participants will personally inspect any of the components of the system before using it.
Nevertheless, minimizing the system's trusted computing base is always a laudable goal.
known as the "x86" architecture.
For grid computing, however, the desire to minimize trust in the steward goes beyond such
general considerations. The key issue is extensibility. Our aim is to enable the establishment of a
decentralized grid computing fabric available for a wide array of participants. For this purpose, it
is implausible to imagine that a single type system will su#ce for all potential grid applications.
Furthermore, it is also implausible (and indeed undesirable) that a single trusted agent would check
the soundness of all proposed new type systems. Thus, it is necessary that the basic steward can
be safely extended with new type systems from untrusted sources.
The natural way to achieve this is using foundational certified code, in which the entire safety
argument, down to a safety policy expressed in terms of the concrete architecture, is given in
machine-checkable form. In its incarnation as foundational PCC [1], a binary is accompanied by
an complete proof of its safety. In our proposed foundational TAL, a program's safety argument
is broken into two parts: The first portion, a self-certified type system, is the specification of
a type system and a machine-checkable proof that it satisfies an established safety policy. This
portion would generally be independent of any particular application. The second portion is the
application's typing derivation in a certified type system.
In this model, any grid application developer could devise his or her own type system su#cient
to certify his or her applications. Whenever a steward encountered a certified application referring
to an unknown type system, the steward would automatically download the type system, verify its
safety proof, and thereafter accept applications with valid typing derivations in that type system.
This model addresses each of the four issues demanding trust of the new type system. The
first three issues are clearly dealt with by the use of complete, machine-checkable proofs. By
packaging applications with typing derivations, as opposed to type annotations, the fourth issue
is also addressed: a single proof checker can check derivations for any type system, and no new
checker need ever be employed.
The aim of this work is to implement a first example of foundational typed assembly language
for the Intel IA-32 architecture, and also to build a flexible foundation on which a variety of other
type systems may be built. Accordingly, we have broken the development of our system into two
stages (in the model of Hamid, et al.'s development of ``Featherweight TAL'' [12]):
. The first stage develops a general typed assembly language that is not (very) specific to any
architecture. This general language is given an operational semantics, and its abstract safety
is established by machine-checkable proofs of type preservation and progress. The safety of
garbage collection is also established at this level (Section 4).
. The second stage shows that the abstract operational semantics maps correctly onto the
concrete architecture. The general type system is designed to account for all those issues
that pertain to the type system (including nearly all central issues), so this second stage is a
simulation argument.
This topic of this paper is the first stage of this e#ort. The second is currently underway.
1.1 TALT
This paper presents a new typed assembly language called TALT ("TAL Two"). The aims of
TALT are threefold: First, TALT is intended to provide su#cient expressive power to serve as the
target language for certifying compilers for expressive, high-level languages (in particular, Standard
ML and Popcorn (a safe dialect of C) [17]). Second, TALT's operational semantics is intended to
account, to the greatest extent possible, for the central issues of execution on the actual hardware,
so that the second stage of the foundational safety proof discussed above is a simple (albeit lengthy
and tedious) simulation argument. Third, TALT is intended to be fully formalized and enjoy a
machine-checkable type safety proof.
We begin our discussion with an overview of how TALT accomplishes each of these aims:
Expressiveness In order to provide the expressive power necessary to compile practical, high-level
programming languages, TALT follows TALx86 [17] in adding support for heterogeneous tuples
(i.e., tuples in which not all fields have the same size), recursive types, disjoint sums, and arrays.
Unlike TALx86, however, TALT supports these constructs using a formalized type theory, rather
than using specialized code in the type checker.
TALT provides all the expressive power of the original published TALx86, with the exception
of TAL's initialization flags, which are replaced by another, slightly less general mechanism (Sec-
tion 2.2.2). Most later enhancements of TALx86 are not supported in TALT, although many could
be added without di#culty.
Completeness The operational semantics of TAL is specified in terms of a low-level abstract
machine, including an explicit register file, memory, and (in stack-based TAL [18]) stack. This
brings TAL nearly to as low a level as possible without committing to the details of an architecture.
However, the TAL machine model did not include a program counter; instead, it included a stream
of input instructions that served as a surrogate for the program counter. On any branch instruction,
the machine would discard the current stream of instructions and copy in the instructions at the
branch address. TALT, on the other hand, includes an explicit program counter.
A program counter must be part of the model to address a few important issues: On the
concrete architecture, it is possible in principle to write into the code just ahead of the program
counter. This is rarely permitted in practice, of course, but even so, since programs are in fact
stored in memory, it is an essential part of a foundational safety proof to explicitly address the
issue. The requisite argument is not di#cult (TALT follows most standard practice and makes
the code read-only), but the machine model must include an explicit program counter to make the
argument at all.
An explicit program counter is also necessary to account for the notion of relative addressing,
which is particularly important on the IA-32 where most control transfers (including all conditional
jumps) are relative. Finally, an explicit program counter, or, more precisely, the fact that each
instruction is individually addressable, allows for a true call instruction in which the return address
is taken from the program counter.
Our system includes a conservative garbage collector [4] as part of its trusted computing base.
This makes the garbage collector e#ectively a part of the architecture. Accordingly, there is no need
to prove that the collector itself is safe, but it is necessary to show that programs adhere to the
invariants that the collector requires [3, 2]. The TALT type system accounts for these invariants, and
using those invariants we prove that type safety is not disrupted by garbage collection (Section 4).
In the interest of simplicity, the version of TALT in this paper provides only a few representative
operations (add, subtract, and compare). We also omit any discussion of floating
point; this is because the IA-32's implementation of floating point (using register stacks) is very
idiosyncratic. We foresee no fundamental di#culties in extending TALT in either direction.
TALT also follows stack-based TAL in viewing the stack as a separate unbounded resource,
rather than as just a designated area of memory. This dramatically simplifies the type system [18],
but requires the second stage of the foundational safety proof to show that the TALT stack can
be mapped onto the concrete stack. The principal issue in doing so is stack overflow, which we
address in Section 6.
Machine-Checkable Proofs TALT is formalized in LF [13] as mechanized in the Twelf system
[23, 24]. In accordance with the usual LF methodology, TALT typing judgements correspond
to LF types, typing rules correspond to LF constants, and TALT typing derivations correspond to
LF terms. The validity of a typing derivation can then be verified by type checking.
Of central importance to this e#ort are the type safety meta-theorems (progress, type preserva-
tion, and GC safety). These are expressed in Twelf in relational form as logic programs [21, 22]. In
support of this, Twelf provides a totality checker [26, 24] that ensures that the relations represent
total functions, and are therefore valid meta-proofs. This is discussed in detail in Section 5.
It is important to note that decidable checking of typability is not an aim for TALT. Unlike
TAL and TALx86, TALT is a type assignment (or Curry-style) system; values contain none of the
type annotations they carry in explicitly typed (or Church-style) systems such as TAL. This means
that checking the typability of TALT programs requires type inference, and since TALT's type
system is polymorphic, this means that typability checking is almost certainly undecidable [30].
Consequently, the safety certificate for a TALT program is an entire typing derivation, rather
than-as it is in TALx86-a collection of type annotations from which one can reconstruct a typing
derivation. However, this is largely just a matter of presentation; a TALT typing derivation contains
little information that would not appear in type annotations, and we conjecture that what overhead
remains can be eliminated using Necula and Rahul's technique [20].
This paper is organized as follows: We begin in Section 2 by presenting the basic TALT language,
and in Section 3 we present extensions supporting disjoint sums, arrays, and relative addressing.
In Section 4 we give our formalization of GC safety. Section 5 discusses the pragmatics of our
machine-checked proofs. Concluding remarks follow in Section 6.
2 Basic TALT
We begin our presentation of the basic TALT language by presenting its untyped fragment in four
parts: First we present the structure of values, second we present the machine model, third we
discuss the instruction set, and fourth we give its operational semantics. Following this, we present
the type system. Throughout this section we will remark on the di#erences between TALT and
TAL for the benefit of those readers familiar with the latter; readers unfamiliar with TAL may skip
these remarks.
We adopt the following notational conventions: W stands for the size of the machine word
(measured in bytes, 4 for the IA-32); i, j, k, m and n range over nonnegative integers; bit ranges
over {0, 1}; b ranges over bytes (i.e., integers modulo 256); and B ranges over words (i.e., integers
As usual, we consider alpha-equivalent expressions to be identical. However, section
identifiers (#) and registers (r) will not be considered variables and will not alpha-vary; the only
variables appearing in TALT will be type constructor variables (#).
unit values u ::= b | junk | a:i | # k :i
values v ::= #u 1 , . ,
addresses a ::= #+n
cond. codes cc ::= {cf # bit , zf # bit}
memories
register files R ::=
states M ::= (H, R, a)

Figure

1: Untyped TALT Syntax
2.1 Untyped TALT
Values TAL separated its collection of values into two syntactic classes, called "heap" and "word"
values. 2 This syntactic distinction determined what could fit into a register. In TALT, we combine
these into a single syntactic class of values that may vary in size, and use types rather than syntax
to determine how they may be used.
The syntax of type-free TALT appears in Figure 1. Values are simply sequences of zero or more
unit values, each of which is exactly one byte in size. We construct values from unit values to
ensure that any byte (including bytes in the middle of an atomic object) may be addressed, and
to make it easy to compute the size of any value. Note that it is not merely a cosmetic change to
eliminate word values but add unit values; unlike TAL's word values, unit values are never objects
of interest by themselves and are used only to construct values.
By a convenient abuse of notation, we will also often write values in the form #v 1 , . , v n #,
representing the appending of several values.
There are four forms of value that we may consider atomic: literal bytes b, junk values, addresses
a (which are W bytes in length), and instruction encodings # k . The metavariable # k ranges over
all k-byte instruction encodings. At this level of abstraction, it is not appropriate to specify the
possible values for # k ; instead, instead we assume the existence of a decoding function [[# k
takes instruction encodings to instructions (#), which we discuss a bit later. Note that need
not be injective, as a single instruction can have multiple encodings, nor need it be surjective.
Literals and junk values are one byte in size, and are represented directly as unit value con-
structs. However, addresses and (usually) instruction encodings have size greater than one byte.
Thus, the latter two forms of unit value represents bytes taken from larger atomic values: a:i represents
the ith byte of the address a, and # k :i represents the ith byte of the instruction encoding
# k . When i is out of the appropriate range, these constructs are considered junk values.
We will rarely need to deal with subcomponents of addresses and instructions, so for most
purposes a and # k can be viewed as value forms, using the abbreviations:
a
included a third class called "small" values. These were not truly values at all, and were renamed
"operands" in later work [18], as they are called here.
registers r ::= r1 | - | rN
operands
destinations d ::= rdest(r) | mdest(m, o, n)
conditions # ::= eq | neq | lt | lte | gt | gte
instructions # ::= add d,
| cmp
| jcc #,
| jmp
| malloc n, d
| mov d,
| sub d,
code I ::= #; I

Figure

2: Instructions
We also write B for the encoding of B in bytes; on a little-endian architecture such as the IA-32,
Machine Model Like TAL, the TALT machine model contains a memory and register file, but
it replaces TAL's stream of input instructions with an explicit program counter. We also augment
the state with a collection of condition codes (indicating the carry and zero flags here, but it would
not be di#cult to add more), which it is convenient to consider as part of the register file, contained
in a flag (fl) register. The TALT register file has a fixed collection of N general-purpose registers,
r1 through rN. 3 (TAL, on the other hand, assumed an infinite supply of registers.)
The TALT memory is broken into sections, identified by section identifiers #. A section represents
an area of memory that is known to be contiguous. Distinct sections, however, appear in an
unknown order in memory, possibly with intervening gaps. Thus, we view the TALT memory as
a mapping of section identifiers to values (since values are simply sequences of bytes). Any byte
in memory can be addressed (subject to the limitations of the garbage collector) by combining a
section identifier # with a numeric o#set n into the section to produce an address #+n.
When we consider garbage collection in Section 4, it will be necessary for us to distinguish
between the heap (which the collector manages) and the remainder of memory. We refer to these
portions as the heap and code segments. In anticipation of this development, we make a few remarks
now. We view the segment that a section resides in to be an intrinsic property of the section that
may be determined from its identifier. This is formalized using two predicates; hseg(#) holds if #
resides in the heap segment and conversely for cseg. The heap segment is traced by the collector
and is read/write; the code segment is not traced and is read-only. Newly allocated sections always
appear in the heap segment.
The Instruction Set The basic TALT instruction set is given in Figure 2. With the exception
of malloc (which is implemented by the run-time system, rather than the architecture), the in-
3 On the IA-32, N is 7, since the stack pointer is treated specially (Section 2.3).
structions should be familiar to any programmer of the IA-32. Note that instructions are given in
Intel-style (destination first) notation. Note also that the load and store instructions of TAL are
omitted; they are replaced by the mov instruction used with appropriate addressing modes. Code
sequences (I) are not used in the TALT operational semantics, but will arise in the type checking
rules.
Our notation for operands and destinations is more novel. The operand im(v) indicates an
immediate operand, and the operand rco(r) indicates that the operand is the contents of the
register r. The contents of memory are obtained using the operand mco(m, o, n), where o is a sub-
operand providing an address; n indicates a fixed o#set from that address at which to read, and m
indicates the size of the operand to be read (typically W ). Similarly, rdest(r) indicates that the
destination for the instruction is the register r, and mdest(m, o, n) indicates that the destination
(of size m) is in memory, with the address indicated by the operand
In order to make TALT as elegant and as general as possible, no e#ort has been made to limit
the available operands or operand/instruction combinations to those actually supported on the
IA-32 (or any other) architecture. (For example, no real architecture permits arbitrary chaining of
indirection through nesting of memory operands as TALT does; and few sizes of memory reads are
permitted.) It is more elegant to include a variety of unsupported possibilities, and to note that
these unsupported instructions are simply not in the range of the decoding function.
Operational Semantics The operational semantics are given in Figure 3. The main judgement
is indicating that the machine state M steps to the machine state M # . There are three
main auxiliary judgements to discuss; with them established, and using some auxiliary definition
given in the figure, the operational semantics should be entirely unsurprising.
The resolution of operands is formalized by the judgement M # which indicates that
in machine state M , the operand o resolves to value v. Propagation of computed results to their
destinations is formalized by the judgement M # d := v # (H, R), which indicates that in machine
state M , when a destination d is assigned the value v, the resulting memory and register file are H
and R. Finally, conditions (for the conditional jump jcc) are handled by the proposition cc #,
which is true if and only if the condition codes cc satisfy the condition #.
A few other points of notation merit comment. Note that the arithmetic equations in the
semantics specify a condition code result as well as the numeric result. The condition code results
are determined in the usual manner: the carry flag (cf) is set when the operation generates a carry
or borrow (formally, when the denormalized result lies outside the allowable range), and the zero
flag (zf) is set when the result is zero. Map update is written H{# v} for memories and similarly
for register files. Map extension (for memories only) is written H{{# v}}, when # is fresh.
2.2 The Type System
The types of TALT appear in Figure 4. The base types are B0 which is the type of the zero-length
value (#), and B1 which is the type of byte literals. The most important type constructor is the
product space, # 1 - # 2 , which contains values consisting of two adjacent values, having types # 1
and # 2 . Since appending of values is associative and has a unit (namely #), products are also
associative and have a (left and right) unit (namely B0); these equivalences are realized by a
collection of subtyping rules.
Note that unlike in TAL, a product space does not contain pointers to tuples; in TALT the
pointer is made explicit with its own type constructor (box, below). This is one factor necessary
to combine TAL's heap and word values; since tuples and pointers to tuples have di#erent types,
they need not be distinguished by syntactic class, as in TAL.
if
add d, o1 , o2 (H # , R # {fl # cc}, a
jcc #,
jcc #,
(H{{# junk n
mov d,
sub d, o1 , o2
Operand Resolution
Destination Propagation
Condition Satisfaction
Definitions
|#u1 , . , un #| def
| {z }
times

Figure

3: Operational Semantics
kinds K ::= T types
| types of size i
| B0 null value
| B1 bytes
| box(#) pointers
| mbox(#) mutable pointers
| code(#) code values
| #:K.# universal quant.
| #:K.# existential quant.
| ns top (nonsense) type
| void bottom (empty) type
| -# recursive type
r. f. types # ::=
mem. types
contexts

Figure

4: Type Syntax
Three di#erent types are provided for pointers: box(#) is the type of ordinary pointers to # ,
mbox(#) is the type of mutable pointers, and # 0 is the type of code pointers. Each pointer type
provides di#erent privileges: box is covariant but immutable, mbox is mutable but invariant, and
only code pointers may be jumped to. A subtyping rule is provided for promoting mutable pointers
to covariant ones.
A series of instructions can be given the type code(#) when it is executable provided the
register file has type #. The function space # 0 contains executable code pointers; # 0 is like
box(code(#)), except that the pointer must point into the code segment.
Universal and existential quantifiers, intersection types, union types, and recursive types are
standard (for a Curry-style system). The top type (ns) contains any value of size 1. (Wider top
types may be defined by exponents of ns.) The bottom type (void) is empty. Several useful
abbreviations (including a word-sized top nsw) are defined in Figure 5.
There are two kinds for TALT types: the kind T contains all types, and the sized kind
contains those types whose elements all have size i. For example, B0 belongs to T0 , B1 belongs to
belongs to T (i . The various pointer types all belong to
TW . Uninhabited types may vacuously belong to more than one sized kind (e.g., B0 # B1 belongs
to T0 and T1 , and void vacuously belongs to any Ti ), but any inhabited type has at most one
sized kind.
Register file types give the type for each register (other than fl). In a well-formed register
file type, each register's type must have kind TW . Every register must be included, so no width
int
ns W

Figure

5: Type Abbreviations
Judgement Interpretation
well-formed with kind K
# is well-formed
# is well-formed
a subtype of # 2
a subtype of # 2
propagation of a value having
type # to destination d results
in a register file with type #
I code I is executable when the
register file has type #
I inits r:mbox(#) discussed in Section 2.2.2
well-formed with type #
is well-formed with type #
is well-formed

Figure

subtyping rules need be included. Instead, when a register's value is irrelevant it may be given the
type nsw, and promotion to nsw can be done using depth subtyping. Heap types give a type for
each section.
2.2.1 Static Semantics
The collection of judgements in the TALT static semantics is given in Figure 6. There are thirteen
total judgements. The complete set of rules appears in Appendix A.1. Three judgements are for
type formation; these rules are unsurprising and are given only in the Appendix. Two judgements
are for subtyping, one for ordinary types and one for register file types; the latter simply applies
the former pointwise to each register's type.
The remaining judgements are for typing. Three are for typing values, operands, and destina-
tions; two are for typing code (the second is an auxiliary judgement for typing tuple initialization
code); and the final three judgements are for typing machine states and their top-level components.
Since pointers may appear anywhere and the type of a pointer depends on the type of the value
where:
ns

Figure

7: Typing Rules (except instructions)
it points to, each typing judgement (except state typing 4 ) includes a memory type as part of the
context. Operands, destinations, and code can also refer to registers, so their typing judgements
also include a register file type in the context. The TALT typing rules appear in Figures 7 and 8
and are discussed below.
Machine States The typing rules for machine states are essentially the same as those of TAL.
A state is well-formed if there exists a memory type # and register file type # with respect to
which the memory, register file, and program counter may be consistently typed. To type check
the program counter, the current code I is looked up in memory at the program counter's address
and type checked. The memory's series of bytes is converted to a code sequence by the function
which lifts the instruction decode function from single instructions to series of instructions.
Two aspects of this will change in future developments. First, we will add a second state typing
4 The state typing judgement omits a memory type because the full machine state is closed. Although the full
memory is also closed, the memory typing judgement still includes a memory type as part of the context because it
is occasionally necessary to type check a memory under weakened assumptions.
rule for typing the intermediate states of tuple initialization (Section 2.2.2). Second, the decode
function will be generalized to account for relative addressing (Section 3.3).
Values Most of the value typing rules are self-explanatory, but the rules for pointers merit dis-
cussion. A pointer with o#set n may be given the type when the section it points to can be
all elements of # 1 have size n (i.e., they are skipped by the o#set). Pointers
# into the heap segment may be given the stronger type mbox(# 2 ), provided that #) is a subtype
and a supertype of # 1 - # 2 . This ensures that when a # 2 is written back into the heap object, the
object still has type #), so the heap's type is unchanged.
The value typing rules tell far from the entire story. Most of the flexibility of the TALT type
system is provided by its subtyping rules. Subtyping provides the introduction facility for existen-
tial, union, and recursive types; the elimination facility for universal, intersection, and recursive
types; associativity and identity rules for products; and distributivity rules for intersection and
union types and void. There are about fifty subtyping rules in all, listed in Appendix A.1; in the
interest of brevity, we will discuss individual rules only as they arise.
Operands and Destinations Since an operand may be drawn from a register, the operand
typing judgement includes the register file's type in its context. Similarly, since a destination may
be a register, propagation of a value to a destination can change the register file type, and hence
the destination typing judgement includes register file types for before and after.
The typing rules for memory operands and destinations are novel. Using the associativity and
identity subtyping rules for products, 5 one casts the pointer's type in the form (m)box(#
is the operand's type, and # 1 and # 3 are the types of the left and right residual values.
The sizes are checked using kinds: # 1 must have kind Tn to match the o#set, and # 2 must have
kind Tm to match the operand size. Note that unlike register destinations, memory destinations
are forbidden to change the data's type; allowing changes would be unsound due to the possibility
of aliasing.
Instructions With much of the type system moved into the rules for operands and destinations,
the typing rules for instructions given in Figure 8 should be largely as expected. The final two
rules merit comment. The first is a subtyping rule for code; it states that if I type checks under
assumptions # then it also type checks under the stronger assumptions #. The second rule is the
elimination rule for existential types. When a register contains a value of existential type, it allows
that value to be unpacked in place. (The TAL instruction unpack is obtained by combining a mov
instruction with this rule.)
2.2.2 Allocation and Initialization
The most complicated TALT typing rule is for malloc. A newly allocated tuple begins filled with
junk and is then initialized field-by-field. As a tuple is initialized, its type must change to reflect
its new components. This means that initialization is incompatible with our usual rule for memory
writes.
TAL provided an elegant way to handle this using "initialization flags," in which the a newly
allocated tuple is essentially stamped with its ultimate type and any initialization must move
toward that ultimate type [10]. This addressed the aliasing problem because any aliases could have
5 Although mbox is invariant, it does respect symmetric subtyping (that is,
# ), so associativity and identity for products can be applied beneath an mbox.
# add d,
# jcc #, o; I
# jmp o; I
# mov d, o; I
I
I

Figure

8: Instruction Typing Rules (except allocation)
weaker views of a tuple, but not incompatible ones. Moreover, since TAL conflates the mechanisms
of pointers and tuples, TAL can track the initialization of a tuple on a field-by-field basis. Thus,
TAL permits the interleaving of initialization with other computation.
Unfortunately, (field-by-field) initialization flags are incompatible with TALT because of TALT's
decoupling of pointers and tuples. Moreover, the flexibility a#orded by initialization flags appears
rarely to be used in practice. Therefore, as an expedient alternative, TALT requires that a newly
allocated object be fully initialized before any other computation takes place. During this uninterrupted
initialization, it is easy to maintain the invariant that no aliases to the new object exist. A
more powerful account of initialization could likely be given using alias types [28], but we have not
explored such an extension.
The rules implementing this mechanism appear in Figure 9. The first rule provides that when
an object is allocated and its pointer is placed in register r, type checking moves into a special
mode in which r's type can be updated, but r cannot be used for any other purpose (the latter is
enforced by giving it type nsw). After a series of initializing moves, the final rule is used to make
r an ordinary pointer and shift back into the ordinary type checking mode. An additional (ugly)
rule for type checking machine states in the midst of initialization appears in Appendix A.1; it
expresses the invariants of initialization so that the Type Preservation property can be established.
# mov mdest(m, rco(r), n), o; I inits r:mbox(#)
I
I inits r:mbox(#)

Figure

9: Allocation/Initialization Typing Rules
2.3 Stacks
TALT supports stacks using type mechanism essentially identical to those of stack-based TAL [18],
although a variety of its special instructions have been folded into TALT's operand/destination
mechanism. The full details appear in Appendix A. For reasons of brevity, we omit any discussion
of stacks in the body of this paper beyond a few remarks here.
Since TALT already has the notions of a null object (#) and of concatenation of objects in
memory (-), there is no need to introduce special types (nil and ::) as in stack-based TAL.
There is, however, a need for a special kind: since the stack's type must determine its size, and
TALT types do not always do so (e.g., B0#B1), we require a kind of types whose size are determined
(though possibly unknown, as for variables of kind TD). This kind, called TD , is rarely useful aside
from stacks, so for practical purposes it serves as the kind of stack types.
2.4 Multiple Entry Points
One facility provided by TALT that may not immediately be obvious is the ability to jump into
the middle of a block of code, which is impossible in TAL. Operationally it is clear that one can
jump to any valid address. What is less obvious is that such jumps can be well-typed. Suppose
where, for simplicity, #v code , v morecode # and v morecode are each executable with register file type #,
and suppose |v code We wish to assign # a type so that both #+0 and #+n have type # 0.
This is possible by giving # the type:
(ns n
This makes it possible to structure TALT code with any desired forward and backward jumps,
without needing to insert arbitrary breaks for typing purposes. More importantly, since any executable
address can be given a type in this manner, TALT can support a true call instruction
in which the return address is obtained from the program counter. Details of the call instruction
appear in Appendix A.

Figure

10: Integer Ranges
Extensions
3.1 Disjoint Sums
The standard implementation of a disjoint sum type, say int is as a pointer to
a tuple whose leading field is a tag identifying the arm of the sum. In TALx86, this idiom is
supported directly by a special type for disjoint sums. In TALT, we decompose it into its primitive
components:
First we add the notion of a singleton type, written set= (B), containing only the integer B.
With it, we can easily construct a type that faithfully characterizes this encoding:
An element of this type is either a pointer to an int following a zero tag, or a pointer to an int-int
following a one tag.

Figure

gives the typing rules and some pertinent subtyping rules for set= , and also for
the upper and lower subrange types set< and set> , which will be useful shortly. By themselves,
these rules are not su#cient, however, because although the type above accurately expressed the
members of a disjoint sum, it is not immediately useful.
The problem is the absence of an elimination rule for union types. We may load the tag word
instructions # ::= - | cmpjcc
# neq,B
unsat
unsat # void (7)

Figure

11: Union Elimination
from o#set 0 into the disjoint union, since:
(distributing # over box)
(distributing # over -)
# (promotion of set= to int)
box(int - (int # (int - int)))
Then, by comparing the tag to zero, we may determine (dynamically) which arm of the disjoint
union the object belongs to. However, with the rules discussed so far, there is no way to take advantage
of that information in the static typing, so there is no way to access the variant constituents
of the disjoint union.
To make it possible to eliminate union types, we add a new instruction cmpjcc. Operationally,
is identical to the two-instruction sequence cmp evaluation
rule is formalized in Appendix A.2) . What is special about this (pseudo-)instruction is its typing
rule.
and r is used in the comparison of . (In the example above, r has
type (#), and the comparison is of mco(W, rco(r), 0) to im(0) using condition eq.) The idea of the
rule is to eliminate r's union type by providing a static proof that r cannot have type # 2 when the
branch is taken, and that r cannot have type # 1 when the branch is skipped. It follows that r can
be given type # 1 for the branch, and # 2 for the non-branch.
Consider the cmpjcc typing rule, given in Figure 11. Clauses 1 and 2 ensure that the comparison
itself is permissible, and indicate that the value being compared against is the number B. In the
event the branch is taken, must have the type #,B
sat , and #,B
unsat if it is not.
Clause 3 identifies the union type of interest, # 1 # 2 . It follows that r has either type # 1 or type
re-types the first operand in the first hypothetical circumstance. Thus, if r has
1 . However, if the branch is skipped, must also have the type #,B
unsat ,
and clause 7 proves that both cannot simultaneously be true. Therefore, if the branch is skipped
we may conclude that r has type # 2 (clause 10). A similar argument shows that if the branch is
taken, we may conclude that r has type # 1 (clause 9).
For example, suppose r has type (#) and we wish to jump if the tag is zero using
cmpjcc mco(W, rco(r), 0), im(0), eq,
The first six clauses are easily established (using the argument above for clause 1); #
out to be set= (0) and set= (1). It remains to show that
and
It is easy to obtain the first using distributivity and the contradiction subtyping rules set= (B) #
void. For the second, observe that set= (1) # set> (0)
and then the result follows by the latter contradiction subtyping rule. Thus, we may continue type
checking with a refined type for r in each branch.
In the more general case of n-ary sums, we may wish to case-analyze a sum using binary
search to execute log 2 n comparisons rather than n - 1. This can be done using the same rule by
choosing an inequality comparison rather than equality. To set up the rule, it is necessary to use
the associativity of union types to cast an n-ary sum in the form of a single union type in which
one arm is incompatible with branching and the other with not branching.
3.2 Arrays
In the developments so far, TALT already supports an array-like type in the form # n , for an n-element
#-array. However, this type has the shortcoming that the array's length must be known
statically. What we want is something like #n.# n .
First we add the facility to quantify over array length by adding a new form of type constructor
representing numbers. Thus far, we have not referred to type constructors because all of TALT's
type constructors have been actual types; now we must rename the syntactic class of types to type
constructors (or "tycons" for short). We will use the metavariable c for type constructors in general,
but will continue to use the metavariable # for tycons of kind T and will use the metavariable x for
tycons of kind Num.
With this terminology established, we add a new kind Num and a new tycon B : Num. We will
occasionally find it convenient to allow the word B (an integer modulo 2 8W ) to be used in place of an
ordinary nonnegative integer, in which case B should be interpreted as its canonical representative.
We also generalize each of the integer subrange types to be defined over tycons of kind Num
including variables, and generalize the various rules dealing with subranges accordingly. Finally,
we add the type of x-element arrays of # as # x. These developments are summarized in Figure 12.
We can now give the type of an array of unknown length as #:Num. set= (#) - mbox(#).
kinds K ::= - | Num
tycons c, #, x ::= -
| set= (x) | set< (x) | set> (x)
operands
destinations d ::= - | imdest(m,

Figure

12: Arrays
Since the addressing modes we have provided so far provide only for fixed o#sets into tuples, we
must also provide an operand and destination construct for reads from and writes to dynamically
specified o#sets into arrays. For this purpose we provide an "indexed memory" operand form
imco(m, and a similar destination form imdest(m,
The o#set calculation for these constructs is n+ k - the base address and size remain
m. Thus, when points to an array in which each element has size k, imco extracts o#set n from
the element of the array. The typing rules for imco and imdest are given in Figure 12; the
operational rules are given in Appendix A.2.
A pseudo-instruction mallocarr is provided to allocate and initialize arrays. Due to space
considerations we do not discuss it here; full details appear in Appendix A.
Note that imco and imdest include no array-bounds checks; the typing derivation is responsible
for showing that the index is within the allowable range. For the (typical) case where an array-
bound check is necessary, one could add another cmpjcc rule to refine a integers to subranges, but
it turns out that the existing cmpjcc su#ces with the addition of a trichotomy rule:
6 On the IA-32, these addressing modes are provided as primitives for and 8; on some other architectures
or for other values of k they would need to be synthesized.
(and some rearranging) we may obtain
It seems likely that a more sophisticated treatment of array bounds checks is possible using
something like Xi and Harper's DTAL [31] to track dependencies between various integer values,
but we have not explored such an extension at this time, as mechanizing their proofs seems likely
to be burdensome.
3.3 Relative Addressing
Given the TALT machine model, PC-relative addressing is not di#cult to add operationally. We
simply add a new operand form pcrel(-n) and the operand resolution rules:
and
For the type system, however, matters are trickier. Relative addressing creates a situation in
which code (and therefore values in general) may have a certain type only when it resides in a
particular location, at least when viewed naively. This situation is undesirable for two reasons:
First, making the typing rules aware of the locations in which values reside would require wide-scale
changes to the type system that would lessen its elegance. Second, the resulting type system
would be very unlike conventional type systems in which a value's type does not depend on where
it is written.
To preserve the type system in its current form, we introduce a technical device we call delocal-
ization. We employ a function deloc to convert relative addresses to absolute ones. For example:
deloc(a, mco(m, o,
Code is always type checked in delocalized form, so no typing rule need be provided for relative
operands. Consequently, the typing rules for instruction can be preserved without change.
The burden of delocalization is assumed in the code typing rule, where values are converted to
code sequences for type checking. Recall the rule from Figure 8:
(old)
First, we modify the decode function (now [[[v]]]a) to account for delocalization:
Second, since the typing rule does not know where in memory v lies, it is permitted to assume any
address (just as it may assume any register file type) and it records the assumption in the type:
(new)
The type code(a, #) should be read as "code that may be executed when the register file has type
#, provided it resides at address a."
The obligation is discharged in the typing rule for code pointers, which admits only properly
delocalized pointers as code pointers:
(new)
Note that if a code block is delocalized at an address other than where it resides, that address
cannot be given a code pointer type.
The only other change that must be made to the type system is that the top-level state typing
rule must be modified in the obvious manner to account for delocalization:
The principal safety results for TALT, as usual, are Progress and Type Preservation:
Theorem 4.1 (Progress) If # M then M # M # , for some M # .
Theorem 4.2 (Type Preservation) If # M and M # M # then # M # .
The Progress proof is by induction on the typing derivation. The Type Preservation proof is
by case analysis on the evaluation derivation, with an outer induction on the typing derivation (to
handle the register file subsumption and existential unpacking rules).
Additionally, since the TALT operational semantics does not account for garbage collection, we
must prove an additional result showing that garbage collection does not disrupt typability.
Like TALx86, TALT is designed for use with the Boehm-Demers-Weiser conservative garbage
collector [4]. Therefore there is no need to maintain any tagging invariants in order to assist
the collector in distinguishing pointers from integers. However, one GC safety condition must be
maintained for the collector to function properly [3]:
Every live heap object must be reachable by a chain of pointers from the root set.
A pointer is permitted to reach an object by pointing anywhere from the object's beginning to its
end. 7 Our root set is the collection of values in the register file and stack.
If this condition is not maintained, the only consequence is that live objects may be garbage
collected. Therefore, for our purposes we define a live object to be one whose presence is required
for the state to be well-typed. Our main GC result then will be a proof that garbage collecting
unreachable objects cannot break typability of the state.
In order to satisfy the GC safety condition, we impose the following two invariants on well-typed
TALT code:
7 Interior pointers are not permitted by Boehm and Chase's specification [3], but are permitted by the collector's
implementation.
where # dom(#) | cseg(#)}

Figure

13: Modified Rules for GC Safety
1. The code segment contains no (non-accidental) pointers into the heap segment.
2. Immediate operands contain no (non-accidental) pointers into the heap segment.
Invariant 1 is necessary because the code segment is not part of the collector's root set. Invariant
2 is not stricly speaking necessary but is not burdensome either; if an operand is part of an
instruction in the code segment then invariant 2 follows from invariant 1, and if not the instruction
is useless anyway. The invariant is imposed because it dramatically simplifies the development to
since it means there is no need to formalize how to look for pointers in code values.
These invariants are achieved by replacing the typing rules for immediate operands and memories
with the rules in Figure 13, which strip all heap sections from the memory type when typing
code sections and immediate operands.
To formalize the GC safety theorem, we need a definition of unreachability:
Definition 4.3 Suppose S is a set of heap section identifiers. Then S is H-reachable from v if v
can be written in the form #v 1 , #+n, v 2 # for some # S and n # |H(#)|.
A section is unreachable from the memory as a whole if every section that can reach it is either
untraced (i.e., in the code segment) or unreachable itself:
Definition 4.4 Suppose S is a set of heap section identifiers. Then S is unreachable from H if for
every # dom(H), either cseg(#) or # S or S is not H-reachable from H(#).
Definition 4.5 Suppose S is a set of heap section identifiers. Then S is unreachable in (H, R, a)
. S is unreachable from H, and
. for every r, S is not H-reachable from R(r), and
. S is not H-reachable from R(sp).
Note that the definition of unreachability is not deterministic. When S is unreachable in M ,
S can be as small as the empty set. The definition is crafted in this manner because we cannot
predict what objects will actually be collected by a conservative collector. Instead, we prove our
result for all unreachable sets, thereby covering whatever the collector turns out to do.
Theorem 4.6 (GC Safety) Suppose S is unreachable in (H, R, a) and suppose that # (H, R, a).
The proof is by induction on the typing derivation.
5 Machine-Checked Proofs
The results of this paper are formalized as machine-checked proofs in the Twelf system [23, 24].
The first step in this formalization is to encode the TALT syntax, type system, and operational
semantics as an LF signature [13] wherein judgements become types and derivations become terms.
This process is standard, so we will not belabor it here.
Once the language is formalized, we can state and prove the principal meta-theorems: Progress,
Type Preservation, and GC Safety. A meta-theorem statement is encoded as a relation between
derivations [21, 22]. For example, the principal meta-theorem statements become:
progress
%mode progress +D1 -D2.
preservation
-> machineok M' -> type.
%mode preservation +D1 +D2 -D3.
collect collect M M'
-> machineok M' -> type.
%mode collect ok +D1 +D2 -D3.
For instance, the progress theorem is a relation between machineok M derivations and
stepsto M M' derivations, and so forth. The %mode declaration following each statement indicates
the input and output arguments of the relation [25]. In each of these cases, the last argument
(with the "-" mode) is the sole output argument.
A proof of a meta-theorem so encoded is a logic program whose type is the relational encoding of
the theorem. The program can then (in principle) be given derivations in the input arguments and
unification variables in the output arguments and executed to obtain the resulting derivations. A
logic program represents a valid meta-proof if the execution always runs to a successful conclusion.
The Twelf totality checker verifies that the logic program is in fact total, with assistance from
the programmer in identifying the induction variable(s). This consists of checking three facts:
1. Mode checking: output arguments (and input arguments to subcalls) are fully determined.
2. Termination checking: the induction variable(s) decrease in all recursive calls.
3. Totality checking: in every case analysis, all cases are covered.
For details, the reader is referred to Pfenning and Sch-urmann [24] or Sch-urmann [26].
The specification of TALT in LF consists of 2081 lines of Twelf code, and the complete proof of
Theorems 4.1, 4.2 and 4.6 consists of 10137 lines of Twelf code (including comments). A breakdown
of the proof code for the interested reader is given in Table 1. The full proof takes approximately
three minutes to check in Twelf 1.3R3 on a Pentium 3 with 128 megs of RAM.
Proof Components
lines purpose
210 Properties of canonical forms
252 Properties of conditions
Properties of memory lookup/update/extension
Instruction decode lemmas
372 Properties of register file lookup/update
399 Properties of values
407 Equality lemmas
429 Properties of natural number arithmetic
515 Validity (well-behavedness of derivations)
537 Canonical Forms lemma
548 Lemmas regarding type formation
Progress
713 Weakening and strengthening of memory types
Operand/destination lemmas
925 Type Preservation
1245 Properties of binary arithmetic

Table

1: Safety Proof Breakdown
6 Conclusion
TALT provides an elegant, expressive, and fully formalized type system for assembly language.
The machine-checkable safety theorems of Section 5 provide a complete safety argument for TALT
programs in terms of a safety policy expressed (by the operational semantics) at the assembly
language level. To complete a foundational TAL system, this work must be combined with a
proof that the TALT operational semantics maps correctly on the concrete architecture. TALT is
designed so that this latter stage of the proof implementation is a type-free simulation argument.
TALT is also designed to be easily adaptable to other architectures. The general architectural
constants (big-endian vs. little-endian, the number of registers, and the size of the machine word)
are parameters to the language and can easily be changed. New instructions can also easily be
added; in fact, given the generality of the TALT operand/destination mechanism, many "new"
instructions may already be present. This means that the primary burden of specializing TALT to
an architecture is accounting for its idiosyncrasies (e.g., the IA-32's treatment of floating point, or
the delay slots following jumps on many RISC architectures).
One issue not addressed in TALT is the issue of processor exceptions and faults (e.g., division
by zero, stack overflow, or various floating-point exceptions). These can be prohibitively expensive
to prevent dynamically, and are di#cult to prevent statically. Fortunately, for our purposes they
can be safely ignored, assuming that the occurrence of an exception aborts the program, because
a program that is no longer running is certainly safe.
The issue of stack overflow is a little bit more involved, because we must ensure that any stack
that overflows will cause the stack overflow exception. We can do so by following the standard
practice of preceding 8 the stack in memory by at least one (typically many) unmapped memory
pages. Any push instruction that overflows the stack will therefore hit an unmapped page and cause
the exception. The salloc instruction, which increases the stack's size by an arbitrary amount, is
a bit trickier because it could skip all the unmapped pages and land in accessible memory. We can
prevent this by limiting salloc to one page at a time and forcing it to touch the top of the stack
as push does. This ensures that any overflowing salloc will hit the unmapped page.
To assist in the development of TALT programs, we have also designed an explicitly typed variant
of TALT, called XTALT, that enjoys decidable type checking. XTALT adds type annotations to
sections and replaces TALT's subtyping with explicit coercions. We are implementing an assembler
that typechecks XTALT programs, generates the corresponding TALT derivations, and compresses
them using Necula and Rahul's technique [20]. Also under development is a Popcorn [17] to XTALT
compiler. These tools can be combined with Dunfield's Standard ML to Popcorn compiler [11]
(based on RML [29] and MLton [6]) to provide a complete certifying compiler from Standard ML
to TALT. A direct Standard ML to TALT compiler is also underway.



--R

A semantic model of types and machine instructions for proof-carrying code
Simple garbage-collector safety
A proposal for garbage-collector-safe C compilation
Garbage collection in an uncooperative environment.
First International Workshop on Grid Comput- ing

Trustless grid computing in ConCert.
A certifying compiler for Java.

Type structure for low-level programming langauges
Personal communication.
A syntactic approach to foundational proof-carrying code
A framework for defining logics.

Second International Workshop on Grid Computing
The Java Virtual Machine Specification.
A realistic typed assembly language.

From System F to typed assembly language.

Logic programming in the LF logical framework.
Implementing the meta-theory of deductive sys- tems
System description: Twelf - a meta-logic framework for deductive systems
Twelf User's Guide
Mode and termination checking for higher-order logic programs
Automating the Meta Theory of Deductive Systems.

Alias types.
From ML to Ada: Strongly-typed language interoperability via source translation
Typability and type checking in System F are equivalent and undecidable.
A dependently typed assembly language.


--TR
Garbage collection in an uncooperative environment
Logic programming in the LF logical framework
A framework for defining logics
Simple garbage-collector-safety
From system F to typed assembly language
A semantic model of types and machine instructions for proof-carrying code
A certifying compiler for Java
Oracle-based checking of untrusted software
Java Virtual Machine Specification
Grid Computing
Mode and Termination Checking for Higher-Order Logic Programs
Flow-Directed Closure Conversion for Typed Languages
Alias Types
A Syntactic Approach to Foundational Proof-Carrying Code
Type Structure for Low-Level Programming Languages
Stack-Based Typed Assembly Language
Implementing the Meta-Theory of Deductive Systems
System Description

--CTR
Joseph C. Vanderwaart , Karl Crary, Automated and certified conformance to responsiveness policies, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.79-90, January 10-10, 2005, Long Beach, California, USA
Michael F. Ringenburg , Dan Grossman, Types for describing coordinated data structures, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.25-36, January 10-10, 2005, Long Beach, California, USA
Adam Chlipala, Modular development of certified program verifiers with a proof assistant, ACM SIGPLAN Notices, v.41 n.9, September 2006
Hongxu Cai , Zhong Shao , Alexander Vaynberg, Certified self-modifying code, ACM SIGPLAN Notices, v.42 n.6, June 2007
Brigitte Pientka, Verifying Termination and Reduction Properties about Higher-Order Logic Programs, Journal of Automated Reasoning, v.34 n.2, p.179-207, December  2005
Feng , Zhaozhong Ni , Zhong Shao , Yu Guo, An open framework for foundational proof-carrying code, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, January 16-16, 2007, Nice, Nice, France
Bor-Yuh Evan Chang , Adam Chlipala , George C. Necula , Robert R. Schneck, Type-based verification of sssembly language for compiler debugging, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.91-102, January 10-10, 2005, Long Beach, California, USA
Feng , Zhong Shao, Modular verification of concurrent assembly code with dynamic thread creation and termination, ACM SIGPLAN Notices, v.40 n.9, September 2005
Andrew W. Appel , Paul-Andr Mellis , Christopher D. Richards , Jrme Vouillon, A very modal model of a modern, major, general type system, ACM SIGPLAN Notices, v.42 n.1, January 2007
Bor-Yuh Evan Chang , Adam Chlipala , George C. Necula , Robert R. Schneck, The open verifier framework for foundational verifiers, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.1-12, January 10-10, 2005, Long Beach, California, USA
Juan Chen , Dinghao Wu , Andrew W. Appel , Hai Fang, A provably sound TAL for back-end optimization, ACM SIGPLAN Notices, v.38 n.5, May
Zhaozhong Ni , Zhong Shao, Certified assembly programming with embedded code pointers, ACM SIGPLAN Notices, v.41 n.1, p.320-333, January 2006

Dan Grossman, Quantified types in an imperative language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.3, p.429-475, May 2006
typed assembly language;proof-carrying code