3 ms·

JSCert: Certified JavaScript

88 points by lelf 11y ago

inglor 11y ago
You can't talk about JavaScript formal analysis for security without mentioning Mark Miller's amazing work here: http://www-cs-students.stanford.edu/~ataly/Papers/sp11.pdf http://www-cs-students.stanford.edu/~ataly/Papers/sp11.pdf Here, not only does he built a secure subset of JavaScript and _prove_ it's tamper safe using formal logic, Mark also finds exploits with the same method in high end tamper filters like Yahoo's. Definitely impressive use of formal logic in language analysis.
- nickpsecurity 11y ago
  Nice paper. Thanks for it.
inglor 11y ago
It's probably a good idea to link to the presentation directly as it explains the point and methodology more clearly IMO: http://jscert.org/popl14/?full#1 http://jscert.org/popl14/?full#1
nickpsecurity 11y ago
Excellent work as usual in practical, formal methods by INRIA. Much of the formal work in academia amount to just screwing around or redoing the same stuff. INRIA is awesome because their work is often useful to the rest of us: robust languages, compilers, parsers, protocols, static analysis tools, WCET estimation, easier-to-use provers... list goes on. INRIA and especially Xavier Leroy's people rock! That simple. :)
MichaelCrawford 11y ago
I applaud every effort to improve Javascript as it all takes eons to download over my dialup but commonly does not actually work. A favorite contribution is called something like "You Don't Really Need jQuery". I will dig it up,in a little bit. Of most serious concern is how to convince the working JS coder to actually avail themselves of better javascript? Most dont read HN. I find it is of no use to point out the errors of their ways.
- CHY872 11y ago
  This isn't for that. This work is to create a formal model of Javascript - a definition of what a perfect Javascript runtime should do. The next step (potentially) is then that you can reason about Javascript programs in a useful manner - you could prove that your security-critical script does the right thing, for example. Generally, such work does not lead to many updates to the state of the art - but is useful in its own way.
  - MichaelCrawford 11y ago
    "I'm not really bad; I'm just drawn that way." -- Jessica Rabbit I see your point, but my concern that the coder who implements a security-critical script doesn't know he should use tools like this one. Lots of those who use other languages like to gripe about the many faults of PHP. While I agree that PHP has its problems I've used lots of languages that were far, far worse. My take is not that PHP is a bad language but that those who use it are often bad programmers. Take Bill at http://www.radioparadise.com/ http://www.radioparadise.com/ He at first built the sight with phpNuke, but rewrote it from scratch in the best of just a few days after "some boys from Brazil" overran it. Radio Paradise is still built on PHP, the difference is that Bill is an excellent engineer.
    - CHY872 11y ago
      They shouldn't use tools like this one, though. This is purely a research project and not industrially usable. In any case, the purpose is to specify what Javascript is supposed to do, and not what Javascript engines actually do. The interpreter was as easily as not an afternoon project; they probably got one for free. There's been some interesting discussion about this for the C language - useful yet undefined behaviours that are relied upon by many pieces of software, where a formal semantics such as this project may fall flat and lead to being overly restrictive. https://www.cl.cam.ac.uk/~pes20/cerberus/notes50-2015-05-24-survey-discussion.html https://www.cl.cam.ac.uk/~pes20/cerberus/notes50-2015-05-24-...
      - MichaelCrawford 11y ago

88 points by lelf 11y ago

You can't talk about JavaScript formal analysis for security without mentioning Mark Miller's amazing work here: http://www-cs-students.stanford.edu/~ataly/Papers/sp11.pdf http://www-cs-students.stanford.edu/~ataly/Papers/sp11.pdf Here, not only does he built a secure subset of JavaScript and _prove_ it's tamper safe using formal logic, Mark also finds exploits with the same method in high end tamper filters like Yahoo's. Definitely impressive use of formal logic in language analysis.

nickpsecurity 11y ago
Nice paper. Thanks for it.

inglor 11y ago

It's probably a good idea to link to the presentation directly as it explains the point and methodology more clearly IMO: http://jscert.org/popl14/?full#1 http://jscert.org/popl14/?full#1

nickpsecurity 11y ago

Excellent work as usual in practical, formal methods by INRIA. Much of the formal work in academia amount to just screwing around or redoing the same stuff. INRIA is awesome because their work is often useful to the rest of us: robust languages, compilers, parsers, protocols, static analysis tools, WCET estimation, easier-to-use provers... list goes on. INRIA and especially Xavier Leroy's people rock! That simple. :)

MichaelCrawford 11y ago

I applaud every effort to improve Javascript as it all takes eons to download over my dialup but commonly does not actually work. A favorite contribution is called something like "You Don't Really Need jQuery". I will dig it up,in a little bit. Of most serious concern is how to convince the working JS coder to actually avail themselves of better javascript? Most dont read HN. I find it is of no use to point out the errors of their ways.

CHY872 11y ago
This isn't for that. This work is to create a formal model of Javascript - a definition of what a perfect Javascript runtime should do. The next step (potentially) is then that you can reason about Javascript programs in a useful manner - you could prove that your security-critical script does the right thing, for example. Generally, such work does not lead to many updates to the state of the art - but is useful in its own way.
- MichaelCrawford 11y ago
  "I'm not really bad; I'm just drawn that way." -- Jessica Rabbit I see your point, but my concern that the coder who implements a security-critical script doesn't know he should use tools like this one. Lots of those who use other languages like to gripe about the many faults of PHP. While I agree that PHP has its problems I've used lots of languages that were far, far worse. My take is not that PHP is a bad language but that those who use it are often bad programmers. Take Bill at http://www.radioparadise.com/ http://www.radioparadise.com/ He at first built the sight with phpNuke, but rewrote it from scratch in the best of just a few days after "some boys from Brazil" overran it. Radio Paradise is still built on PHP, the difference is that Bill is an excellent engineer.
  - CHY872 11y ago
    They shouldn't use tools like this one, though. This is purely a research project and not industrially usable. In any case, the purpose is to specify what Javascript is supposed to do, and not what Javascript engines actually do. The interpreter was as easily as not an afternoon project; they probably got one for free. There's been some interesting discussion about this for the C language - useful yet undefined behaviours that are relied upon by many pieces of software, where a formal semantics such as this project may fall flat and lead to being overly restrictive. https://www.cl.cam.ac.uk/~pes20/cerberus/notes50-2015-05-24-survey-discussion.html https://www.cl.cam.ac.uk/~pes20/cerberus/notes50-2015-05-24-...
    - MichaelCrawford 11y ago