Lambda Capabilities
roscidus.com
roscidus.com
Also good, along similar lines, is the W7 paper:
"A Security Kernel Based on the Lambda-Calculus", Jonathan A. Rees, MIT AI memo 1564, 1996.
Available as PDF at its official home at https://dspace.mit.edu/handle/1721.1/5944 and as readable HTML at jar's homepage at http://mumble.net/~jar/pubs/secureos/secureos.html.
This is incorrect: in Rust, you can declare global mutable variables, but it is unsafe to access them, since you must manually ensure there are no data races. You can also have global mutable state in safe code, as long as you protect it behind a Mutex or RwLock (which enforce exclusive mutability), or declare it as an atomic integer if it is small enough (since atomic ops do not cause data races).
> Avoiding global variables is usually considered good practise, and some systems ban them for other reasons anyway (for example, Rust doesn't allow global mutable state as it wouldn't be able to prevent races accessing it from multiple threads).
Rust does avoid global variables. You will very very rarely see a global mutex in a Rust library, and only occasionally see it in an application. (The most recent time I saw a Rust mutex was to implement string interning in wasm, a platform without atomics. So it's basically free).
Sure, global mutexes are pretty uncommon. (Although I can spy some in a few of the largest crates, such as log, crossbeam-utils, thread_local, rayon-core, and openssl.) But it's far from uncommon to use global atomic variables. Atomic counters are often used for unique ID generators, e.g., in autocfg, url, tokio, futures-util, uuid, same-file, and gimli. Atomics are also used as mutexes for external data, e.g., in parking_lot and backtrace, as well as direct storage of mutable flags and other data, e.g., in proc-macro2, time, parking_lot_core, tracing-core, and crossbeam-epoch.
I just don't want people getting the impression that Rust is among the "systems [that] ban [global variables]". I don't deny that it discourages global mutable state for most situations, but its overall approach is far more pragmatic than a simple ban.
It makes sense to me that PLs have a role to play and it would be nice if the type system were able to track capabilities.
Controlling access through keys/capabilities can also be useful for memory management. This has been worked out by Crary, Walker, Morrisett "Typed Memory Management in a Calculus of Capabilities" (POPL'99).
If this reminds you of Rust, it should since Rust is a practical implementation of many of these ideas (there were several papers and authors on tracking memory with types).
Back to security: type systems such as the Rust one that are capable of tracking lifetimes can be used for enforcing a capability discipline. An example is GhostCell by Yanovsky, Dang, Jung, Dreyer https://plv.mpi-sws.org/rustbelt/ghostcell subtitled "separating permissions from data"
The permissions in the above references are about read/write access, but one could imagine fine-grained distinction of I/O actions being subject to a similar typing discipline.
Security in type systems has been researched, with Volpano, Smith and others listed here https://en.m.wikipedia.org/wiki/Security_type_system so probably there is more. (edited for typo)
> However, writing only pure code is quite limiting. Also, we still need to audit all IO code.
Quite the turn-around.
The second is no IO.
Understatement of the year.