Proof of security

[benjamingr]

I think that it would be interesting (and important) to include a proof that it is impossible to escape the isolated realm and cause unconfined side effects. Assuming one is ready of course given your (Mark) previous work on the topic.

Optimally, this is something people can run and scrutinize on their computers and would include all other ES2017 features in the "jail".

[erights]

Adding @brabalan, @edgemaster , @jpolitz, @blerner, @rossberg, @dherman, @shriram, @philippagardner, @sergiomaffeis, @totherme, @sophiaIC, @tobycmurray, @doerrie, @ankurtaly, @dominiquedevriese, @kjx, @charguer, @tvcutsem

There are several high quality formalizations of ES5, notably ENCAP, S5, JSCert, and one I am not remembering at the moment. I don't know how far any such effort has gotten formalizing later versions of EcmaScript. All of the mechanisms in Draft Proposed Standard SES apply to ES5 in exactly the same way they apply to later versions, so this should be a good place to start. ENCAP and S5 have already been used to reason about previous versions of SES or subsets of SES. Formalists (you know who you are), does this sound like an interesting challenge to take on?

Of course, a proof that security holds in SES as applied to ES5 does not imply that it still holds as applied to later versions. Can you think of anything that ES2015, ES2016, or the March 17 draft of ES2017 adds or changes to ES5 that might invalidate an ES5 proof?

In other words, if we did become confident that SES on ES5 successfully confines, what should we worry about first regarding later editions?

[IgnoredAmbience]

http://github.com/jscert/jscert remains at ES5 for now with weak plans to extend to ES2015. The Imperial College research focus is currently full formal verification and symbolic execution for JavaScript programs.
I will review this SES proposal in a bit more detail on Monday and have a think.

[erights]

Please let me know if you spot anything in the SES proposal that is sensitive to any of the differences between ES5 and later. Thanks.

[benjamingr]

@erights Well, as you know a lot of things have changed that are potentially problematic between ES versions - namely you'll need to address things like proxies, cross-realm symbols, module bindings pass-by-binding and so on.

I was under the impression that you personally made sure that every feature is completely SES compatible in that SES has a clear way of dealing with it by either forbidding it or keeping it confined. (At least I recall at least half a dozen discussions on ESDiscuss regarding it).

For some features you can show a direct desugaring to ES5 or the formal constructs you used in the SES proof. For others it'll be more work.

In either case - in my opinion the beauty of SES is in its formal analysis and proof. I don't think a proposal would pass if it forbids any use of post ES5 features.

