SCS Undergraduate Thesis Topics
|Alex Vaynberg||Peter Lee||From Typed Assembly Language to Proof Carrying Code|
Typed Assembly Language (TAL) and Proof Carrying Code (PCC) are two assembly languages with additional markup that can certify that the binary code is safe to run. Although their goals are the same, they are not similar in their approaches. Furthermore the approaches taken by compilers to generate these binaries are very different, and hence compilers tend to target only one of these binaries, and are difficult to retarget. The goal of the research is to specify the translation from TAL to PCC such that any safe program in TAL will be a safe program in PCC with equivalent behavior. An additional goal is to implement an x86 version of the translator.