Bytecode: Safe or not? / luac manual

classic Classic list List threaded Threaded
51 messages Options
123
Reply | Threaded
Open this post in threaded view
|

Bytecode: Safe or not? / luac manual

Stefan Reich
Hmm! Just found that "man luac" says:

       -p     load  files  but  do not generate any output file.  Used mainly
              for syntax checking and for testing  precompiled  chunks:  cor-
              rupted  files  will  probably generate errors when loaded.  Lua
              always  performs  a  thorough  integrity  test  on  precompiled
              chunks.   Bytecode that passes this test is completely safe, in
              the sense that it will not  break  the  interpreter.

"Lua always performs a thorough integrity test on precompiled chunks"?
I thought everybody agreed that bytecode is unsafe in 5.1.

How can the contradiction be solved?

Stefan

Reply | Threaded
Open this post in threaded view
|

Re: Bytecode: Safe or not? / luac manual

Luiz Henrique de Figueiredo
> "Lua always performs a thorough integrity test on precompiled chunks"?
> I thought everybody agreed that bytecode is unsafe in 5.1.
>
> How can the contradiction be solved?

It was solved in 5.2 by removing the bytecode verifier,
mainly because Peter Cawley has shown several exploits
of flaws in the bytecode verifier of Lua 5.1. See also
http://lua-users.org/lists/lua-l/2011-10/msg00214.html

Reply | Threaded
Open this post in threaded view
|

Re: Bytecode: Safe or not? / luac manual

Stefan Reich
Ah. So the manpage is basically in error because it doesn't know about
the exploits yet.

I really do hope that lbcv covers all the possible violations. Having
a safe way of loading untrusted bytecode is quite crucial to what I
want to be able to do with Mobile Lua.

Once we have safe deserialisation of Lua states - we can achieve total
mobility for all Lua code.

I don't know about you guys, but I for one am really excited about
that perspective.

-Stefan

On Sun, Oct 30, 2011 at 7:29 PM, Luiz Henrique de Figueiredo
<[hidden email]> wrote:
>> "Lua always performs a thorough integrity test on precompiled chunks"?
>> I thought everybody agreed that bytecode is unsafe in 5.1.
>>
>> How can the contradiction be solved?
>
> It was solved in 5.2 by removing the bytecode verifier,
> mainly because Peter Cawley has shown several exploits
> of flaws in the bytecode verifier of Lua 5.1. See also
> http://lua-users.org/lists/lua-l/2011-10/msg00214.html

Reply | Threaded
Open this post in threaded view
|

Re: Bytecode: Safe or not? / luac manual

Frank Meier-Dörnberg
Am 30.10.2011 21:50, schrieb Stefan Reich:
...
> I really do hope that lbcv covers all the possible violations. Having
> a safe way of loading untrusted bytecode is quite crucial to what I
> want to be able to do with Mobile Lua.
...

Do you really have to "load untrusted bytecode"?
Is not it enough or even better to load cryptographically signed bytecode?

Greetings
Frank

Reply | Threaded
Open this post in threaded view
|

Re: Bytecode: Safe or not? / luac manual

Axel Kittenberger
Since lua-jit only supports source code, why use byte code at all?

In case of speed: I suppose the state of affairs is that bytecode is
only loaded faster if not checked. Any speedadvantage to parsing is
eaten up by through untrusted bytecode checking. In case of size: how
much smaller is bytecode compared to source code that is say
precompile-stripped of comments etc. and gzipped if at all?

On Mon, Oct 31, 2011 at 12:47 PM, Frank Meier-Dörnberg <[hidden email]> wrote:

> Am 30.10.2011 21:50, schrieb Stefan Reich:
> ...
>>
>> I really do hope that lbcv covers all the possible violations. Having
>> a safe way of loading untrusted bytecode is quite crucial to what I
>> want to be able to do with Mobile Lua.
>
> ...
>
> Do you really have to "load untrusted bytecode"?
> Is not it enough or even better to load cryptographically signed bytecode?
>
> Greetings
> Frank
>
>

Reply | Threaded
Open this post in threaded view
|

Re: Bytecode: Safe or not? / luac manual

Duncan Cross
On Mon, Oct 31, 2011 at 12:46 PM, Axel Kittenberger <[hidden email]> wrote:
> Since lua-jit only supports source code, why use byte code at all?

The latest version of LuaJIT2 (beta8) actually does support byte code
- though its own form, not compatible with standard Lua's:

<http://lua-users.org/lists/lua-l/2011-06/msg01052.html>

See the "Bytecode loading/saving" section.

-Duncan

Reply | Threaded
Open this post in threaded view
|

