research-article

Dependent Types for Safe and Secure Web Programming

Authors:

Edwin BradyAuthors Info & Claims

IFL '13: Proceedings of the 25th symposium on Implementation and Application of Functional Languages

Pages 49 - 60

https://doi.org/10.1145/2620678.2620683

Published: 28 August 2013 Publication History

Abstract

Dependently-typed languages allow precise types to be used during development, facilitating static reasoning about program behaviour. However, with the use of more specific types comes the disadvantage that it becomes increasingly difficult to write programs that are accepted by a type checker, meaning additional proofs may have to be specified manually.

Embedded domain-specific languages (EDSLs) can help address this problem by introducing a layer of abstraction over more precise underlying types, allowing domain-specific code to be written in a verified high-level language without imposing additional proof obligations on an application developer.

In this paper, we apply this technique to web programming. Using the dependently typed programming language Idris, we show how to use EDSLs to enforce resource usage protocols associated with common web operations such as CGI, database access and session handling. We also introduce an EDSL which uses dependent types to facilitate the creation and handling of web forms, reducing the scope for programmer error and possible security implications.

References

[1]

Heiko Böck. Java Persistence API. In The Definitive Guide to NetBeans Platform 7, pages 315--320. Springer, 2011.

[2]

Edwin Brady. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming, 23:552--593, 9 2013. ISSN 1469-7653.

[3]

Edwin Brady. Programming and Reasoning with Algebraic Effects and Dependent Types. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, 2013. To appear.

Digital Library

[4]

Edwin Brady and Kevin Hammond. Resource-safe systems programming with embedded domain specific languages. In Practical Aspects of Declarative Languages, pages 242--257. Springer, 2012.

Digital Library

[5]

Adam Chlipala. Ur: Statically-typed metaprogramming with type-level record computation. In Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '10, pages 122--133, New York, NY, USA, 2010. ACM. ISBN 978-1-4503-0019-3.

Digital Library

[6]

