EVALUATION The goal of this paper is to discuss the SPIN operating system. SPIN is designed to be a fast, safe operating system using the techniques of software protection. Their approach is to write the operating system using a statically checked, type safe programming language. An important feature of this is the lack of arbitrary references in their language, Modula-3, which precludes many of the bugs that plague systems written in C and C++. Their system is also flexible, in that it lets extensions to the operating system have very fine-grained control over memory and threads. This seems to be a novel way to implement an operating system since it puts the software techniques for protection that we've discussed and puts them in to practice. But: their implementation is on a dead architecture. They could not have known that the Alpha was doomed when they created the system, but SPIN as it is described in this paper is useless in 2005. Moreover, since their system is so different from conventional operating systems, application software (such as Microsoft Word and the Apache web server) would have to be at least recompiled, if not also rewritten in whole or in part, to be usable on such a system. This limits its usability to being a research operating system. Lastly, and this is more of a pet peeve than anything else, but I find that talking about related work early in the paper to be somewhat obnoxious. ---------------------------------------------------------------------- Such approach provides a safe environment for adding extensions. The performence is also good. However, extensions must be implemented by Modula-3. Also, it seems that source codes must be provided to the system. ---------------------------------------------------------------------- The novel approach with SPIN is the combination of a safe language for extension that is also powerful enough to support fine-grained changes and control. The authors describe the extension interfaces, their event model (every procedure call), their capability-based protection model, and provide a performance analysis. SPIN allows the safe extension of the kernel, which is far different from most commodity operating systems whereby (at best) code written in unsafe languages is digitally signed to demonstrate trust in the new module. SPIN's compiler signs modules, but only after guaranteeing memory safety because of the type-safety of the Modula-3 programming language. SPIN's language-based approach allows for an increase in performance because runtime checks can be reduced and more code can be run in the same address space without paying the price of unsafe kernel extension. Aside from the protective advantages of SPIN, the interface definitions allow for fine-grained control of which parts of the OS can be extended, allowing for a very diverse system. One point worth noting is that, even though memory safety is a *huge* win for kernel extensions, it does not guarantee safety in general. For example, extensions can do "bad" things semantically even though they are only playing with the correct interfaces. For example, in an OS kernel, performing "allowed" tasks such as turning off interrupts is ultimately a potentially dangerous event without checking for the corresponding reinstatement of interrupts. Type-safety alone cannot guarantee correctness of the implemented modules. It is, however, much better than most existing LKM badness. ---------------------------------------------------------------------- Any attempt to isolate the core part of a kernel from extensions like drivers is a Good Thing (TM). SPIN's main thrust was in dealing with arbitrary new extensions cooked up to serve a particular site's users, so it didn't seem too bad that SPIN "shipped" with a small core set of DEC OSF/1 drivers written in C. From a security point of view, it might be nice to have all the drivers properly isolated, if possible. This leads to a question: I see how SPIN's language-based mechanism can keep extensions from scribbling on each other. But what about extensions that need to manipulate hardware---the PCI bus, CPU registers, and so on---drivers like the SCSI driver they took from DEC OSF/1? Maybe you need to add some program re-writing to add some checks, and integrate this with the binary-signing stuff SPIN already has? (Mike: these can be hidden behind the high-level language. I.e. the language doesn't provide direct access to unsafe primitives, but rather santizes them through a function call interface tailored to the permissions granted to the extension.) ---------------------------------------------------------------------- However, the emphasis is more on extensibility that in safety. Safety only flows from the main goal of obtaining extensibility. ---------------------------------------------------------------------- SPIN is extremely flexible and the performance results seem good. Moreover, the techniques it uses are extrememly developed and reliable, making them, in some sense 'trusted'. SPIN's flexibility raises security issues. It seems, although I am probably wrong, that allowing choices about how VM is managed might raise a host of security issues if not done extremely carefully. Thus, there are no default assumptions that can be made, SPIN is only as safe as it is configured to be, which is appropriate for sophisticated users, and may even be a strength. ---------------------------------------------------------------------- SPIN uses the module interface features in Modula-3 to enforce proper access to kernel features and provide extension/plugin APIs. The use of the type-safe Modula-3 interfacing mechanism permits isolation between application spaces, enforces a level of memory integrity, and most importantly allows the calling of kernel extensions to be implemented as a procedure call. This can greatly increase the reponsiveness of the kernel extensions and operating system in general, and provide for much lower-latency system calls and message passing. They did not mention anything in the paper about the size of the trusted computing base. It seems that the SPIN model implicitly trusts the Modula3 compiler, linker, and dynamic loader/linker. They also donÕt speak much of actual memory protection, other than to say that type safety and application protection provide everything that is needed. I wonder if this would always be the case.... The authors also seemed to give SPIN a leg up in a few areasÐ they implement usage-specific memory management schemes in each of the SPIN subsystems. While this does seem a good optimization for speed, it greatly increases the size and complexity of the operating system, which could lead to more bugs and less secure code. ---------------------------------------------------------------------- RESEARCH I would like to know if SPIN was ever implemented on another architecture. Their paper seemed to imply that it was fairly reliant on the Alpha and Digital UNIX (see the sal module describe in section 5.1). I would like to see the sort of flexible memory and thread management, as well as fast cross-address space communication, in a conventional OS. ---------------------------------------------------------------------- It seems to me that SPIN is quite success by the Modula-3 implementation. Can it be implemented by other means, such that it can support other languages? Like the idea in CORBA, different objects written in different languages can communicate to each other. ---------------------------------------------------------------------- IMHO, the truly interesting aspect of the paper is the use of language-based techniques to provide properties of system correctness, even for a dynamic system. The "extensible" nature of the system is cool, but most systems do not need the features of an extensible OS. An obvious area of future research is to take a real kernel such as Linux and begin to integrate language-based techniques to provide certain properties. This is the goal of Nooks. Additionally, adding policy checks for properties in addition to memory safety, similar to the interrupt case described above, would be a valuable extension. Semantic policy enforcement for system extensions would be a huge advance. Consider a scheduler that guarantees deadlock avoidance or a network protocol that is formally verified. ---------------------------------------------------------------------- Use Modula-3, program-rewriting, and signed binaries to implement a system whose Reference Monitor is protected from tampering, even from naughty use of DMA. ---------------------------------------------------------------------- Since the main topic here is the construction of an extensible OS (SPIN), the main topic of research should be related to safety inside that type of OS. The authors have a site with source code for x86 architecture, and it would be good to test it and modify it with the new techniques that we are learning now. ---------------------------------------------------------------------- SPIN seems a really excellent system to work with in order to reason about how global properties based on the interfaces exported by the trusted modules.