Re: Bytecode: Safe or not? / luac manual

liam mail
In reply to this post by Axel Kittenberger
On 31 October 2011 12:46, Axel Kittenberger <[hidden email]> wrote:
> Since lua-jit only supports source code, why use byte code at all?
>
What do you mean by that? LuaJIT supports bytecode and is not platform specific.

http://article.gmane.org/gmane.comp.lang.lua.general/80228

Reply | Threaded
Open this post in threaded view
|

Re: Bytecode: Safe or not? / luac manual

Luiz Henrique de Figueiredo
In reply to this post by Axel Kittenberger
> In case of speed: I suppose the state of affairs is that bytecode is
> only loaded faster if not checked. Any speedadvantage to parsing is
> eaten up by through untrusted bytecode checking.

Not really. Parsing still takes longer. But of course all this only
appplies to large programs. For everything else, both loading and
parsing are quite fast.

> In case of size: how much smaller is bytecode compared to source code
> that is say precompile-stripped of comments etc. and gzipped if at
> all?

Bytecode can be larger. Size reduction is not a goal in precompiling.
The goals are faster loading, protecting source code from accidental
user changes, and off-line syntax checking. Another goal is to allow
hosts to reduce their footprint by omitting the parser engine (lexer,
parser, code generator).

Reply | Threaded
Open this post in threaded view
|

Re: Bytecode: Safe or not? / luac manual

Stefan Reich
In reply to this post by Frank Meier-Dörnberg
Hi Frank! (Quite a few Germans on this list it seems.)

On Mon, Oct 31, 2011 at 11:47 AM, Frank Meier-Dörnberg <[hidden email]> wrote:
> Am 30.10.2011 21:50, schrieb Stefan Reich:
> ...
>> I really do hope that lbcv covers all the possible violations. Having
>> a safe way of loading untrusted bytecode is quite crucial to what I
>> want to be able to do with Mobile Lua.
>
> Do you really have to "load untrusted bytecode"?

Yes, that is the ultimate goal - and a really important one. Because
what I want is "total mobility".

(Heh, the term sounds a little... fascist. I can assure you it's not.)

By total mobility I mean an infrastructure of freely available
computation servers, open for everyone. Open like the WWW, email and
public streets.

For that, we need to run code from untrusted sources. If we require
trusted sources all the time, we cannot expand the system the way I
want it to expand.

> Is not it enough or even better to load cryptographically signed bytecode?

That is ok as an intermediate measure. But even then: Why would I want
anything I load to endanger my system - no matter where it came from?
Better to just make the system water-tight.

Stefan

Reply | Threaded
Open this post in threaded view
|

Re: Bytecode: Safe or not? / luac manual

Stefan Reich
In reply to this post by Axel Kittenberger
On Mon, Oct 31, 2011 at 12:46 PM, Axel Kittenberger <[hidden email]> wrote:
> Since lua-jit only supports source code, why use byte code at all?

Let me explain the principle once more.

Script S is run on machine A until it calls freeze().
It is then serialized into a Pluto image (or an image made by a future
library that is even better than Pluto).
The image is sent to machine B - which may or may not "trust" machine
A, it doesn't matter much.
There, it is deserialized and script S continues to compute. (Safely,
because of sandboxing.)
Later, the script may travel somewhere else again, of course.

Pluto requires saving and loading bytecode, so we need that ability
for this to work.

> In case of speed: I suppose the state of affairs is that bytecode is
> only loaded faster if not checked. Any speedadvantage to parsing is
> eaten up by through untrusted bytecode checking. In case of size: how
> much smaller is bytecode compared to source code that is say
> precompile-stripped of comments etc. and gzipped if at all?

Neither speed nor size are particularly important at this point.
Important, right now, is to get the system working and see Lua scripts
travel.

Stefan

Reply | Threaded
Open this post in threaded view
|

Re: Bytecode: Safe or not? / luac manual

Frank Meier-Dörnberg
In reply to this post by Stefan Reich
Am 31.10.2011 14:19, schrieb Stefan Reich:
> For that, we need to run code from untrusted sources.

Ah! In other words: It is not required that the code comes from one of
your own (friendly & trustworthy) pluto-serializers.
The code may come from the vicious and sneaky side.

You want to continue not only pure (byte)code, you want to reinstantiate
a full Lua-State from a pluto-like image, right?
Even a flawless byte code verifier is not the right tool to verify a
Lua-State, by all I'm able to imagine.

So it may be better to verify the source of the pluto-image than the
image itself ?!

--Frank


Reply | Threaded
Open this post in threaded view
|

Re: Bytecode: Safe or not? / luac manual

Stefan Reich
On Mon, Oct 31, 2011 at 5:28 PM, Frank Meier-Dörnberg <[hidden email]> wrote:
> Am 31.10.2011 14:19, schrieb Stefan Reich:
>>
>> For that, we need to run code from untrusted sources.
>
> Ah! In other words: It is not required that the code comes from one of your
> own (friendly & trustworthy) pluto-serializers.

Yes, exactly.

> The code may come from the vicious and sneaky side.

Hah... yes, if you'd like to call it that.

> You want to continue not only pure (byte)code, you want to reinstantiate a
> full Lua-State from a pluto-like image, right?

Yes.

> Even a flawless byte code verifier is not the right tool to verify a
> Lua-State, by all I'm able to imagine.

Well, it's one part. The other part would be a Pluto image verifier
which, among other things, calls the bytecode verifier for all
bytecode chunks.

I mean, this is an engineering task. No more no less. I don't know
exactly how much work it is, but I don't think it would take all that
long if a skilled engineer gets to work on it.

And I know there are some real Lua internals experts even on this very list :)

