Re: Arbitrary Sandbox

[Ludovic Brenta <ludovic@ludovic-brenta.org>]

Rob,

I second Thomas' suggestion that you first look into existing
virtualization solutions.

If you decide that no existing virtualization solution works for you,
then fall back on Ada and perhaps even SPARK, a subset of Ada
sugmented with annotations suitable for static analysis and formal
proof of correctness.  There is a detailed case study of how SPARK has
been used to achieve military-grade security here:

http://www.adacore.com/home/products/sparkpro/tokeneer/

I believe that if you implement a virtual machine in C# you will
probably fail because C# already runs on the .NET virtual machine; it
makes no sense to create a virtual machine on top of another.  If you
use Ada and program to the bare Win32 API, you stand only a small
chance of success because the weakest link in your solution will be
Windows itself.  If you target the bare metal, then you can
reimplement a hypervisor on top of which the untrusted, obscure and un-
audited Windows code base can run; this is your only reasonable option
IMHO.  Since several hypervisors already exist, your only chance to
make a difference and prove the superiority of your implementation is
to use SPARK and formal proof.

Good luck.

--
Ludovic Brenta.