(I realize I'm telling you thinks you already know - I just want it to be obvious for all readers in this thread)

[erights]

@benjamingr

I was under the impression that you personally made sure that every feature is completely SES compatible

Yes. That is why I was having a hard time spotting what we should still worry about. Your answer helps separate issues, and does point out the one interesting remaining area where we need to reason more carefully about possible loss of confinement.

Separating issues:

On

• the design of proxies,
• the huge controversy and eventual death of private symbols,
• the constraints around the design of private state,
• the subtle issues around the reflective invariants (e.g., can't claim a property is data-nonwritable-nonconfigurable and then report different values over time),

these are about (not respectively)

• defending integrity,
• avoiding various confusion attacks,
• not compromising encapsulation,
• supporting defensive consistency.

All crucial(!) but distinct from confinement. To know that SES has the security properties it claims, we should work towards proof of all these as well, which will be more subtle and absolutely will hinge on differences between ES5 and later. (Please file bugs on the needs for proofs of these as you see fit!)

The module system has complex interactions with the overall goal of SES. Since we do not yet have any standard builtin modules, I think we can see simply the absence of any threat to confinement. The fact that all state in the module system, including mutable state at the top level of loaded modules, is per loader, and there are no cross-realm loaders (or indeed, not yet any loaders at all), there is no threat to confinement lurking there.

The issue that I missed:

The one new issue where new reasoning is needed to show that confinement is upheld is the cross-realm symbol registry. I need to add a new section showing why this does not violate confinement because it does not clearly follow from the rest of the document. Any proof will likely need to reason carefully and separately about it as well.

Thanks!

[brabalan]

Two quick comments:

• there is now a link between S5 and JSCert (https://github.com/tilk/LambdaCert);
• we're prototyping an idea to streamline exchanges between formalists and specifiers, I may have something to show at the May TC39 meeting.

[erights]

Hi @brabalan that would be great. Looking forward to seeing that in May.

I would like to get your impressions of SES and how well your current formal machinery could support a proof, first, of confinement. Thanks.

[erights]

In addition to the Symbol registry issue I missed, we now potentially have a much bigger challenge.

If @dtribble, @mhevery, and I are right about Zones at https://esdiscuss.org/topic/fwd-are-zones-global-state-do-they-provide-a-dangerous-communications-channel , extending any proof of SES confinement to cover them will require very different reasoning. In particular, I suspect we'll need a much more subtle definition of confinement so that it still prohibits what we wish to prohibit while allowing what we explain here.

[erights]

@brabalan, @edgemaster, @philippagardner, @sergiomaffeis, @totherme, @charguer

At https://verificationinstitute.org/event/verified-trustworthy-software-systems-specialist-meeting/ I asked @charguer about this and received an alarming answer. (@charguer, please correct if I am not summarizing correctly):

All security is about what cannot happen. From a partial specification, we can prove that certain things can or will happen. But to prove that something cannot happen, we need to do an induction over the entire spec. Until all the details of the language are specified, we will be unable to prove that anything cannot happen.
[not quoting anything. Just my summary]

This is exactly backwards. First, if true, it means that this spec process, and any spec process like it, is useless for security because we will never finish capturing every last detail of the spec -- Date, internationalization, RegExp, unicode. None of the details of these are relevant to security. All that matters for any of these is that they do not violate the basic invariants of JavaScript's object-oriented programming model. The problem is not that the spec is unfinished. It is that these basic invariants are not written down. @allenwb has repeatedly asked for guidance in stating general invariants that the spec should not violate. I was hoping this would be a result of this formalization work.

It is exactly backwards in that it treats TC39 as a black box, producing a stream of detail, whatever it is, for specifiers to consume without influencing. If some detail of Internationalization accidentally introduces a hole making security impossible, the right response is to fix that bug in internationalization. However, the suggested approach would be to just proceed to formalize it, and not even notice that this bug had made security impossible until years later, when the formalization of some then-stale version of ES is complete and the proof of what cannot happen fails.

At this workshop I saw a preview of the tools you folks are producing to help the committee, that you will be demonstrating and talking about in May. Very impressive! I think these will be a great aid to us and I really appreciate the effort! However, regarding proofs of what cannot happen, they are again exactly backwards. They merely provide us tools to write more detailed specifications, not to express general invariants that should hold across the spec, or to show that the current partial spec does not violate them.

Instead, this issue is a perfect opportunity for this formal methods work to affect what we actually do, in a way much more interesting than just giving us a more precise language to express endless details. From just a partial formalization of ES5/strict, we should be able to derive candidate general invariants that characterize the "laws" of the JS object model. We can then check

• which of these invariants are accidental regularities vs unstated but intended regularities, articulating our currently inarticulate intentions. This would be checked by human judgement of the participants.
• which of these invariants are or are not broken by remaining spec text. This would be a continual process as new spec text is written. When there is a conflict, humans need to judge whether the flaw is in the new spec text or in the statement of the invariants.

The invariants that survive this process should then be proposed for inclusion as normative in the spec itself -- both prose and as formalized. IIUC the whole point of using formal methods for these activities, once these invariants are explicitly formalized, then the formalization of any detail that accidentally breaks these invariants will be immediately caught as introducing an inconsistency into the spec.

Is this all plausible? At the May meeting, all the machinery you folks are creating for formally expressing detail is great. But it would be much more productive for you to help us understand what invariants we are inarticulately preserving, or only accidentally violating, and to help us state these explicitly.You could then present the formal tools as a way to catch these accidental violations early -- both the accidental violations already in there as well as future ones. Thanks.

[erights]

Let's start with the four invariants on slide 19 of https://github.com/FUDCo/frozen-realms/blob/master/frozen-realms-draft.pdf that I state JS already obeys:

• Memory Safety
• Encapsulation
• Defensible Objects
• Effects only by held references

How can we state these so that we can check whether anything in the partial formalization that we have violates them?

[sophiaIC]

Mark,

I cannot find slide numbers, so it is not obvious to me what slide 19 is.

Sophia

On 8 Apr 2016, at 08:12, Mark S. Miller <[email protected]mailto:[email protected]> wrote:

Let's start with the four invariants on slide 19 of https://github.com/FUDCo/frozen-realms/blob/master/frozen-realms-draft.pdf that I state JS already obeys:

• Memory Safety
• Encapsulation
• Defensible Objects
• Effects only by held references

How can we state these so that we can check whether anything in the partial formalization that we have violates them?

—
You are receiving this because you were mentioned.
Reply to this email directly or view it on GitHubhttps://github.com//issues/4#issuecomment-207264135

[erights]

Slide title: "Modern JavaScript? (2009-present)"

[sophiaIC]

Yes, I see. I thought it could be easy for you to add the slide numbers anyway.

Sophia

On 8 Apr 2016, at 08:18, Mark S. Miller <[email protected]mailto:[email protected]> wrote:

Slide title: "Modern JavaScript? (2009-present)"

—
You are receiving this because you were mentioned.
Reply to this email directly or view it on GitHubhttps://github.com//issues/4#issuecomment-207267155

[sergiomaffeis]

a comment on the "alarming answer" post above.

you can find a different approach to security proof in my Defensive JavaScript. the idea there is to identify some strong invariant (based on common behaviour of ES3, ES5 and hopefully future versions on JS) and show that the security property (there defensiveness) follows from this invariant. that gives us some level of confidence that the security property holds as proven both in the version of JS we are looking at and in past and future versions too, without formalizing Date or RegExp but just assuming they don't break our "reasonable" invariant.

[dominiquedevriese]

If I can just make a few comments as an outsider:

• The quote of @charguer is maybe a bit unnuanced. It's obviously true that for any formalisation of security, you somehow need to prove that it is not broken by any of the builtin objects that are made available and that can only be done if you have sufficient information about their behavior. However, there are many cases where a partial spec for their behavior can be sufficient to decide this. For example, if you know that Regexp.test() always returns a primitive boolean and only depends on the native string it receives and its own definition, then that should be sufficient to prove security, irrespective of how the boolean is actually computed.
• Perhaps it's also worth pointing out (maybe this is obvious, but still) is that an easy way to prove that the spec of something like Regexp does not break security of the language is to use a model implementation inside the language (not sure if that's realistic). This will obviously only work for features that are actually implementable inside the language, so not things like reflection etc., but maybe viable for things like Regexp and so on?
• Finally, formalising the notions of Memory Safety, Encapsulation and "Effects only by held references" is precisely the topic of a recent paper by Lars Birkedal, Frank Piessens and myself (https://lirias.kuleuven.be/handle/123456789/529252). Unfortunately, we only cover a subset of LambdaJS, and the formalisation is currently mathematically non-trivial and hard to use. However, we are thinking about ways to fix those problems, although I'm not sure we will dare to make the move to full JavaScript...

[erights]

On Apr 8, 2016 8:57 AM, "Dominique Devriese" [email protected]
wrote:

The quote of @charguer is maybe a bit unnuanced.

Not a quote. My paraphrase. Any lack of nuance I am sure is mine.

[charguer]

@erights, all,

I discussed with Alan and here are a few answers/comments.

*) I did tell you that, to establish a security theorem, you need to
formalize all the "features" of the language. As Dominique
pointed out, for many libraries, which are written in pure JS
(or at least are morally equivalent to pure JS code), we don't need
to formalize them, because such libraries don't introduce additional
"language features" which might give rise to security breaches.
However, any library that has an internal state (e.g. Date, Random,
and I suppose many interactions with the DOM, etc..) can be potential
sources of trouble. Indeed, as soon as a stateful module might get
called both by trusted code and untrusted code, you may have
an information channel that might be exploited.

*) We agree that it is somewhat unrealistic to expect all language
features to be formalized before starting to work on the proof
of security theorems. Like you said, we should attempt to work out
and to formally state in Coq the invariants that are required for
proving the theorems of interest. Then, we could advertise these
invariants (translated in English prose) to the developers of the
various language features, in the hope that those developers can
confirm that their features indeed satisfy the invariants---or
at least that they intend to.

*) Regarding the statement of the invariants, we should work on them
together. In particular, Alan and I came up with some ideas for
specifying what a proxy should guarantee. We should discuss that
with you, probably offline (we expect a certain number of iterations
may be needed to converge to something that makes enough sense).
In general, to formally express particular invariants, it is required
to augment the semantics with so-called "ghost" information, used
for keeping track, e.g., of the set of pointers that have been
leaked on purpose.

*) In parallel, we believe it would still be worthwhile extending our
reference interpreter from ES5 to a large subset of ES6. However,
we simply don't have the manpower to do this work ourselves.
Nevertheless, we would be happy to help whenever a difficulty is
encountered. Note that our interpreter is currently written in a
tiny subset of the OCaml language. Overall, we believe it should
not be hard for a programmer with no experience in OCaml to extend
our interpreter.

---Remark: our interpreter used to be written in Coq and extracted
to OCaml but we cound it simpler to write OCaml directly; we are
looking forward to generate Coq definitions from OCaml code in the
future. We were even tempted to consider writing the interpreter
a tiny subset of JS, but we found that OCaml provides a far more
concise syntax, moreover it provides handy type-checking of the code.
In addition, that our OCaml interpreter gets translated to readable
and executable JS code.)

(Alan will present the interpreter and give a demo in May.)

Best,
Arthur

[erights]

Hi @charguer , thanks for the detailed response. It would be wonderful to have draft formal and informal statements of these invariants. Anything you can post about these? With such invariants in hand, how would we go about proving security properties of frozen realms?

I look forward to discussing these issues and seeing you demo in May!

[erights]

In case it helps, the presentation you saw is at https://youtu.be/jE0DY5pS-xY?t=6h39m59s with the slides at https://github.com/FUDCo/proposal-frozen-realms/raw/master/frozen-realms-draft.key , https://github.com/FUDCo/proposal-frozen-realms/blob/master/frozen-realms-draft.pdf . I mention this one because this presentation was constructed for this audience -- to suggest what formal properties would be relevant.