> So it may be better to verify the source of the pluto-image than the image
> itself ?!

Hm, what do you mean, "verify the source"? The "it's someone I know,
so the code is probably fine " thing?

Well that is something we can do: distinguish between trusted and
random sources. But I still want to be able to process code from
random sources. That's kind of the whole point.

What would Java be without the Java sandbox? It allows you to run
untrusted code and it was one of the main reason why Java took off
that quickly back then.

Same with JavaScript. Imagine JavaScript running "trusted" code only.
Would it still be as useful? Your machine would be in danger every
time you browse an unknown website.

No no no. The point of Mobile Lua is to make a robust sandbox for ANY
Lua code (frozen or "virgin"). With a sandbox like that, it will soar.
Because then you can offer computing services to anyone. No worries -
maximum power!

Cheers,
Stefan

Reply | Threaded
Open this post in threaded view
|

Re: Bytecode: Safe or not? / luac manual

Javier Guerra Giraldez
On Mon, Oct 31, 2011 at 1:15 PM, Stefan Reich
<[hidden email]> wrote:
> Same with JavaScript. Imagine JavaScript running "trusted" code only.
> Would it still be as useful? Your machine would be in danger every
> time you browse an unknown website.

AFAICT, javascripts VMs trust only locally-generated bytecode (or
JIT-ed machine language, or executable ASTs or whatever they execute).
 everything is received as source code

--
Javier

Reply | Threaded
Open this post in threaded view
|

Re: Bytecode: Safe or not? / luac manual

Jorge Visca
In reply to this post by Stefan Reich
On lun, 2011-10-31 at 18:15 +0000, Stefan Reich wrote:
> I mean, this is an engineering task. No more no less. I don't know
> exactly how much work it is, but I don't think it would take all that
> long if a skilled engineer gets to work on it.

No amount of engineering will solve the Halting problem.


Reply | Threaded
Open this post in threaded view
|

Re: Bytecode: Safe or not? / luac manual

Stefan Reich
On Mon, Oct 31, 2011 at 7:32 PM, Jorge <[hidden email]> wrote:
> On lun, 2011-10-31 at 18:15 +0000, Stefan Reich wrote:
>> I mean, this is an engineering task. No more no less. I don't know
>> exactly how much work it is, but I don't think it would take all that
>> long if a skilled engineer gets to work on it.
>
> No amount of engineering will solve the Halting problem.

Sorry, but what does this have to do with anything discussed before?
Don't you rather want to contribute something related to the topic?

Stefan

Reply | Threaded
Open this post in threaded view
|

Re: Bytecode: Safe or not? / luac manual

steve donovan
On Tue, Nov 1, 2011 at 3:42 PM, Stefan Reich
<[hidden email]> wrote:
> Sorry, but what does this have to do with anything discussed before?

But it is relevant; in theory it is impossible to tell whether a
foreign script will ever finish executing. Hence the need for
time-outs and memory limits, etc.

Personally I feel that it's best to pass code as text, rather than bytecode.

You will also need a clever security model so some trusted scripts can
actually do something on the machines they run on.

steve d.

Reply | Threaded
Open this post in threaded view
|

Re: Bytecode: Safe or not? / luac manual

Rob Kendrick-2
In reply to this post by Stefan Reich
On Tue, Nov 01, 2011 at 01:42:17PM +0000, Stefan Reich wrote:
> On Mon, Oct 31, 2011 at 7:32 PM, Jorge <[hidden email]> wrote:
> > On lun, 2011-10-31 at 18:15 +0000, Stefan Reich wrote:
> >> I mean, this is an engineering task. No more no less. I don't know
> >> exactly how much work it is, but I don't think it would take all that
> >> long if a skilled engineer gets to work on it.
> >
> > No amount of engineering will solve the Halting problem.
>
> Sorry, but what does this have to do with anything discussed before?

