💾 Archived View for dcreager.net › papers › Strom1983.gmi captured on 2024-08-25 at 00:29:27. Gemini links have been rewritten to link to archived content

-=-=-=-=-=-=-

Strom1983

Robert E. Strom. “Mechanisms for compile-time enforcement of security”. POPL '83: Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. January 1983. pp276–284

Remarkable PDF

Original PDF

DOI

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₀.