Re: gaping security hole

[Tomas Z. <zel...@gm...>]

On 10/12/05, Don Cohen <don...@is...> wrote:
>
>  > > For a start I think it would be sufficient to have only as much
>  > > assurance as we have for other implementations already in common use=
.
>  > Agreed.
> This leads to investigation of restrictions on java applets.
> http://java.sun.com/docs/books/tutorial/applet/overview/security.html
> (That also, in my mind revives the problem of threads - if java has
> 'em then maybe they're not as hard to add to lisp as I imagine.)
>
>  -  An applet cannot load libraries or define native methods.
> I assume this means running arbitrary machine instructions
>  - It cannot ordinarily read or write files on the host that's
>   executing it.
> my restrictions on open
>  - It cannot make network connections except to the host that it came
>   from.
>  - It cannot start any program on the host that's executing it.
>  - It cannot read certain system properties.
> not clear what harm this can do, but equally hard to see why the
> applet needs to know
>  - Windows that an applet brings up look different than windows that an
>   application brings up.
> Well, that raises another problem - applets might want access to the
> screen (for that matter sound), which lisp doesn't provide.
>
> Another small point - if you want to share one lisp among multiple
> applets then you probably want to put each in its own package, prevent
> them from changing things in other packages.  There also seems to be
> some restriction about calling methods only from your own page.
> Sharing an image makes threads even more desirable, of course.
>
> The fact that bugs/vulnerabilities have been found in JVM
> implementations suggests that they have not been verified in the
> sense we might like.
>
> http://java.sun.com/sfaq/verifier.html
> There's a whole topic about verification of byte code but I don't
> quite understand the problem this is supposed to solve.  What can
> go wrong if you're allowed to execute arbitrary byte codes in
> arbitrary order?  I have a feeling this is related to trying to
> save some checking overhead by making use of strong typing.
> I wonder whether anything goes wrong in clisp if you execute
> arbitrary byte codes.
>
>  > > I'll look into it a bit further.  Of course, I hope others on this
>  > > list will help me out.
>  > I am certainly interested in this.
> At some level it's very straight forward to understand the sort of
> proof we want.  For instance I'd just like to prove that there's
> SOME instruction that cannot be executed by running the applet
> (I'm mainly trying to prove it can't do anything it wants).
> What I was vaguely remembering when I wrote the last message is
> work on "proof carrying code" where the applet contains a proof
> that it obeys some policy and the machine receiving the applet can
> easily verify the proof before running the code.
>
> Even better than a separate proof for each applet would be a single
> proof for all applets, i.e., showing that a given lisp implementation
> compiled with appropriate flags, no matter what input it gets, can
> never execute some instruction.  I'd hope this would actually be the
> case, so it makes sense to try to prove it.
>
> Naturally, this proof tends to depend on the size of the program (in
> this case the lisp implementation).  This suggests removing as much
> code as possible from the implementation, which seems obvious, but the
> result in the case of clisp is still going to be very large by
> standards of proofs.  Actually, we gain a great deal here by the fact
> that a lot of the code is written in lisp, and that code need not be
> verified since it could have been supplied by the applet.  But the
> remaining c code is still very large.  There's also an issue of
> whether to try to verify c code or compiled code.  The c code might
> seem better cause (a) it's much smaller and (b) the same proof would
> then apply to all binary versions generated from it.  Unfortunately,
> these advantages are lost (and then some) when you realize that it
> becomes necessary to verify the compiler(s) you use.
>

I still think that
- you would need huge amount of time to make the code reduction, not
even talking about proof, and you will always have to solve what to
add and what not (differents requirements).
- safer way in general is to add approved, not remove dangerous features

I think that for what you need (safe snippets of foreign code in your
program), the first approximation would better be something on high
level - something like compile/load with modified readtable (even
without colon, or better with colon modified to allow access only to
keyword package) and with fixed purpose-made package that imports only
approved subset of common-lisp package (catching attempts to redefine
it so that rest of code is not modified). This way, you could find out
what is really needed by users, and have some level of security soon.

Just an opinion.

Tomas