From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,af0c6ea85f3ed92d
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.68.241.37 with SMTP id wf5mr3570036pbc.4.1328873970614;
        Fri, 10 Feb 2012 03:39:30 -0800 (PST)
Path: 
 wr5ni8437pbc.0!nntp.google.com!news1.google.com!postnews.google.com!t2g2000yqk.googlegroups.com!not-for-mail
From: Ludovic Brenta <ludovic@ludovic-brenta.org>
Newsgroups: comp.lang.ada
Subject: Re: Arbitrary Sandbox
Date: Fri, 10 Feb 2012 03:39:30 -0800 (PST)
Organization: http://groups.google.com
Message-ID: <ee629a84-83f6-4fc1-80fe-f6dcb1fd3eeb@t2g2000yqk.googlegroups.com>
References: 
 <8e83f2be-c6e9-4b0b-b53c-d50fe70d01e1@pq6g2000pbc.googlegroups.com>
 <jh25oo$lsl$1@speranza.aioe.org>
 <b413fd6c-dc65-4b85-8126-6d9704c2e3c5@qt7g2000pbc.googlegroups.com>
 <4f34b6d6$0$292$14726298@news.sunsite.dk>
 <e07915da-7d7d-45c8-9001-60843347ccf5@6g2000pbh.googlegroups.com>
 <4f34ecd6$0$283$14726298@news.sunsite.dk>
NNTP-Posting-Host: 153.98.68.197
Mime-Version: 1.0
X-Trace: posting.google.com 1328873970 2116 127.0.0.1 (10 Feb 2012 11:39:30
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Fri, 10 Feb 2012 11:39:30 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: t2g2000yqk.googlegroups.com; posting-host=153.98.68.197;
 posting-account=pcLQNgkAAAD9TrXkhkIgiY6-MDtJjIlC
User-Agent: G2/1.0
X-Google-Web-Client: true
X-Google-Header-Order: HUALESRCNK
X-HTTP-UserAgent: Mozilla/5.0 (Windows NT 5.1;
 rv:9.0.1) Gecko/20111222 Firefox/9.0.1,gzip(gfe)
Content-Type: text/plain; charset=ISO-8859-1
Date: 2012-02-10T03:39:30-08:00
List-Id: <comp.lang.ada>

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.