Re: Bytecode: Safe or not? / luac manual

[Stefan Reich <stefan.reich.maker.of.eye@...>]

On Tue, Nov 1, 2011 at 3:44 PM, Tony Finch <dot@dotat.at> wrote:
> Rob Kendrick <rjek@rjek.com> wrote:
>>
>> The halting problem is impossible to solve.  A byte code verifier is a
>> halting problem.  Thus, a perfect byte code verifier cannot exist.
>
> That isn't true. The proof obligation for safe bytecode is much simpler
> than the halting problem, because it only needs to accept bytecode that
> can be created by the Lua compiler. It is fine if the checker rejects some
> programs that do not crash the interpreter. It is rather like a static
> type checker in this respect.

Yes, this is a good explanation. Verification is a general safety
check - not a proof of termination.

As I said, with some VMs, bytecode verification is a null operation.
And those VMs are turing-complete too.

Stefan