SPIN [7] is an extensible operating system that allows kernel extensions, so called spindles, to be inserted dynamically. Spindles as well as SPIN itself, are written in Modula-3, a type-safe object oriented programming language. The use of a type- and pointer-safe language prevents spindles from calling services inside the kernel that have not been specifically exported. The language makes it also impossible to access memory that is not part of an object to which the spindle has been given explicit access.
As long as the Modula-3 compiler is trusted to implement the language specification faithfully, and only spindles generated by this compiler are accepted, SPIN is safe from malicious code. The compiler runs at user level and is the only process that is allowed to insert spindles into the kernel. Only spindles generated at runtime can be inserted into the kernel. This eliminates the need to cryptographically sign a spindle, but has the drawback that the time to compile and optimize a spindle has to be expended for each spindle insertion. Dynamically linking a spindle into the running kernel also takes time. It is assumed that the time savings and flexibility of having the spindles execute inside the kernel compensate for this overhead.