Languages assume various stances regarding the line between the language and library. Is printf part of C? A recent thread on an OCaml list began when someone using the provided binding to the OpenGL suite complained of segfaults. OCaml has modules Obj, Parsing and Marshal that are unsafe by their specifications. Keykos has the peek capability that allows reading arbitrary locations in real memory. Keykos restricts distribution of peek. OCaml makes the unsafe modules available to arbitrary programs.
Keykos affords dynamic distribution of capabilities and authority and indeed has no concept of ‘compile-time’. OCaml could do such restriction at compile-time by marking some modules as ‘unsafe’; a module deploying an unsafe module would be marked unsafe. I see significant advantages to both of these incompatible ideas.
Assuring abstraction is possible if the modules that use Obj obey rules that perhaps only the language implementers understand. In such cases those modules can be marked as safe by virtue of being part of the language platform. Large parts of the platform, sometimes all of the platform, are written in some language such as C and would be classed as unsafe except for being part of the platform proper. Are we to exclude writing part of the platform in its own language? That would be counterproductive to security. There is an extra burden if we do so however: Before abstractions were assured even if the platform could not do arithmetic correctly; if part of the platform is written in the platform’s language, than that part must operate correctly as well as guarding abstractions. We probably wanted that property anyway.
Translated to kernel systems, system integrity does not depend on the add command working right is user mode; it does depend on add working correctly in kernel mode. As a practical matter there is about a MB of user mode code in Keykos that most applications rely on.
In a complex security environment security, and the language safety that supports it, is relative. A state-department computer may have some data for which programs are allowed to use a wrapping of the Marshal module which shares that data with a certain computer in a foreign country. In Keykos this would be done with factories with holes. The hole would be to a Keykos object that held a crypto key shared only with some counterpart on the remote computer. The result is a form of perimeter security where the perimeter is defined by the holes in some factory—one perimeter per factory.
I raise the above scenario to argue against the temptation of a single category ‘unsafe’. As Bill Frantz said “I trust my money to my banker and my children to my mother-in-law, but not the other-way-round.”. I know how to do this in dynamic capability systems but not yet in static systems such as compile-time OCaml.