¶Abstract

This paper discusses features of a secure systems programming language designed and implemented at IBM's Watson Research Lab. Two features of the language design were instrumental in permitting security to be enforced with minimum run-time cost: (1) Language constructs (e.g. pointer variables) which could result in aliasing were removed from the programmer's direct control and replaced by higher level primitive types; and (2) traditional strong type checking was enhanced with typestate checking, a new mechanism in which the compiler guarantees that for all execution paths, the sequence of operations on each variable obeys a finite state grammar associated with that variable's type. Examples are given to illustrate the application of these mechanisms.

¶Notes

• Need to find papers that encode typestates directly as sets of available operations

• The discard operation (a special part of NIL's semantics) corresonds to the drop method in Swanson. It's just convention that it's called drop — any method that consumes the receiver discharges linearity just as well.

• The find operations on tables correspond to Rust's & and &mut references, if you include a lifetime bound to tie the returned reference to the table's lifetime. NIL will automatically degrade to a RefCell-style runtime check if it detects a potential read/write conflict at compile time.

• Typestates are an explicit part of function signatures. They would be in S₀ too! But they could maybe (hopefully) be inferred in higher-level languages that compile down to S₀.