 |
Semantic Modeling of Typed Assembly Language
Amal Ahmed
10:00 a.m., January 12, 2000, room 402 CS Building
Before it runs an untrusted program, a host computer may want some
assurance that the program does no harm: does not read private data or
overwrite valuable data. Proof-carrying code, introduced by Necula,
is a technique for providing such assurances. With PCC, the host
specifies a safety policy which describes under what conditions a word
of memory may be read or written. Along with the executable, the
provider of the program must also provide a proof that the program
satisfies these conditions. The host can then mechanically check the
proof before running the program. An important feature of PCC is that
proofs can be performed on native machine code, so that no unsoundness
can be introduced (for instance by a compiler) in translation from the
proved program to the program that will execute.
Necula's PCC system included the language typing rules in the safety
policy, that is, in the trusted computing base. Instead, we can model
types via definitions from first principles and prove the typing rules
as lemmas to be included in the proof. This moves information from the
trusted computing base into the semantic model and makes the safety
policy independent of the type system used by the program so that
programs compiled from different source languages may be sent to the
same code consumer.
My research is centered around the Typed Assembly Language of Morrisett
et al. and the machine model for PCC proposed by Appel and Felty.
We show an encoding of the TAL type system in higher-order logic and are
building a semantic model of the type system of TAL as an example of the
above approach to safety policies. Our model implements types as partial
equivalence relations (PERs). This implementation is useful for type
abstraction and should allow us to prove some interesting semantic
theorems. The machine model of Appel and Felty supports only
immutable types. As part of our research we are adding support for
mutable fields to the model.
|
