Correct and Secure Web Programming using Dependent Types and Embedded
Simon Fowler, Edwin C. Brady · 2013
Dependently-typed languages allow very expressive types to be used during development, in turn facilitating easier reasoning about the operation of programs written in such languages. Stronger type specifications do however bring with them the disadvantage that it becomes increasingly difficult to write programs that are accepted by the type checker and additional proofs may have to be specified by a user. Embedded domain-specific languages (EDSLs) address this problem by introducing a layer of abstraction over more specific underlying types, allowing domain-specific code to be written in high-level languages which use dependent types to enforce certain invariants without additional proof obligations. In this paper, we apply this technique to web programming, and introduce an EDSL to facilitate the creation and handling of web forms which retain type information, reducing the scope for programmer error and attacks such as SQL injection. We also show how to enforce resource usage protocols associated with common web operations such as CGI, database access and session handling.