Lambda the Ultimate

Securing the .NET Programming Model. Andrew J. Kennedy.

The security of the .NET programming model is studied from the standpoint of fully abstract compilation of C#. A number of failures of full abstraction are identified, and fixes described. The most serious problems have recently been fixed for version 2.0 of the .NET Common Language Runtime.

This is highly amusing stuff, of course. Some choice quotes:

if source-language compilation is not fully abstract, then there exist contexts (think ‘attackers’) in the target language that can observably distinguish two program fragments not distinguishable by source contexts. Such abstraction holes can sometimes be turned into security holes: if the author of a library has reasoned about the behaviour of his code by considering only source-level contexts (i.e. other components written in the same source language), then it may be possible to construct a component in the target language which provokes unexpected and damaging behaviour.

One could argue that full abstraction is just a nicety; programmers don’t really reason about observations, program contexts, and all that, do they? Well, actually, I would like to argue that they do. At least, expert programmers...

"A C# programmer can reason about the security properties of component A by considering the behaviour of another component B written in C# that “attacks” A through its public API." -
This can only be achieved if compilation is fully abstract.

To see the six problems identified by thinking about full abstraction you'll have to go read the paper...

While not directly related to PL theory, I consider compiler construction a close relative. This set of papers describes Indiana University's compiler coursework. The key to these papers is "very small source-to-source transformations", remaining executable between passes for pedagogy and verification. Scheme is used as the source and target language because its s-expression syntax requires no 'marshaling' to and from human-readable syntax and AST structures. Later stages of the compiler include annotations directly in the source as quoted, unevaluated lists.

There is also a Summer Scheme Workshop (with complete compiler code) demonstrating some of these ideas. If anyone finds code for the Nanopass or Micropass compiler, please let me know. I'm interested in studying them as well.

A compiler structured as a small number of monolithic passes is difficult to understand and difficult to maintain. ... An attractive alternative is to structure a compiler as a collection of many fine-grained passes, each of which performs a single task. This structure aligns the implementation of a compiler with its logical organization, simplifying development, testing, and debugging.

[1] Compiler Construction Using Scheme Hilsdale, Ashley, Dybvig, and Friedman.
[2] Compiling: A high-level introduction using Scheme Haynes
[3] A Nanopass Framework for Compiler Education Sarkar, Waddell, Dybvig

Ancillary:
[4] Destination Driven Code Generation
[5] Summer Scheme Workshop; Compiling Scheme

New status report on the R6RS effort (also available as PDF).

Previous LtU discussion (March 2006).