[Date Prev][Date Next][Thread Prev][Thread Next]
- Subject: Re: Bytecode: Safe or not? / luac manual
- From: Stefan Reich <stefan.reich.maker.of.eye@...>
- Date: Tue, 1 Nov 2011 16:04:20 +0000
On Tue, Nov 1, 2011 at 3:44 PM, Tony Finch <firstname.lastname@example.org> wrote:
> Rob Kendrick <email@example.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.