>> Their approach seems to be to "verify" each program before it runs, 
>> checking that it doesn't do any "bad" things.
> 
>   That's impossible. It can be proven that it's an unsolvable problem,
> exactly for the same reason as the halting problem is unsolvable.

In the general case, it's definitely unsolvable. I'm not sure precisely 
what they're doing to "make" it solvable - but clearly it must involve 
some kind of limitation or other.

>> Presumably verifying whether a program does or does not do something 
>> "bad" is formally equivilent to the halting problem, so I imagine they 
>> apply some arbitrary set of restrictions to simplify the problem.
> 
>   Those restrictions could seriously hinder compiler optimizations.

It's hard to say, but it *also* appears that Singularity runs some kind 
of portable VM code.

 From what I can gather, when you "install" an application, a verifier 
checks that the VM code doesn't do any "bad" things, and then compiles 
it to native code - whatever that might be. Then when you run the 
application, it just runs the native code, trusting that it can't 
possibly do bad things.

Apparently it "works" in their research prototype. Whether it could work 
in a real-world OS is another matter entirely...

-- 
http://blog.orphi.me.uk/
http://www.zazzle.com/MathematicalOrchid*

Post a reply to this message