Command injection attacks, continuations, and the Lambek calculus

Hayo Thielecke
(Computer Science, University of Birmingham)

This paper shows connections between command injection attacks, continuations, and the Lambek calculus: certain command injections, such as the tautology attack on SQL, are shown to be a form of control effect that can be typed using the Lambek calculus, generalizing the double-negation typing of continuations. Lambek's syntactic calculus is a logic with two implicational connectives taking their arguments from the left and right, respectively. These connectives describe how strings interact with their left and right contexts when building up syntactic structures. The calculus is a form of propositional logic without structural rules, and so a forerunner of substructural logics like Linear Logic and Separation Logic.

In Olivier Danvy and Ugo de'Liguoro: Proceedings of the Workshop on Continuations (WoC 2015), London, UK, April 12th 2015, Electronic Proceedings in Theoretical Computer Science 212, pp. 81–96.
Published: 19th June 2016.

ArXived at: http://dx.doi.org/10.4204/EPTCS.212.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org