AJACS

ANR.png
ANR-14-CE28-0008

body

AJACS Papers & Software

Previous Papers

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]

Journal Papers

  • 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]

Conference Papers

  • 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, Tamara Rezk. In Proceedings of the WWW'17. [pdf]
  • Type Abstraction for Relaxed Noninterference, Raimil Cruz, Tamara Rezk, Bernard Serpette, É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]

Workshop papers

  • 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]

Software