David Raymond Christiansen. Dependent Type Providers. In Workshop on Generic Programming (WGP '13), 2013.

Digital Library

[7]

Ezra Cooper, Sam Lindley, Philip Wadler, and Jeremy Yallop. The essence of form abstraction. In Programming Languages and Systems, pages 205--220. Springer, 2008.

Digital Library

[8]

Robert DeLine and Manuel Fähndrich. Typestates for objects. In ECOOP 2004--Object-Oriented Programming, pages 465--490. Springer, 2004.

[9]

Lee Garber. Security, Privacy, and Policy Roundup. IEEE Security & Privacy, 10(2):15--17, 2012. ISSN 1540-7993.

Digital Library

[10]

Imperva. Lessons Learned From the Yahoo! Hack. 2013. URL http://www.imperva.com/download.asp?id=299.

[11]

C. McBride and J. McKinna. The view from the left. Journal of Functional Programming, 14(1):69--111, 2004.

Digital Library

[12]

Conor McBride and Ross Paterson. Functional pearl: Applicative programming with effects. Journal of functional programming, 18(1): 1--13, 2008.

Digital Library

[13]

Erik Meijer. Server side web scripting in Haskell. Journal of Functional Programming, 10:1--18, 1 2000. ISSN 1469-7653.

Digital Library

[14]

OWASP. Cross-site Scripting (XSS). URL https://www.owasp.org/index.php/Cross-site_scripting.

[15]

OWASP. SQL Injection, 2013. URL https://www.owasp.org/index.php/SQL_injection.

[16]

Rinus Plasmeijer and Peter Achten. iData for the world wide web--programming interconnected web forms. In Functional and Logic Programming, pages 242--258. Springer, 2006.

Digital Library

[17]

Rinus Plasmeijer and Peter Achten. A Conference Management System based on the iData Toolkit. In Implementation and Application of Functional Languages, pages 108--125. Springer, 2007.

Digital Library

[18]

Rinus Plasmeijer, Peter Achten, and Pieter Koopman. iTasks: executable specifications of interactive work flow systems for the web. SIGPLAN Not, 42:141--152, 2007.

Digital Library

[19]

Gordon Plotkin and Matija Pretnar. Handlers of Algebraic Effects. In ESOP 09: Proceedings of the 18th European Symposium on Programming Languages and Systems, pages 80--94, 2009.

Digital Library

[20]

Christian Queinnec. Inverting back the inversion of control or, continuations versus page-centric programming. ACM SIGPLAN Notices, 38 (2):57--64, 2003.

Digital Library

[21]

Don Syme, Keith Battocchi, Kenji Takeda, Donna Malayeri, Jomo Fisher, Jack Hu, Tao Liu, Brian McNamara, Daniel Quirk, Matteo Taveggia, et al. Strongly-typed language support for internet-scale information sources. Technical report, Microsoft Research, 2012.

[22]

Peter Thiemann. WASH/CGI: Server-side web scripting with sessions and typed, compositional forms. In Practical Aspects of Declarative Languages, pages 192--208. Springer, 2002.

Digital Library

[23]

Eelco Visser. WebDSL: A case study in domain-specific language engineering. In Generative and Transformational Techniques in Software Engineering II, pages 291--373. Springer, 2008.

Digital Library

[24]

W3Techs. Usage of server-side programming languages for websites, July 2013. URL http://w3techs.com/technologies/overview/programming_language/all.

Cited By

Ciccone LPadovani LGabbrielli MAbel ACheney J(2020)A Dependently Typed Linear π-Calculus in AgdaProceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming10.1145/3414080.3414109(1-14)Online publication date: 8-Sep-2020
https://dl.acm.org/doi/10.1145/3414080.3414109
Kazerounian MGuria SVazou NFoster JVan Horn DMcKinley KFisher K(2019)Type-level computations for Ruby librariesProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314630(966-979)Online publication date: 8-Jun-2019
https://dl.acm.org/doi/10.1145/3314221.3314630
Thaler JAltenkirch TSiebers P(2018)Pure Functional EpidemicsProceedings of the 30th Symposium on Implementation and Application of Functional Languages10.1145/3310232.3310372(1-12)Online publication date: 5-Sep-2018
https://dl.acm.org/doi/10.1145/3310232.3310372
Show More Cited By

Index Terms

Dependent Types for Safe and Secure Web Programming
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Functional languages

Recommendations

A specification for dependent types in Haskell

We propose a core semantics for Dependent Haskell, an extension of Haskell with full-spectrum dependent types. Our semantics consists of two related languages. The first is a Curry-style dependently-typed language with nontermination, irrelevant ...
Cayenne—a language with dependent types

Cayenne is a Haskell-like language. The main difference between Haskell and Cayenne is that Cayenne has dependent types, i.e., the result type of a function may depend on the argument value, and types of record components (which can be types or values) ...
Depending on types
ICFP '14: Proceedings of the 19th ACM SIGPLAN international conference on Functional programming

Is Haskell a dependently typed programming language? Should it be? GHC's many type-system features, such as Generalized Algebraic Datatypes (GADTs), datatype promotion, multiparameter type classes, and type families, give programmers the ability to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

IFL '13: Proceedings of the 25th symposium on Implementation and Application of Functional Languages

August 2013

146 pages

ISBN:9781450329880

DOI:10.1145/2620678

General Chair:
Rinus Plasmeijer
Radboud University Nijmegen, The Netherlands

Copyright © 2013 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 28 August 2013

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

IFL '13

IFL '13: The 25th symposium on Implementation and Application of Functional Languages

August 28 - 30, 2013

Nijmegen, Netherlands

Acceptance Rates

Overall Acceptance Rate 19 of 36 submissions, 53%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
185
Total Downloads

Downloads (Last 12 months)12
Downloads (Last 6 weeks)0

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ciccone LPadovani LGabbrielli MAbel ACheney J(2020)A Dependently Typed Linear π-Calculus in AgdaProceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming10.1145/3414080.3414109(1-14)Online publication date: 8-Sep-2020
https://dl.acm.org/doi/10.1145/3414080.3414109
Kazerounian MGuria SVazou NFoster JVan Horn DMcKinley KFisher K(2019)Type-level computations for Ruby librariesProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314630(966-979)Online publication date: 8-Jun-2019
https://dl.acm.org/doi/10.1145/3314221.3314630
Thaler JAltenkirch TSiebers P(2018)Pure Functional EpidemicsProceedings of the 30th Symposium on Implementation and Application of Functional Languages10.1145/3310232.3310372(1-12)Online publication date: 5-Sep-2018
https://dl.acm.org/doi/10.1145/3310232.3310372
Claret GRégis-Gianas YGnesi SPlat N(2015)Mechanical verification of interactive programs specified by use casesProceedings of the Third FME Workshop on Formal Methods in Software Engineering10.5555/2820126.2820142(61-67)Online publication date: 16-May-2015
https://dl.acm.org/doi/10.5555/2820126.2820142
Claret GRégis-Gianas Y(2015)Mechanical Verification of Interactive Programs Specified by Use CasesProceedings of the 2015 IEEE/ACM 3rd FME Workshop on Formal Methods in Software Engineering10.1109/FormaliSE.2015.17(61-67)Online publication date: 18-May-2015
https://dl.acm.org/doi/10.1109/FormaliSE.2015.17
Brady E(2014)Resource-Dependent Algebraic EffectsTrends in Functional Programming10.1007/978-3-319-14675-1_2(18-33)Online publication date: 27-Dec-2014
https://doi.org/10.1007/978-3-319-14675-1_2

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents