Isn't Google's Native Client exactly an example of a safe bytecode? Moreover, it is a safe subset of an already existing really large byte code language (x86 machine code), which inspires me to believe that it should be possible to identify similar subsets that are statically verifiable for other, especially simpler, byte code languages.

Many holes were discovered in Native Client. Difference is that Google was willing to fix them as they were discovered.

For example, https://developer.chrome.com/native-client/community/securit... lists 20 holes. I think the actual number of explicitly discovered holes in CPython and Lua bytecodes are each less than 20, and that was enough for them to give up.

Google's Sandbox will also show more and more holes every day. Because it's a comparably easy target, especially with x86 being so complicated and even having undocumented Opcodes.

Even just mov or lea are Turing complete.

Not that there's a point anyway (in Python), `ctypes` is part of the stdlib, you could just call into that and access the VM directly.

Java's bytecode verifier intrigued me at lot, back at university when we played around with it.

I thought the verifier had been removed last time I checked, but it looks I misremembered that.

It hasn't (although some alternative VMs didn't implement it) but Java applets basically died and now I think people don't really benefit from the bytecode verifier, except arguably in debugging their JVM-targeted compilers. (I say "arguably" because generating valid JVM bytecode sometimes requires bending over backwards a bit, so your compiler would probably be simpler if it didn't have to deal with the verifier.)

Many holes have been found in the verifier over the years. More probably remain, although at this point JIT compiler bugs may be a more significant attack surface.

Also the ebpf bytecode interpreter in modern linux kernels:

http://www.brendangregg.com/blog/2015-05-15/ebpf-one-small-s...

https://www.kernel.org/doc/Documentation/networking/filter.t...