Formal methods for web security

DOI10.1016/j.jlamp.2016.08.006zbMath1359.68021DBLPjournals/jlp/BugliesiCF17OpenAlexW2514023902WikidataQ62045656 ScholiaQ62045656MaRDI QIDQ511944

Stefano Calzavara, Riccardo Focardi, Michele Bugliesi

Publication date: 22 February 2017

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2016.08.006

zbMATH Keywords

surveyformal methodsweb security

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02) Internet topics (68M11)

Uses Software

• ProVerif
• JavaScript
• TS#
• Python
• Ur/Web
• KJS
• F*
• JSLINQ
• SeLINQ
• Links
• K Prover

Cites Work

• An overview of the K semantic framework
• Conditional rewriting logic as a unified model of concurrency
• Survey on JavaScript security policies and their enforcement mechanisms in a web browser
• Fine-Grained Detection of Privilege Escalation Attacks on Browser Extensions
• SeLINQ
• Fully abstract compilation to JavaScript
• Defining code-injection attacks
• Tracking Information Flow in Dynamic Tree Structures
• JavaScript instrumentation for browser security
• Mobile values, new names, and secure communication
• Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif
• The essence of command injection attacks in web applications
• Secure distributed programming with value-dependent types
• A trusted mechanised JavaScript specification
• Gradual typing embedded securely in JavaScript

This page was built for publication: Formal methods for web security