Safe Virtual Machine

A VirtualMachine that guarantees that the code it executes cannot violate its type, thus allowing security enforcement via type constraints.

Examples:

• Dis, the InfernoOs VM: http://doc.cat-v.org/inferno/4th_edition/dis_VM_design
• JavaVirtualMachine
• The .NET CommonLanguageRuntime
  • The CLR is generally not used as a VirtualMachine (though there exist VMs which execute CLR bytecode). Instead, when a .NET program is run, DynamicCompilation from the CLR bytecode to the native code of the underyling processor occurs.
  • Same with Java. But how the code is 'executed' is secondary, the important point is the type safety.
• More generically, pretty much any of the VMs that popular scripting languages run on, including Python, Perl, and the new Parrot VM.

One advantage of SafeVirtualMachine is to be able to apply TaglessGarbageCollection.

---

The JavaVirtualMachine uses this method to allow execution of UntrustedCode in a SandBox. Multiple disjoint code spaces can coexist in one VirtualMachine. In Java this separation is controlled by ClassLoaders and SecurityManagers.

---

In doing some VisualBasicDotNet development, I got an exception that came from deep in the system libraries. The exception was "Attempted to access invalid memory. This is an indication that other memory is corrupt." After some investigation (and some pointless HeroicDebugging), I determined the crash was in handling the message in the underlying native control. A bit of investigation revealed the whole story: inserting an object whose ToString method returned Nothing into the Items collection of a ComboBox caused a null pointer dereference deep inside the system.

---

See StronglyTypedWithoutLoopholes, ObjectCapabilityModel, ProofCarryingCode, TypedAssemblyLanguage