The halting problem is impossible to solve.  A byte code verifier is a
halting problem.  Thus, a perfect byte code verifier cannot exist.

> Don't you rather want to contribute something related to the topic?

He did.  And as a bonus, he didn't bring up some fantasy about us not
using money by next year.  *That* is off-topic.

B.

Reply | Threaded
Open this post in threaded view
|

Re: Bytecode: Safe or not? / luac manual

Stefan Reich
In reply to this post by steve donovan
Hi Steve!

On Tue, Nov 1, 2011 at 1:50 PM, steve donovan <[hidden email]> wrote:
> On Tue, Nov 1, 2011 at 3:42 PM, Stefan Reich
> <[hidden email]> wrote:
>> Sorry, but what does this have to do with anything discussed before?
>
> But it is relevant; in theory it is impossible to tell whether a
> foreign script will ever finish executing. Hence the need for
> time-outs and memory limits, etc.

Yes, there is a need for that. We just implement those limits - as
long as computers are finite creatures, there are limits anyway.

> Personally I feel that it's best to pass code as text, rather than bytecode.

Yeah, I'd love to do that. Easier and more readable. But I also want
running scripts to migrate between machines (with no programming
overhead) - and that only seems to work with serialized bytecode at
this point.

We start with source code in step 1 though (when new scripts are run)
- from steps 2 on (script migration) we transfer Pluto images.

> You will also need a clever security model so some trusted scripts can
> actually do something on the machines they run on.

They can already compute anything that can be computed. Local
interaction is an additional benefit that we can add gradually. Yes,
security comes into play there. It's a new field for intelligent
creation. :)

Best,
Stefan

Reply | Threaded
Open this post in threaded view
|

Re: Bytecode: Safe or not? / luac manual

Stefan Reich
In reply to this post by Rob Kendrick-2
On Tue, Nov 1, 2011 at 1:51 PM, Rob Kendrick <[hidden email]> wrote:

> The halting problem is impossible to solve.  A byte code verifier is a
> halting problem.  Thus, a perfect byte code verifier cannot exist.

What? How is a byte code verifier a halting problem? Doesn't it depend
on the format of the byte code and how the VM operates?

Verification, to me, means assuring the byte code will not crash the
VM or access internals in wrong ways.

That is easily possible with many VMs. For example, a C64 emulator can
in all likelihood not be crashed by bad C64 code. It just doesn't work
that way as 6510 assembly instructions are easy to control. (Only
controlled halting of the VM is possible.)

Also, I once wrote a VM for an assembly language with only one
instruction. That was also very easily verifiable bytecode.

Also, Java has a bytecode verifier that, AFAIK, has no known vulnerabilities.

So a bytecode verifier is obviously different from a halting problem.

>> Don't you rather want to contribute something related to the topic?
>
> He did.  And as a bonus, he didn't bring up some fantasy about us not
> using money by next year.  *That* is off-topic.

Haha. No it's not. It's extremely important and very real. Because
many people believe - wrongly - that money is something that will
continue to exist. And base their lives on this fantasy.

I offer you reality. Are you ready for it? Seems like you're a little
outside of it, Rob.

And since you chose to attack me: Who are you anyway? All I found on
your homepage is:

"Rob Kendrick has no website design skills."

Sounds... uhm, "impressive" :)

Cheers,
Stefan

Reply | Threaded
Open this post in threaded view
|

Re: Bytecode: Safe or not? / luac manual

Jorge Visca
In reply to this post by Stefan Reich
On mar, 2011-11-01 at 13:42 +0000, Stefan Reich wrote:

> On Mon, Oct 31, 2011 at 7:32 PM, Jorge <[hidden email]> wrote:
> > On lun, 2011-10-31 at 18:15 +0000, Stefan Reich wrote:
> >> I mean, this is an engineering task. No more no less. I don't know
> >> exactly how much work it is, but I don't think it would take all that
> >> long if a skilled engineer gets to work on it.
> >
> > No amount of engineering will solve the Halting problem.
>
> Sorry, but what does this have to do with anything discussed before?
> Don't you rather want to contribute something related to the topic?

Sorry it came trough as a being nasty, it wasn't the intention.

There are inherent limits to what can be done with automatic
verification. You should define the scope of what you want to verify and
check its feasibility, before you put it on your feature list and start
throwing resources at it.

The effort needed do satisfy different level of correctness grown very
fast, and jumps to infinite surprisingly fast.


123