Jessie static analysis; e.g. Zoe offer safety

[dckc]

met McCarthy at SFBW '19. He was chatting up MarkM about Jessie. He has done a bunch of work with ACL2. It looked fun and easy to do Jessie in ACL2 and prove properties such as offer safety of Zoe.

[dckc]

I have started on an ocaml implementation instead because

• ocaml dev is fun (ref spotter)
• ACL2 doesn't take advantage of the proofs-as-types Curry-Howard correspondence
• an ocaml prototype is in the direction of a coq formalism. Lots of people, including MarkM, seem to appreciate coq
  • as much as I kinda prefer idris, coq is more mature

https://github.com/dckc/TinySES/tree/ml/ml

For successively elaborate test cases, an online JS book such as https://eloquentjavascript.net/01_values.html might be a good source.

I considered using a profile of https://github.com/facebook/flow/tree/master/src/parser . It has some good inspriation, but it would hardly demonstrate the hypothesis that Jessie is easy to implement. It has some good inspiration, though.

https://github.com/prakhar1989/ocaml-js/blob/master/src/lexer.mll looks handy

road not taken: https://github.com/inhabitedtype/angstrom (no line numbers)

[dckc]

darn; just when I thought I was ready to put this away

Discovering Concrete Attacks on Website Authorization by Formal Analysis, C. Bansal, K. Bhargavan & S. Maffeis. CSF 2012 (Read more) Social sign-on and social sharing are becoming an ever more popular feature of web applications. This success is largely due to the APIs and support offered by prominent social networks, such as Facebook, Twitter, and Google, on the basis of new open standards such as the OAuth 2.0 authorization protocol. A formal analysis of these protocols must account for malicious websites and common web application vulnerabilities, such as cross-site request forgery and open redirectors. We model several configurations of the OAuth 2.0 protocol in the applied pi-calculus and verify them using ProVerif. Our models rely on WebSpi, a new library for modeling web applications and web-based attackers that is designed to help discover concrete website attacks. Our approach is validated by finding dozens of previously unknown vulnerabilities in popular websites such as Yahoo and WordPress, when they connect to social networks such as Twitter and Facebook. -- https://prosecco.gforge.inria.fr/webspi/ https://github.com/Inria-Prosecco/proscript-messaging ocaml code https://github.com/Inria-Prosecco/proscript-messaging/blob/master/EuroSP.pdf https://github.com/Inria-Prosecco/proscript-messaging/blob/master/ps2pv/parser.mly