The goal of this work is to explore techniques for making today's software, which is largely written in type-unsafe, low-level languages such as C, as reliable and trustworthy as code written in type-safe, high-level languages such as Java or ML. Type-safe languages automatically block or prevent common vulnerabilities such as buffer overruns, format string attacks, and overflow attacks which are all too common in today's critical software infrastructure. To this end, we have implemented a...
Topics: DTIC Archive, Morrisett, Greg, HARVARD UNIV CAMBRIDGE MA, *COMPUTER PROGRAMS, *COMPILERS, *HIGH...
To transform a sequential program into a concurrent program, a compiler typically divides the sequential program into a partially-ordered set of basic blocks, allowing unrelated blocks to execute concurrently. Blocks may execute concurrently only if there are no dependencies among them, and therefore a compiler can introduce concurrency only to the extent that it can guarantee the absence of dependencies. A limitation of this technique is that it is necessarily conservative: it may be difficult...
Topics: DTIC Archive, Morrisett, Greg, CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE,...
In previous work, we presented Typed Assembly Language (TAL). TAL is sufficiently expressive to serve as a target language for compilers of high level languages such as ML. That work assumed such a compiler would perform a continuation passing style transform and eliminate the control stack by heap allocating activation records. However, most compilers are based on stack allocation. This paper presents STAL, an extension of TAL with stack constructs and stack types to support the stack...
Topics: DTIC Archive, Morrisett, Greg, CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE,...
Most specifications of garbage collectors concentrate on the low-level algorithmic details of how to find and preserve accessible objects. Often, they focus on bit-level manipulations such as 'scanning stack frames,' 'marking objects,' 'tagging data,' etc. While these details are important in some contexts, they often obscure the more fundamental aspects of memory management: what objects are garbage and why? We develop a series of calculi that are just low-level enough that we can express...
Topics: DTIC Archive, Morrisett, Greg, CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE, *DATA...