[dckc]

FWIW, my favorite formalism of capability security of js is:

D. Devriese, Birkedal, and Piessens
Reasoning about Object Capabilities with Logical Relations and Effect Parametricity
1st IEEE European Symposium on Security and Privacy, Congress Center Saar, Saarbrücken, GERMANY, 2016.

The paper is available at:
https://lirias.kuleuven.be/bitstream/123456789/529252/1/paper-preprint.pdf
The presentation Devriese gave about the work Mar 2016 at the IEEE
EuroS&P conference is available too:
https://people.cs.kuleuven.be/dominique.devriese/obj-cap-log-rel-eff-param.pdf
Technical details and proofs are available in an associated technical report:
https://lirias.kuleuven.be/bitstream/123456789/524074/1/CW690.pdf

It directly discusses λ JS , but Brown PLT work suggests this extends to the rest of JS, at least as of 2011.

Unlike jscert, the proofs by Devriese are not formalized, unfortunately.

[dominiquedevriese]

I happen to be subscribed to this issue and am happy to see my work mentioned :)

I just thought I should mention another more recent formulation of capability-safety for a JavaScript-like calculus, that uses a similar approach as my EuroS&P16 proposal: Swasey et al.'s OCPL https://people.mpi-sws.org/~swasey/papers/ocpl/ocpl-oopsla17-long.pdf
Like my EuroS&P16 paper, they also formulate capability safety as a semantic property, a form of parametricity defined using a logical relation, that can be directly used for reasoning about programs.
On the negative side, they drop effect parametricity (which I needed to prove previous syntactic formulations of capability safety and for reasoning about effects).
However, on the (very) positive side, their logic is mechanized and makes use of nice Iris program logic machinery which removes a lot of tedious step-indexing accounting in the proof.

