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]

Workshop papers

  • ProScript-TLS: Verifiable Models and Systematic Testing for TLS 1.3, Nadim Kobeissi, and Karthikeyan Bhargavan. In Proceedings of TRON'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]