Invisible <voi### [at] devnull> wrote:
> 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. There's
no way for any program to check if a piece of code is executed and how.

  It's also impossible for it to know, for example, the addresses of all
pointers by simply examining the program (for example the address of a
pointer could be calculated from user input).

> 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.
For example accessing the nth element of an array can usually be done
with a simple CPU opcode. However, if the system restricts this because
it cannot prove what that n might contain, it means that the compiler
cannot generate the single opcode for accessing that array, but must
perform something much more complicated to keep the system happy.

  Ah, but that's the trend nowadays: Computers get faster and the amount
of RAM grows exponentially with time. There's no need for highly optimized
code.

-- 
                                                          - Warp

Post a reply to this message