Formal methods for web security

DOI10.1016/J.JLAMP.2016.08.006MaRDI QIDQ511944zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Michele Bugliesi, Stefano Calzavara, Riccardo Focardi

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)

Recommendations

• Survey on JavaScript security policies and their enforcement mechanisms in a web browser
• scientific article; zbMATH DE number 1746450
• scientific article; zbMATH DE number 1024091
• A Universally Composable Framework for the Analysis of Browser-Based Security Protocols
• IT Security Analysis Best Practices and Formal Approaches

Cites work

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

Cited in

(4)

• Survey on JavaScript security policies and their enforcement mechanisms in a web browser
• Web source code post-processing: a new approach based on classic models and methods
• IT Security Analysis Best Practices and Formal Approaches
• Gray-box runtime enforcement of hyperproperties

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q511944)