AJACS

The following papers are not the result of the Ajacs project, but they are foundations on which Ajacs is built.

• Pretty-Big-Step Semantics, Arthur Charguéraud. In Proceedings of ESOP'13. [hal]
• A Trusted Mechanised JavaScript Specification, Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt, and Gareth Smith. In Proceedings of the POPL'14. [hal]

• Mashic Compiler: Mashup Sandboxing using Inter-frame Communication, Zhengqin Luo, Jose Fragoso Santos, Ana Almeida Matos, and Tamara Rezk. In Journal of Computer Security, 2014. [pdf]
• Using JavaScript Monitoring to Prevent Device Fingerprinting, Frédéric Besson, Nataliia Bielova, Thomas Jensen. In ERCIM News, Special theme: Cybersecurity, July 2016. [web]
• Skeletal Semantics and their Interpretations, Martin Bodin, Philippa Gardner, Thomas Jensen, and Alan Schmitt. In Proceedings of the ACM on Programming Languages, January 2019. [hal]

• Certified Abstract Interpretation with Pretty-Big-Step Semantics, Martin Bodin, Thomas Jensen, Alan Schmitt. In Proceedings of CPP'15. [hal]
• BrowserAudit: Automated Testing of Browser Security Features, Charlie Hothersall-Thomas, Sergio Maffeis, Chris Novakovic. In Proceedings of ISSTA'15. [pdf, web]
• A Trusted Mechanised Specification of JavaScript: One Year On Philippa Gardner, Gareth Smith, Conrad Watt, Thomas Wood. In Proceedings of CAV'15 (invited talk). [pdf]
• Hybrid Typing of Secure Information Flow in a JavaScript-like Language, José Fragoso Santos, Thomas Jensen, Tamara Rezk, Alan Schmitt. In Proceedings of TGC'15. [hal]
• Modular Monitor Extensions for Information Flow Security in JavaScript, José Fragoso Santos, Tamara Rezk, Ana Almeida Matos. In Proceedings of TGC'15. [hal]
• A Taxonomy of Information Flow Monitors, Nataliia Bielova, Tamara Rezk. In Proceedings of POST'16. [pdf]
• On access control, capabilities, their equivalence, and confused deputy attacks, Vineet Rajani, Deepak Garg, and Tamara Rezk. In Proceedings of CSF'16. [pdf]
• Hybrid Monitoring of Attacker Knowledge, Frédéric Besson, Nataliia Bielova, Thomas Jensen. In Proceedings of CSF'16. [pdf]
• Spot the Difference: Secure Multi-Execution and Multiple Facets, Nataliia Bielova, Tamara Rezk. In Proceedings of ESORICS'16. [pdf]
• DOM: Specification and Client Reasoning, Azalea Raad, José Fragoso Santos, Philippa Gardner. In Proceedings of APLAS'16. [pdf]
• Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate, Karthikeyan Bhargavan, Bruno Blanchet, Nadim Kobeissi. In Proceedings of S&P'17. [pdf]
• Formal Modeling and Verification for Domain Validation and ACME, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Nadim Kobeissi. In Proceedings of FC'17. [hal]
• Automated Verification for Secure Messaging Protocols and their Implementations: A Symbolic and Computational Approach, Nadim Kobeissi, Karthikeyan Bhargavan, Bruno Blanchet. In Proceedings of EuroS&P'17. [pdf]
• On the Content Security Policy Violations Due to the Same-Origin Policy, Dolière Francis Somé, Nataliia Bielova, and Tamara Rezk. In Proceedings of the WWW'17. [pdf]
• Type Abstraction for Relaxed Noninterference, Raimil Cruz, Tamara Rezk, Bernard Serpette, and Éric Tanter. In Proceedings of ECOOP'17. [pdf]
• Control What You Include ! Server-Side Protection against Third Party Web Tracking, Dolière Francis Somé, Nataliia Bielova, and Tamara Rezk. In Proceedings of ESSoS'17. [arxiv]
• JSExplain: A Double Debugger for JavaScript, Arthur Charguéraud, Alan Schmitt, and Thomas Wood. In Proceedings of Web Programming, The Web Conference 2018. [hal]
• A Better Facet of Dynamic Information Flow Control, Minh Ngo, Nataliia Bielova, Cormac Flanagan, Tamara Rezk, Alejandro Russo, and Thomas Schmitz. In Proceedings of WPDAI 2018, The Web Conference 2018. [pdf]

• ProScript-TLS: Verifiable Models and Systematic Testing for TLS 1.3, Nadim Kobeissi, Karthikeyan Bhargavan. In Proceedings of TRON'15. [pdf]
• FLEXTLS: A Tool for Testing TLS Implementations, Benjamin Beurdouche, Antoine Delignat-Lavaud, Nadim Kobeissi, Alfredo Pironti, Karthikeyan Bhargavan. In Proceedings of WOOT'15. [pdf]
• An Abstract Separation Logic for Interlinked Extensible Records, Martin Bodin, Thomas Jensen, Alan Schmitt. In Proceedings of JFLA'16. [hal]
• Certified Desugaring of Javascript Programs using Coq, Marek Materzok. In Proceedings of CoqPL'16. [pdf]
• Dynamic leakage - a need for a new quantitative information flow measure, Nataliia Bielova. In Proceedings of PLAS'16. [pdf]
• Formal Verification of Smart Contracts, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy, Santiago Zanella-Béguelin. In Proceedings of PLAS'16. [pdf]
• Non-Interference through Annotated Multisemantics, Gurvan Cabon and Alan Schmitt. In Proceedings of JFLA'17. [hal]
• Annotated multisemantics to prove Non-Interference analyses, Gurvan Cabon, Alan Schmitt. In Proceedings of PLAS'17. [hal]
• To Extend or not to Extend: on the Uniqueness of Browser Extensions and Web Logins, Gábor György Gulyás, Dolière Francis Somé, Nataliia Bielova, Claude Castelluccia. In Proceedings of WPES'18. [pdf]

• https://github.com/jscert/jscert: a Coq formalization of ECMAScript 5 (JavaScript)
• http://crypto.cat: chat with your friends, securely
• https://webstats.inria.fr: statistics about JavaScript Libraries and Constructs, Use of Content Security Policy, HTTPOnly and Secure Cookies, and much more
• https://github.com/jscert/jsexplain: an interactive debugger for the JavaScript specification
• https://extensions.inrialpes.fr: behavioral fingerprinting via browser Extensions and login-leaks
• http://www-sop.inria.fr/members/Doliere.Some/essos/: an automatic rewriting tool for web application developers that eliminates tracking from third-party content.