Hacker News Reader

Comment by smosher | Hacker News Reader

The main hack done to the compiler is that generated code avoids certain constructs that inhibit perfect static analysis, allowing the NaCL host (i.e. Google Chrome at present) to verify the behaviour of some untrusted binary before ever executing it (just like Java does).

I am having a hard time with this. At first I thought this amounted to a claim that the halting problem had been solved, or else that Java and NaCl are not Turing complete. I'm guessing the problem is with the term "perfect." So something interesting must be going on or it wouldn't be worth mentioning. What's being verified? That the code can't execute data and won't call certain interrupts, or is something more interesting happening?

View on HN

At first I thought this amounted to a claim that the halting problem had been solved,

That's not what the halting problem means! There is no rule that says you cannot prove a program is safe: the rule is only that you cannot prove any arbitrary program is safe. NaCl gets around that by adding checks to the code (bounds checks, etc) to anywhere that it can't prove is safe.

Perfect static analysis is certainly halting-equivalent. What you're describing falls short of perfection, which is what I've suggested.

It's still Turing complete because it can perform arbitary computation; it just can't cause arbitrary behavior at the machine code level. (Indeed, making a VM that's both Turing complete and safe is not generally a hard problem - for example, most Brainfuck interpreters qualify. The hard problems are making safe interfaces to the rest of the system, and speed.)

I don't know exactly what NaCL does, but the JVM/CLR verification is all about making sure you don't write over someone else's memory, jump to some arbitrary address, etc. Essentially the problem is: how do you run untrusted code in the same address space, without it getting all of your process's permissions.

More info here: http://en.wikipedia.org/wiki/Java_Virtual_Machine#Bytecode_v...

Ah, thanks. I think I have a handle on the size and shape of it.

Halting problem is literally that the program will halt. That's not provable, even if you offer it on rentacoder.com.

JVM bytecode, .NET CLR bytecode, NACL bytecode are all verified as containing no illegal API calls. That's completely different. And its completely possible.

It doesn't have to solve the halting problem, just contain the code from interacting with the wider system except through tightly-defined interfaces. "does this code make any far jumps" is an answerable question when you can constrain the machine code generated and ban self-modifying code.

Reply on news.ycombinator.com