Looking for an idea for security related project
Daniel Hans
my name is Daniel and I am a student from Poland. I am currently
looking for an objective for my master thesis at University of Warsaw.
When I was visiting Google office in New York at the beginning of
January, I had a chance to meet Nick Santos from Google Closure with
whom I talked about possibilities of working on one of Google open
source projects. He suggested the caja project, as it is strongly
related to security. After I got back to Poland, I checked the project
which seemed to be very promising and interesting. Nicolas contacted
someone of you and advised me to post to this list. First of all I
would like to apologize for writing so late. I had some extremely time
consuming university related issues, thus really needed to focus on
them. Fortunately now I have a plenty of time, so it is not a
limitation anymore.
You also suggested specifying what type of project I would like to
work on. To be honest I have to admit I do not know :-) I am very new
to caja project and does not know what are the priorities or even what
needs to be done. Anyway, I am completely open to your ideas. Just to
clarify: it must fit for a master thesis project, so before the actual
work it will have to be approved by my tutor. He is also very
receptive and willing to negotiate. The only constraint is that it
must be security related. I have seen some issues on your tracker, but
I am not sure if they would be ok for a master thesis. Maybe do you
have in mind something which is not listed? Also, I would really
appreciate if the project idea was well-defined and doable. For
example, a feature which would be really nice to have, but you cannot
work on it, as the caja team has limited resources. By doable I mean
it will not turn out that it literally cannot be done at some stage of
work, because I will end up with nothing :-P However, the idea may
still require doing some research. As I said, I am very open. If you
have some questions, or need any additional information before
deciding if (and possibly on what) I could work on your project,
please feel free to ask me.
I am really looking forward to hearing from you.
Regards,
Daniel
Mike Samuel
> Hello Caja team,
>
> my name is Daniel and I am a student from Poland. I am currently
> looking for an objective for my master thesis at University of Warsaw.
> When I was visiting Google office in New York at the beginning of
> January, I had a chance to meet Nick Santos from Google Closure with
> whom I talked about possibilities of working on one of Google open
> source projects. He suggested the caja project, as it is strongly
> related to security. After I got back to Poland, I checked the project
> which seemed to be very promising and interesting. Nicolas contacted
> someone of you and advised me to post to this list. First of all I
> would like to apologize for writing so late. I had some extremely time
> consuming university related issues, thus really needed to focus on
> them. Fortunately now I have a plenty of time, so it is not a
> limitation anymore.
Great. Was it Mark Miller that you corresponded with?
> You also suggested specifying what type of project I would like to
> work on. To be honest I have to admit I do not know :-) I am very new
> to caja project and does not know what are the priorities or even what
> needs to be done. Anyway, I am completely open to your ideas. Just to
> clarify: it must fit for a master thesis project, so before the actual
> work it will have to be approved by my tutor. He is also very
What's your background? How familiar are you with web application
security, language based security, etc.?
Are you looking to do something like formally prove that caja has this
or that property?
Are you interested in researching a class of attacks and discussing
how caja does or does not address that class of attack?
Would you be interested in demonstrating how to build applications
with interesting security properties on top of caja?
Would you be interested in trying to find ways to penetrate caja, and
maybe suggest how caja could be hardened against any attacks you find?
How much time have you got to work on this?
> receptive and willing to negotiate. The only constraint is that it
> must be security related. I have seen some issues on your tracker, but
> I am not sure if they would be ok for a master thesis. Maybe do you
> have in mind something which is not listed? Also, I would really
> appreciate if the project idea was well-defined and doable. For
What good are volunteers if you can't unload impossible tasks on them? :)
Daniel Hans
thanks for your response!
On Feb 19, 2:11 am, Mike Samuel <mikesam...@gmail.com> wrote:
> 2010/2/19 Daniel Hans <daniel.m.h...@gmail.com>:
>
> > Hello Caja team,
>
> > my name is Daniel and I am a student from Poland. I am currently
> > looking for an objective for my master thesis at University of Warsaw.
> > When I was visiting Google office in New York at the beginning of
> > January, I had a chance to meet Nick Santos from Google Closure with
> > whom I talked about possibilities of working on one of Google open
> > source projects. He suggested the caja project, as it is strongly
> > related to security. After I got back to Poland, I checked the project
> > which seemed to be very promising and interesting. Nicolas contacted
> > someone of you and advised me to post to this list. First of all I
> > would like to apologize for writing so late. I had some extremely time
> > consuming university related issues, thus really needed to focus on
> > them. Fortunately now I have a plenty of time, so it is not a
> > limitation anymore.
>
> Great. Was it Mark Miller that you corresponded with?
>
I am sorry, maybe I was not clear enough. I just corresponded with
Nicolas, from Closure team, who said that had written someone from
caja team, but I do not know whom.
> > You also suggested specifying what type of project I would like to
> > work on. To be honest I have to admit I do not know :-) I am very new
> > to caja project and does not know what are the priorities or even what
> > needs to be done. Anyway, I am completely open to your ideas. Just to
> > clarify: it must fit for a master thesis project, so before the actual
> > work it will have to be approved by my tutor. He is also very
>
> What's your background? How familiar are you with web application
> security, language based security, etc.?
>
About web security, I am aware of some types of popular attacks and
when I develop a web application, I try to prevent them (usually on
server side, but also on JS) and find holes in existing code. Also, I
gave a speech about HTTP Response Splitting vulnerability at my
university. Actually I do not have much experience with security
oriented programming. My first contact with Caja truly demonstrates
that it is powerful in this area. Anyway, now I am learning so as to
understand its foundations. I have started to read about not only
about object capability model, but also about the E language, which
caja may potentially inherit from. I think it can be useful for better
comprehension of the concepts in caja itself. I would be grateful for
any clues on what I should pay most attention.
> Are you looking to do something like formally prove that caja has this
> or that property?
> Are you interested in researching a class of attacks and discussing
> how caja does or does not address that class of attack?
> Would you be interested in demonstrating how to build applications
> with interesting security properties on top of caja?
> Would you be interested in trying to find ways to penetrate caja, and
> maybe suggest how caja could be hardened against any attacks you find?
>
> How much time have you got to work on this?
I have plenty of time that I am willing to spend on the project, so if
we came up with a project idea and you direct me what I should focus
on, I will do everything I can to complete it successfully. I am not
sure if I can give you any exact numbers now, but I am planning to
work for about 12-20 hours a week. To be honest I have to admit that I
am not sure what is the firm date when master thesis projects must be
completed at my university, but probably it should be fine if I give
it to my tutor for review by June.
> > receptive and willing to negotiate. The only constraint is that it
> > must be security related. I have seen some issues on your tracker, but
> > I am not sure if they would be ok for a master thesis. Maybe do you
> > have in mind something which is not listed? Also, I would really
> > appreciate if the project idea was well-defined and doable. For
>
> What good are volunteers if you can't unload impossible tasks on them? :)
That is a good point, but I would need to provide my tutor with an
excellent justification to receive his positive opinion :-)
Looking forward to hearing from you.
Mike Samuel
Daniel Hans
thanks you for giving me directions. Last week I had some time to play
more with caja. I think I would prefer to work on the core if it is
possible. I have more experience in working with Java than with
Javascript, but I do not recognize it as a serious problem.
Do you have any ideas on what could be added/implemented in this area?
Then, once I have it accepted by my tutor, I can start working 'full-
time'. Maybe do you have some smaller issues which I could start from?
That would be helpful for getting more familiar with code, etc.
I can also ask Nicolas for explaining me again the idea that we talked
about when we meet in NYC. I do not think I am able to recall all
details after two months. Anyway, I remember the problem that he was
not sure that it was achievable in all parts.
I also saw the open problems on caja wiki page. The one with formal
semantics seems to be noteworthy. Could anyone explain a bit more what
do you have in mind? It may be difficult in general, but I have dealt
with some simple semantics in various forms. One can explicitly write
down the entire semantics on paper and prove all statements, but there
are also more modern approaches like adding a list of assertions to
the code. There is also JML which is a formal method of defining
behavioral specification. Has anyone ever started working on it? I
would like to know what level of, let us say, abstraction you want to
introduce. Some examples? Anyhow, I am not sure if my tutor would
agree on that. Although my university does a lot of theoretical
research, he is the one who prefers implementation work and that is
mostly why I would prefer to take up something with the codebase.
Regards,
Daniel
On Feb 23, 10:34 pm, Mike Samuel <mikesam...@gmail.com> wrote:
> 2010/2/22 Daniel Hans <daniel.m.h...@gmail.com>
Mark Miller
Hi Daniel,
Since you also have a Java background, I'm wondering whether you might
be interested in building towards something we've long wanted, which
can be summarized (too simply) as
GWT(Joe-E) => Caja-compatible JS
Taking this apart,
GWT, the Google Web Toolkit, is a translator from a subset of Java to
the JavaScript that runs in browsers.
Joe-E is a subset of Java with object-capability security properties.
The subset chosen by Joe-E is similar in many way to the subset chosen
by GWT, even though the subsetting had very different motivations.
Caja is of course a subset of JS with ocap security properties,
implemented by a translator from Caja to the JS that runs in browsers.
What we'd like to understand and eventually build is a GWT variant
that, when given code that verifies as valid Joe-E, i.e., is in the
intersection of the GWT and Joe-E subsets of Java, translates to JS
code that 1) preserves not just the semantics of the original Java but
also preserves its security semantics, and 2) is security
link-compatible with the output of the Caja translator.
By #2, I mean that the JS resulting from translating GWT/Joe-E code
and the JS resulting from translating Caja code can be linked
together, confident that neither can violate the security properties
the other relies on.
To harmonize the interplay of these technologies, niether GWT, Caja,
nor Joe-E should be taken as written in stone. Minor
security-preserving adjustments to each to bring them into alignments
with the others can be considered. Probably the first step is to
understand what the GWT-Joe-E intersection looks like, and what is
needed to make this as practical a language a GWT and Joe-E are
individually.
Please let me know if this sounds like an interesting direction, in
which case I can provide further guidance. And thanks for the offer!
--
Cheers,
--MarkM
Daniel Hans
First of all, thank your for your response! The project sounds very
interesting and will definitely want to work on that. I suppose it may
be also decent foundation for a master thesis as it requires both
reaseach to (as you said) understand and implementation.
I had a chance to try out GWT some time ago and think it is a powerful
and interesting solution especially for those developers who are not
keen on JavaScript. I did not work on any professional projects with
GWT, but I was surprised at being able to create some cool ajax
gadgets with very some limited amount of code.
To be fair, I have not heard much about Joe-E, but I took a glance
today and it seems to me that the motivation is somehow similar to
Caja's one. I mean Caja is a strict subset of JS which allows to
preserve some security capabilities, while Joe-E tries to achieve the
same in Java. Therefore it sounds sane to start from finding the
intersection of GWT and Joe-E and find out whether it has some sense
or not.
If it does, it is perfect - I could start building some initial
implementation. On the other hand, what if the intersection turns out
to be useless at some point? Then, it will require some changes to
either GWT or Joe-E, won't it? I suspect it might be easier to modify
GWT, as with Joe-E one needs to make sure that all security
capabilities and invariants are preserved.
In the upcoming days I will be trying to single out the intersection.
I am going to work as intensively as I can. On Thursday I will talk
with my tutor if the project idea is appropriate, but I think he
should be fine.
I have seen this project on the ideas page with potential GSoC
projects [0]. There are reasons I will probably not be able to
participate as a student this year. First of all, I am planning to be
a mentor for Melange, which is a Google project whose aim is to
represent open source contribution programs (like GSoC or GHOP).
Secondly, there is a chance that I will be doing internship at Google
this summer. As far as I know, at this moment they are looking for a
project which I could work on. I have not been contacted recently, so
I am afraid that cannot find anything. Btw. if you are in need of an
intern, you can ping my recruiter:-P Anyway, if you prefer to have a
GSoC student for the project, please tell me and I will see what I can
do.
Looking forward to hearing from you.
Regards,
Daniel
[0] http://code.google.com/p/google-caja/wiki/ProjectIdeas
On Mar 16, 6:55 pm, Mark Miller <erig...@gmail.com> wrote:
> On Tue, Mar 9, 2010 at 6:38 AM, Daniel Hans <daniel.m.h...@gmail.com> wrote:
> > Hey,
>
> > thanks you for giving me directions. Last week I had some time to play
> > more with caja. I think I would prefer to work on the core if it is
> > possible. I have more experience in working with Java than with
> > Javascript, but I do not recognize it as a serious problem.
> > Do you have any ideas on what could be added/implemented in this area?
> > Then, once I have it accepted by my tutor, I can start working 'full-
> > time'. Maybe do you have some smaller issues which I could start from?
> > That would be helpful for getting more familiar with code, etc.
> > I can also ask Nicolas for explaining me again theideathat we talked
Daniel Hans
first of all, apologies for my mistake in your name in my previous
email. In my defense, it was very late in Poland when I was writing.
Today I did some very initial checking for similarities between Google
Web Toolkit and Joe-E. Fortunately the particular Java subsets are
not disjoint, but I hoped they would have more in common.
There are some explicit differences, but after thinking for a while
they are not restrictive regarding expressiveness. For example, using
finally is forbidden in Joe-E, as it might be awkward if an exception
is thrown within the finally block. Anyway, as far as I know, each
piece of code which uses finally may be rewritten without it and still
do exactly the same.
Maybe there are more sophisticated constraints in Joe-E, but I will
try to locate them later. Currently, I have a bigger concern which I
would like to clarify as soon as possible. Could you explain me what
exactly you meant by Java subset chosen by Google Web Toolkit? I am
asking because it is a bit ambiguous which part of GWT application
should be a valid Joe-E.
A web developer which works on a GWT project may use classes which
belong to available subset of Java 2 SE or to GWT library which
contains more than 700 classes. Should all of them validate as correct
Joe-E? Or can we assume that they are harmless and verify only files
that were created by the developer? I am asking because I have seen
different approaches. For instance, in Google Native Client each
module consists of trusted and untrusted parts and only code in the
former one is sandboxed.
Also, I have a tremendous concern about the classes of GWT library.
The main reason of secure oriented programming is to guarantee some
security properties. Joe-E tries to ensure that memory safe property
is not broken and achieves it mostly by disabling native methods which
may cause serious leaks.
However, GWT uses a lot of native methods in JavaScript Native
Interface. They are declared with commented-out bodies which contain
JavaScript. After compilation, GWT incorporates the JavaScript. It is
a very thoughtful idea, but it will certainly not validate as a Joe-E
file, because native methods are severely forbidden. I am not sure if
the methods might be replaced, as JavaScript Native Interface seems to
be a fundamental facility of GWT.
Do you think we need to take these methods into account and deal with
them somehow? Maybe we should allow them at this stage and verify they
after GWT=>JS translation? What do you think?
Looking forward to hearing from you.
Regards,
Daniel
On Mar 16, 6:55 pm, Mark Miller <erig...@gmail.com> wrote:
Mike Samuel
> Hello Mark,
>
> first of all, apologies for my mistake in your name in my previous
> email. In my defense, it was very late in Poland when I was writing.
>
> Today I did some very initial checking for similarities between Google
> Web Toolkit and Joe-E. Fortunately the particular Java subsets are
> not disjoint, but I hoped they would have more in common.
>
> There are some explicit differences, but after thinking for a while
> they are not restrictive regarding expressiveness. For example, using
> finally is forbidden in Joe-E, as it might be awkward if an exception
> is thrown within the finally block. Anyway, as far as I know, each
> piece of code which uses finally may be rewritten without it and still
> do exactly the same.
Joe-E is not rewriter based. It is a verifier -- if it says the Java
is safe to run, then you can compile and run it as-is.
You can get pretty close, but you can't rewrite finally to be
semantics preserving because you can't intercept OutOfMemoryErrors or
StackOverflowErrors.
> Maybe there are more sophisticated constraints in Joe-E, but I will
> try to locate them later. Currently, I have a bigger concern which I
> would like to clarify as soon as possible. Could you explain me what
> exactly you meant by Java subset chosen by Google Web Toolkit? I am
> asking because it is a bit ambiguous which part of GWT application
> should be a valid Joe-E.
> A web developer which works on a GWT project may use classes which
> belong to available subset of Java 2 SE or to GWT library which
> contains more than 700 classes. Should all of them validate as correct
> Joe-E? Or can we assume that they are harmless and verify only files
> that were created by the developer? I am asking because I have seen
> different approaches. For instance, in Google Native Client each
> module consists of trusted and untrusted parts and only code in the
> former one is sandboxed.
Joe-E provides a library layer as well as a verifier. See the
"Browseable Joe-E/Java API docs (taming-aware)" link on the right of
http://code.google.com/p/joe-e/
> Also, I have a tremendous concern about the classes of GWT library.
> The main reason of secure oriented programming is to guarantee some
> security properties. Joe-E tries to ensure that memory safe property
> is not broken and achieves it mostly by disabling native methods which
> may cause serious leaks.
>
> However, GWT uses a lot of native methods in JavaScript Native
> Interface. They are declared with commented-out bodies which contain
> JavaScript. After compilation, GWT incorporates the JavaScript. It is
> a very thoughtful idea, but it will certainly not validate as a Joe-E
> file, because native methods are severely forbidden. I am not sure if
> the methods might be replaced, as JavaScript Native Interface seems to
> be a fundamental facility of GWT.
> Do you think we need to take these methods into account and deal with
> them somehow? Maybe we should allow them at this stage and verify they
> after GWT=>JS translation? What do you think?
I think you're right.
The native JS methods can contain references to java classes and
methods. I think those would need to be validated somehow. Then the
resulting JS produced from that would have to obey normal caja rules.
> To unsubscribe from this group, send email to google-caja-discuss+unsubscribegooglegroups.com or reply to this email with the words "REMOVE ME" as the subject.
>
David-Sarah Hopwood
> Also, I have a tremendous concern about the classes of GWT library.
> The main reason of secure oriented programming is to guarantee some
> security properties. Joe-E tries to ensure that memory safe property
> is not broken and achieves it mostly by disabling native methods which
> may cause serious leaks.
>
> However, GWT uses a lot of native methods in JavaScript Native
> Interface. They are declared with commented-out bodies which contain
> JavaScript. After compilation, GWT incorporates the JavaScript. It is
> a very thoughtful idea, but it will certainly not validate as a Joe-E
> file, because native methods are severely forbidden. I am not sure if
> the methods might be replaced, as JavaScript Native Interface seems to
> be a fundamental facility of GWT.
This seems surmountable by cajoling the commented-out body, and using
the result as the translation of the "native" method. That would be a
safe extension of Joe-E, I think; however, it might require significant
modifications to the GWT library to get all native methods to cajole
(bearing in mind that they must each cajole independently, i.e. can't
access unsafe globals or free variables).
--
David-Sarah Hopwood ⚥ http://davidsarah.livejournal.com
David-Sarah Hopwood
> Hello Mark,
>
> first of all, apologies for my mistake in your name in my previous
> email. In my defense, it was very late in Poland when I was writing.
>
> Today I did some very initial checking for similarities between Google
> Web Toolkit and Joe-E. Fortunately the particular Java subsets are
> not disjoint, but I hoped they would have more in common.
>
> There are some explicit differences, but after thinking for a while
> they are not restrictive regarding expressiveness. For example, using
> finally is forbidden in Joe-E, as it might be awkward if an exception
> is thrown within the finally block.
Note that it isn't really the intended functionality of the try/finally
construct that is a problem (in either Java or JavaScript), only the
details of what exceptions can be caught. The issue is that in the
obvious expansion (in JavaScript) of try/finally to try/catch:
try { S } finally { T }
<==>
try { S; T } catch ($e) { T; throw $e } // $e is fresh
the catch ($e) will catch any exception, even ones that would be
restricted from being caught in the language subset.
There's another issue with this expansion that is less important from
a security point of view, but not ideal from the point of view of
debuggability: if an exception is thrown in the finally clause, it
effectively overrides any exception thrown in the try clause, and so
information about the original exception that might have been useful
for debugging will be lost.
In Jacaranda (which uses static verification rather than translation),
the following library functions are provided to solve both problems:
/**
* Try-finally in Jacaranda must be written as follows:
* $tryFinally(function() {
* ...
* }, function() {
* ...
* });
*
* This solves two problems with JavaScript's try-finally construct:
* - if a nondeterministic exception (e.g. stack error) occurs, the
* code in the finally clause runs and may attempt to exploit
* corrupted state of the abstraction in which the exception
* occurred;
* - if an exception is thrown in the finally clause, it will
* effectively override any exception thrown in the try clause,
* and so information about the original exception will be lost.
*
* If an exception occurs in 'finallyClause', an immutable object will
* be thrown with the following properties:
* FinallyException: the exception that occurred in 'finallyClause'
* TryException: the exception that occurred in 'tryClause', or
* undefined
* TryExceptionOccurred: true if any exception occurred in
* 'tryClause', otherwise false
*/
function $tryFinally(tryClause, finallyClause) {
$tryCatchFinally(tryClause, undefined, finallyClause);
}
/**
* Equivalent to:
* $tryFinally(function() {
* try {
* tryClause();
* } catch (e) { $caught(e);
* if (catchClause !== undefined) { catchClause(e); }
* }
* }, finallyClause);
*/
function $tryCatchFinally(tryClause, catchClause, finallyClause) {
var tryExceptionOccurred = false;
var tryException;
try {
tryClause();
} catch (e) { $caught(e);
tryExceptionOccurred = true;
tryException = e;
if (catchClause !== undefined) {
try {
catchClause(e);
} catch (e2) { $caught(e2);
tryException = e2;
}
}
}
try {
finallyClause();
} catch (finallyException) { $caught(finallyException);
throw {FinallyException: finallyException,
TryExceptionOccurred: tryExceptionOccurred,
TryException: tryException,
toString: function() {
try {
return "FinallyException: first " + tryException +
"\nthen in finally clause, " + finallyException;
} catch (ee) { $caught(ee); return "FinallyException"; }
}};
}
if (tryExceptionOccurred) throw tryException;
}
> Anyway, as far as I know, each
> piece of code which uses finally may be rewritten without it and still
> do exactly the same.
Yes, for example using the functions above (or the Joe-E equivalents).
David-Sarah Hopwood
> 2010/3/22 Daniel Hans <daniel...@gmail.com>:
>> Hello Mark,
>>
>> first of all, apologies for my mistake in your name in my previous
>> email. In my defense, it was very late in Poland when I was writing.
>>
>> Today I did some very initial checking for similarities between Google
>> Web Toolkit and Joe-E. Fortunately the particular Java subsets are
>> not disjoint, but I hoped they would have more in common.
>>
>> There are some explicit differences, but after thinking for a while
>> they are not restrictive regarding expressiveness. For example, using
>> finally is forbidden in Joe-E, as it might be awkward if an exception
>> is thrown within the finally block. Anyway, as far as I know, each
>> piece of code which uses finally may be rewritten without it and still
>> do exactly the same.
>
> Joe-E is not rewriter based. It is a verifier -- if it says the Java
> is safe to run, then you can compile and run it as-is.
>
> You can get pretty close, but you can't rewrite finally to be
> semantics preserving because you can't intercept OutOfMemoryErrors or
> StackOverflowErrors.
Well, a ~Joe-E -> JS system would be a rewriter. The ~Joe-E language is a
static subset of Java, but that doesn't mean that it necessarily has to
be implemented as a static verifier connected to a Java implementation
(even if using the modified version of the existing Joe-E verifier to do
most of the checking).
In particular, for out-of-memory and stack overflow, it will always be
possible for the generated JS code to trigger those conditions even for
code that never uses finally (in the input ~Joe-E, or in libraries or
native methods). So we can only securely implement a fail-stop subset
of Java that stops when these conditions occur. Therefore, it's perfectly
OK to accept a Java 'try/finally' construct and translate it to JS code
(*not* using JS 'try/finally') that stops in those cases.
Mike Samuel
> Mike Samuel wrote:
>> 2010/3/22 Daniel Hans <daniel...@gmail.com>:
>>> Hello Mark,
>>>
>>> first of all, apologies for my mistake in your name in my previous
>>> email. In my defense, it was very late in Poland when I was writing.
>>>
>>> Today I did some very initial checking for similarities between Google
>>> Web Toolkit and Joe-E. Fortunately the particular Java subsets are
>>> not disjoint, but I hoped they would have more in common.
>>>
>>> There are some explicit differences, but after thinking for a while
>>> they are not restrictive regarding expressiveness. For example, using
>>> finally is forbidden in Joe-E, as it might be awkward if an exception
>>> is thrown within the finally block. Anyway, as far as I know, each
>>> piece of code which uses finally may be rewritten without it and still
>>> do exactly the same.
>>
>> Joe-E is not rewriter based. It is a verifier -- if it says the Java
>> is safe to run, then you can compile and run it as-is.
>>
>> You can get pretty close, but you can't rewrite finally to be
>> semantics preserving because you can't intercept OutOfMemoryErrors or
>> StackOverflowErrors.
>
> Well, a ~Joe-E -> JS system would be a rewriter. The ~Joe-E language is a
> static subset of Java, but that doesn't mean that it necessarily has to
> be implemented as a static verifier connected to a Java implementation
> (even if using the modified version of the existing Joe-E verifier to do
> most of the checking).
The rewriter here is GWT.
Joe-E is a validator. GWT would do the Java to JS step.
> In particular, for out-of-memory and stack overflow, it will always be
> possible for the generated JS code to trigger those conditions even for
> code that never uses finally (in the input ~Joe-E, or in libraries or
> native methods). So we can only securely implement a fail-stop subset
> of Java that stops when these conditions occur. Therefore, it's perfectly
> OK to accept a Java 'try/finally' construct and translate it to JS code
> (*not* using JS 'try/finally') that stops in those cases.
It doesn't claim to stop those errors. Only to disallow code from
trapping them.
Daniel Hans
thank you for your all responses.
> Joe-E is not rewriter based. It is a verifier -- if it says the Java
> is safe to run, then you can compile and run it as-is.
>
> You can get pretty close, but you can't rewrite finally to be
> semantics preserving because you can't intercept OutOfMemoryErrors or
> StackOverflowErrors
Yes, I had in mind replacing finally block with a equivalent block
without it. As it was pointed out by David-Sarah, those two blocks
have similar semantics in JavaScript.
try { S } finally { T }
<==>
try { S; T } catch ($e) { T;
throw $e } // $e is fresh
I think something very similar can be done in regular Java. Then, the
block will be a valid Joe-E. If I understand you Mike correctly, you
mean that I cannot intercept JVM Errors in Joe-E programs, right? I am
not worrying about it at this moment, because it is mentioned in GWT
documentation that these errors are not thrown, because it is not
possible to map all underlying JavaScript exception onto Java
exception types. Instead, JavaScriptException is thrown.
> The rewriter here is GWT.
> Joe-E is a validator. GWT would do the Java to JS step.
Yes, exactly. There is certainly no point in writing a new rewriter :)
Thanks to the Joe-E we can verify the Java code. Thus, we can assure
that some secure properties are met. Then the client side code is
translated/rewritten into JS. After that, we have translated code
which is merged with native JavaScript methods. However, if I
understand correctly, we need code which is caja-compatible. The naive
solution could to just cajole the code and check if it is valid.
Yesterday, I did it with some simple GWT project and it worked :-P On
the one hand, if the code is cajoable, it should be safe. On the other
hand, I think that we need to check what is the relation between
security properties that are enforced by caja and Joe-E. If there is a
relation Joe-E <= Caja, it should be fine, but otherwise, if Joe-E is
'stricter', there might be some problems. Also, we deal with two
different languages, so some aspects of one of them may be not
applicable to the other.
I will also have to understand what problems might be caused by what
you said: "the native JS methods can contain references to java
classes and methods". I think we really need to validate it. To come
up with an idea, I think I will have to understand in depth how the JS
code is actually created. Tomorrow I will try to find some
documentation in this area.
>> In particular, for out-of-memory and stack overflow, it will always be
>> possible for the generated JS code to trigger those conditions even for
>> code that never uses finally (in the input ~Joe-E, or in libraries or
>> native methods). So we can only securely implement a fail-stop subset
>> of Java that stops when these conditions occur. Therefore, it's perfectly
>> OK to accept a Java 'try/finally' construct and translate it to JS code
>> (*not* using JS 'try/finally') that stops in those cases.
> It doesn't claim to stop those errors. Only to disallow code from
> trapping them.
By "stop those errors" you mean that Joe-E is not able to prevent the
application from getting out of memory, do you? For example to
following code is obviously allowed:
LinkedList<Object> list = new LinkedList<Object>();
while(true) {
list.add(new Object());
}
Anyway, as you even mentioned before, "Joe-E provides a library layer
as well as a verifier". If you use just the verifier, you only get
information which parts of your code are not valid, but if you use
both of them, you can use Joe-E's ErrorHandler implementation. I
haven't tried it yet, but it seems it will terminate the application
as expected by Joe-E specification
However, as I mentioned above GWT documentation says that most JS
errors are thrown as JavaScriptException, so I will have to think how
to deal with them.
Regards,
Daniel
Mike Samuel
> Hello,
>
> thank you for your all responses.
>
>> Joe-E is not rewriter based. It is a verifier -- if it says the Java
>> is safe to run, then you can compile and run it as-is.
>>
>> You can get pretty close, but you can't rewrite finally to be > semantics preserving because you can't intercept OutOfMemoryErrors or > StackOverflowErrors
>
> Yes, I had in mind replacing finally block with a equivalent block
> without it. As it was pointed out by David-Sarah, those two blocks
> have similar semantics in JavaScript.
> try { S } finally { T } <==> try { S; T } catch ($e) { T;
> throw $e } // $e is fresh
> I think something very similar can be done in regular Java. Then, the
> block will be a valid Joe-E. If I understand you Mike correctly, you
> mean that I cannot intercept JVM Errors in Joe-E programs, right? I am
> not worrying about it at this moment, because it is mentioned in GWT
> documentation that these errors are not thrown, because it is not
> possible to map all underlying JavaScript exception onto Java
> exception types. Instead, JavaScriptException is thrown.
Joe-E prevents those from being trapped because it doesn't want
malicious code to do something like
* push max_stack_depth - 1 frames onto the stack
* call foo.bar()
* trap the stack overflow and observe foo in an inconsistent state
because bar() didn't complete.
The same attack will work in JS.
Exactly.
> Anyway, as you even mentioned before, "Joe-E provides a library layer
> as well as a verifier". If you use just the verifier, you only get
> information which parts of your code are not valid, but if you use
> both of them, you can use Joe-E's ErrorHandler implementation. I
> haven't tried it yet, but it seems it will terminate the application
> as expected by Joe-E specification
A container that wants to load and run Joe-E code can install an
UncaughtExceptionHandler that exits on untrapped Throwables, and a
SecurityManager that prevents untrusted code from trapping exit or
from changing the UncaughtExceptionHandler.
> However, as I mentioned above GWT documentation says that most JS
> errors are thrown as JavaScriptException, so I will have to think how
> to deal with them.
> Regards,
> Daniel
>