Tuesday September 16, 1997 Meeting

10:00am Matthias Blume : Hierarchical Modularity: Flexible namespace management and efficient recompilation

Many programming languages identify modular units with compilation units, while only few extend this to permit hierarchies of language-level modules within individual compilation units. But when the number of such compilation units is large, then it becomes increasingly important that they themselves can be grouped together and that explicit export interfaces can be used to control namespaces.

When there are many groups, then one may want to organize them into supergroups, and so on. I explain how the group model implemented in SML/NJ's compilation manager CM provides the necessary facilities to avoid unwanted interferences between unrelated parts of large programs. I also discuss the problem of automatic dependency analysis as well as its complexity and show ways of avoiding intractability.

10:45pm Break

11:00pm New Business (plan next meeting!)

11:10pm Samuel Weber : Verifying Operating System Security

EROS (the Extremely Reliable Operating System) is a high-performance, secure operating system being developed at the University of Pennsylvania. As a secure system, it is required that no process ever be able to access a resource unless it has been explicitly granted permission to do so. Furthermore, it must be possible to `confine' an untrusted process: execute the process in such a way as to render it incapable of disclosing sensitive information to any unauthorized third person. In order to satisfy these goals one has to be able to reason not only about the system state at a particular moment, but about all possible future states of the system: a confined process must be confined regardless of any future events.

This talk will describe the formal verification of EROS security. We constructed a formal model of the EROS kernel, called Agape. Agape specifies the behaviour of all the kernel calls available to EROS processes. We then formally defined the security policies of EROS and showed that these policies reflect the actual system executions. For example, if a process was not given permission to write to a certain disk page, there must be no execution in which that process did so, either directly or via intermediates.

In the process of this work we have uncovered some implementation errors. Our methodology has been designed to be applicable to any capability-based system, and to aid in the design of similar systems.

This is joint work with Jonathan Shapiro.

12:10pm Break for Lunch

1:30am Riccardo Pucella : Programming reactive systems in ML

I present in this talk an ML library that simplifies the task of programming reactive systems. A reactive system can be viewed as a system that continuously react to its environment, a task traditionally not handled very well by transformational programming language. The library provides facilities for defining control points in expressions, and combinators to act on those expressions by directing the flow of control from control points to control points.

The library is currently used as a target language for an experimental higher-level synchronous language, part of a user interface toolkit John Reppy and I are developing.

2:15pm Walid Taha : Multi-Stage Programming with Explicit Annotations

We introduce MetaML, a statically-typed multi-stage programming language extending Nielson and Nielson's two stage notation to an arbitrary number of stages. MetaML extends previous work by introducing four distinct staging annotations which generalize those published previously. Most importantly, MetaML allows us to both manipulate and run open code, all within the same type system. This was not previously possible.

We give a static semantics in which type checking is done once and for all before the first stage, and a dynamic semantics which introduces a new concept of cross-stage persistence, which requires that variables available in any stage are also available in all future stages.

We illustrate that staging is a manual form of binding time analysis. We explain why, even in the presence of automatic binding time analysis, explicit annotations are useful, especially for programs with more than two stages.

A thesis of this paper is that multi-stage languages are useful as programming languages in their own right, and should support features that make it possible for programmers to write staged computations without significantly changing their normal programming style. To illustrate this we provide a simple three stage example, and an extended two-stage example elaborating a number of practical issues.

This is joint work with my advisor Tim Sheard.

3:00pm Break

3:15am John Reppy : Designing Moby

For the past 9 months or so, I've been thinking about the design of Moby, a new ML-style language, which might serve as a straw man for the ML2000 design. Unlike most of the previous work on the design of ML2000, this effort is focused on the issues of designing a concrete surface language. While Moby doesn't really exist yet as a coherent design, I have some ideas and opinions about many of its features as well as the general design philosophy. In this talk, I'll explore these, and pose some additional questions that I'm considering.