RE: Extensions review

["Dodier-Lazaro, Steve" <s dodier-lazaro 12 ucl ac uk>]

Hi,

> [...]
>
> You cannot be "absolutely certain" that the code does not trigger a
> buffer overflow (or jump to an arbitrary heap address or whatever) you
> cannot prove security for non trivial cases you can only
> prove non security.

Well, I really don't know JS. I'm not sure exactly what you mean by non-trivial,
surely it's hard to prove non-trivial properties such as program termination in
a general way, but we could already specify a bit what it is that extensions are:

- code written in the JavaScript language (obviously)
- non-deterministic code, or is it?*

Really, I can't stress how I don't know enough of JS to give any useful pointers,
but I'm aware that there are a number of subsets to the language on which people
can run verifiers. So surely there are certain security properties that can be
proved on certain JS programs. I'd intuitively state that simple properties like
non-interference (but between what and what? :) ) could be sometimes proved on 
some extensions. Maybe what subset of the Shell is exposed to clients and what
subsets of JS are implemented in GJS can play a role for directed static analysis.

Where it really hurts is that each extension is unique, and you may want to prove
different things in each of them; and of course the proof is only valid modulo bugs in
GJS. You could reframe or instrument the Shell to allow for some analysis methods,
but you'd still need reviewers who took a language-based security/program analysis
class to know what to do with the tools!

* how are threads created? can extensions make threads? if so, what for? basic
map-reduce like parallelism, or do they e.g. treat multiple clients depending on
the order in which they reach a shared resource? do they actually have a
non-deterministic behaviour or merely a non-deterministic implementation? Some
people also manage to prove things on some non-det programs.

 
> Also why would you try to run shell code if you can simply eval() a JS
> string that you get from somewhere ... would be way easier.

eval() might be a bit obvious :) Even I know that! I had in mind typing my previous
email the charming people who write advanced persistent threat malwares. Shell
extensions really have all the properties you'd expect from a backdoor, so they
shouldn't be treated lightly... It's great that you have a code review in place,
something which probably does not happen with many FOSS projects -- and that's
what brings me to commenting on it in the first place: what can you improve to make
sure that it delivers as much as you'd expect?

 
> But anyway hidding in an extension in a way to not get noticed by a
> reviewer (i.e it has to look like legit code that does something
> useful) is not as trivial as you might think.

It's certainly not trivial for me :)
--
Steve Dodier-Lazaro
PhD student in Information Security
University College London
Dept. of Computer Science
Malet Place Engineering, 6.07
Gower Street, London WC1E 6BT
OpenPGP : 1B6B1670