If someone would like to prove a form of capability safety for JavaScript + frozen realms (IIUC), I would recommend starting from such an approach...
I think it should definitely be possible to use Iris for reasoning about programs in the JSCert operational semantics and build a logical relation-style formulation of the capability safety you get with frozen realms (haven't been following the details though).

[sophiaIC]

Hi Dominique, This feels like the middle of some discussion. What is it about? Yes, I know the work by David Swasey. Here is our work, as would have also appeared at FASE. https://arxiv.org/abs/2002.08334 We now have some Coq proofs. Copying my co-authors into this. Best wishes, Sophia

…

--- Sophia Drossopoulou https://wp.doc.ic.ac.uk/sd/ From: Dominique Devriese <[email protected]> Reply to: tc39/proposal-ses <[email protected]> Date: Wednesday, 3 June 2020 at 22:11 To: tc39/proposal-ses <[email protected]> Cc: Sophia Drossopoulou <[email protected]>, Mention <[email protected]> Subject: Re: [tc39/proposal-ses] Proof of security (#4) This email from [email protected] originates from outside Imperial. Do not click on links and attachments unless you recognise the sender. If you trust the sender, add them to your safe senders list<https://spam.ic.ac.uk/SpamConsole/Senders.aspx> to disable email stamping for this address. I happen to be subscribed to this issue and am happy to see my work mentioned :) I just thought I should mention another more recent formulation of capability-safety for a JavaScript-like calculus, that uses a similar approach as my EuroS&P16 proposal: Swasey et al.'s OCPL https://people.mpi-sws.org/~swasey/papers/ocpl/ocpl-oopsla17-long.pdf Like my EuroS&P16 paper, they also formulate capability safety as a semantic property, a form of parametricity defined using a logical relation, that can be directly used for reasoning about programs. On the negative side, they drop effect parametricity (which I needed to prove previous syntactic formulations of capability safety and for reasoning about effects). However, on the (very) positive side, their logic is mechanized and makes use of nice Iris program logic machinery which removes a lot of tedious step-indexing accounting in the proof. If someone would like to prove a form of capability safety for JavaScript + frozen realms (IIUC), I would recommend starting from such an approach... I think it should definitely be possible to use Iris for reasoning about programs in the JSCert operational semantics and build a logical relation-style formulation of the capability safety you get with frozen realms (haven't been following the details though). — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub<#4 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/ABULC4JV3W6J7HO3KB3IXRTRU236RANCNFSM4B6R6DVQ>.

[dominiquedevriese]

Sophia, Op do 4 jun. 2020 om 01:03 schreef Sophia Drossopoulou < [email protected]>:

This feels like the middle of some discussion. What is it about? Yes, I know the work by David Swasey.

AFAIU, this is an old ticket about proving security of a subset of javascript with frozen realms which I was subscribed to for some reason. I replied to Dan Connolly's message about my work, to point out Swasey et al.'s paper which is related but has been mechanized.

Here is our work, as would have also appeared at FASE. https://arxiv.org/abs/2002.08334 We now have some Coq proofs.

Ah great, I hadn't seen this yet. I think I've seen earlier versions of this work and even briefly discussed it with Mark Miller over email. I'm looking forward to reading this new version, but I'm a bit buried with POPL submissions for the moment... See you, Dominique Copying my co-authors into this.

[shriram]

Hi Sophia: FYI, this is a public Twitter thread you're responding to. It's this one:

#4