skip to main content
10.1145/1481861.1481866acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

Secure compilation of a multi-tier web language

Published: 24 January 2009 Publication History

Abstract

Storing state in the client tier (in forms or cookies, for example) improves the efficiency of a web application, but it also renders the secrecy and integrity of stored data vulnerable to untrustworthy clients. We study this general problem in the context of the Links multi-tier programming language. Like other systems, Links stores unencrypted application data, including web continuations, on the client tier; hence, Links is open to attacks that expose secrets, and modify control flow and application data. We characterise these attacks as failures of the general principle that ecurity properties of multi-tier applications should follow from review of the source code (as opposed to the detailed study of the files compiled for each tier, for example). We eliminate these threats by augmenting the Links compiler to encrypt and authenticate any data stored on the client. We model this compilation strategy as a translation from a core fragment of the language to a concurrent lambda-calculus equipped with a formal representation of cryptography. To formalize source-level reasoning about Links programs, we define a type-and-effect system for our core language; our implementation can machine-check various integrity properties of the source code. By appeal to a recent system of refinement types for secure implementations, we show that our compilation strategy guarantees all the properties provable by our type-and-effect system.

References

[1]
M. Abadi. Protection in Programming-Language Translations. In Secure Internet Programming, pages 19--34, 1999.
[2]
M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. Information and Computation, 148:1--70, 1999.
[3]
M. Abadi, R. Corin, and C. Fournet. Computational secrecy by typing for the pi calculus. In N. Kobayashi, editor, APLAS, volume 4279 of Lecture Notes in Computer Science, pages 253--269. Springer, 2006.
[4]
J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis. Refinement types for secure implementations. In 21st IEEE Computer Security Foundations Symposium (CSF'08), pages 17--32, 2008.
[5]
S. Chong, J. Liu, A. C. Myers, X. Qi, K. Vikram, L. Zheng, and X. Zheng. Secure web application via automatic partitioning. In SOSP '07: Proceedings of twenty-first ACM SIGOPS symposium on Operating systems principles, pages 31--44, New York, NY, USA, 2007. ACM.
[6]
E. Cooper, S. Lindley, P. Wadler, and J. Yallop. Links: Web Programming Without Tiers. In FMCO: Proceedings of 5th International Symposium on Formal Methods for Components and Objects, LNCS. Springer-Verlag, 2006.
[7]
ECMA International. Standard ECMA-262, ECMAScript Language Specification, 3rd edition. WWW electronic publication, December 1999. http://www.ecma-international.org/publications/standards/Ecma-262.htm.
[8]
C. Flanagan. Hybrid type checking. In ACM Symposium on Principles of Programming Languages (POPL'06), pages 245--256, 2006.
[9]
C. Fournet and T. Rezk. Cryptographically sound implementations for typed information-flow security. In ACM Symposium on Principles of Programming Languages (POPL'08), pages 323--335, 2008.
[10]
D. Gollmann. Authentication by correspondence. IEEE Journal on Selected Areas in Communication, 21(1):88--95, 2003.
[11]
Google. Google Web Toolkit. WWW electronic publication, 2006. http://code.google.com/webtoolkit/.
[12]
A. D. Gordon and A. S. A. Jeffrey. Typing correspondence assertions for communication protocols. TCS, 300:379--409, 2003.
[13]
A. D. Gordon and R. Pucella. Validating a web service security abstraction by typing. Formal Aspects of Computing, 17(3):277--318, 2005.
[14]
P. T. Graunke, S. Krishnamurthi, S. V. D. Hoeven, and M. Felleisen. Programming theWeb with High-Level Programming Languages. In ESOP '01: Proceedings of the 10th European Symposium on Programming Languages and Systems, pages 122--136, London, UK, 2001. Springer-Verlag.
[15]
M. Howard and D. LeBlanc. Writing secure code. Microsoft Press, second edition, 2003.
[16]
J. Hughes. Generalising monads to arrows. Science of Computer Programming, 37:67--111, 2000.
[17]
S. Krishnamurthi, P. W. Hopkins, J. Mccarthy, P. T. Graunke, G. Pettyjohn, and M. Felleisen. Implementation and use of the PLT scheme Web server. HOSC, 20(4):431--460, 2007.
[18]
E. Meijer,W. Schulte, and G. Bierman. Programming with circles, triangles and rectangles. In XML Conference, 2003.
[19]
Microsoft. ASP.Net. WWW electronic publication, November 2006. http://www.asp.net/.
[20]
Microsoft. Language Integrated Query (LINQ). WWW electronic publication, 2005. http://msdn.microsoft.com/en-us/netframework/aa904594.aspx.
[21]
T. Murphy VII, K. Crary, and R. Harper. Type-Safe Distributed Programming with ML5. In Trustworthy Global Computing, LNCS, pages 108--123. Springer, 2008.
[22]
M. Neubauer and P. Thiemann. From sequential programs to multi-tier applications by program transformation. In ACM Symposium on Principles of Programming Languages (POPL'06), pages 221--232, 2005.
[23]
B. C. Pierce and D. N. Turner. Local type inference. In ACM Symposium on Principles of Programming Languages (POPL'98), pages 252--265, 1998.
[24]
C. Queinnec. The influence of browsers on evaluators or, continuations to program web servers. In ACM International Conference on Functional Programming (ICFP'00), pages 23--33, 2000.
[25]
A. Sabry and M. Felleisen. Reasoning about programs in continuationpassing style. LISP and Symbolic Computation, 6(3-4):289--360, 1993.
[26]
J. Scambay and M. Shema. Hacking Web Applications Exposed. McGraw-Hill/Osborne, 2002.
[27]
M. Serrano, E. Gallesio, and F. Loitsch. Hop: a language for programming the web 2.0. In OOPSLA '06: Companion to the 21st ACM SIGPLAN symposium on Object-oriented programming systems, languages, and applications, pages 975--985, New York, NY, USA, 2006. ACM.
[28]
Sun Microsystems. JSR 245: JavaServerTM Pages 2.1. WWW electronic publication, November 2006. http://java.sun.com/jsp/.
[29]
N. Swamy, B. J. Corcoran, and M. Hicks. Fable: A Language for Enforcing User-defined Security Policies. In IEEE Symposium on Security and Privacy, pages 369--383, 2008.
[30]
D. Syme, A. Granicz, and A. Cisternino. Expert F#. Apress, 2007. The PHP Group. PHP: Hypertext Preprocessor. WWW electronic publication, November 2006. http://www.php.net/.
[31]
W3C. Cascading Style Sheets Level 2 Revision 1 (CSS 2.1) Specification.
[32]
WWW electronic publication, July 2007. http://www.w3.org/TR/2007/CR-CSS21-20070719/.
[33]
W3C. HTML 4.01 Specification. WWW electronic publication, December 1999. http://www.w3.org/TR/html401/.
[34]
T.Woo and S. Lam. A semantic model for authentication protocols. In IEEE Computer Society Symposium on Research in Security and Privacy, pages 178--194, 1993.
[35]
H. Xi and F. Pfenning. Dependent types in practical programming. In ACM Symposium on Principles of Programming Languages (POPL'99), pages 214--227, 1999.
[36]
F. Yang, J. Shanmugasundaram, M. Riedewald, and J. Gehrke. Hilda: A High-Level Language for Data-Driven Web Applications. In ICDE '06: Proceedings of the 22nd International Conference on Data Engineering (ICDE'06), page 32, Washington, DC, USA, 2006. IEEE Computer Society.

Cited By

View all
  • (2024)Bridging Between Active Objects: Multitier Programming for Distributed, Concurrent SystemsActive Object Languages: Current Research Trends10.1007/978-3-031-51060-1_4(92-122)Online publication date: 29-Jan-2024
  • (2019)Formal Approaches to Secure CompilationACM Computing Surveys10.1145/328098451:6(1-36)Online publication date: 4-Feb-2019
  • (2017)Secure Compilation and Hyperproperty Preservation2017 IEEE 30th Computer Security Foundations Symposium (CSF)10.1109/CSF.2017.13(392-404)Online publication date: Aug-2017
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
TLDI '09: Proceedings of the 4th international workshop on Types in language design and implementation
January 2009
122 pages
ISBN:9781605584201
DOI:10.1145/1481861
  • General Chair:
  • Andrew Kennedy,
  • Program Chair:
  • Amal Ahmed
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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 24 January 2009

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. compilers
  2. cryptography
  3. integrity
  4. type systems
  5. web application security
  6. web programming

Qualifiers

  • Research-article

Conference

POPL09
Sponsor:

Acceptance Rates

Overall Acceptance Rate 11 of 26 submissions, 42%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)2
  • Downloads (Last 6 weeks)1
Reflects downloads up to 20 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Bridging Between Active Objects: Multitier Programming for Distributed, Concurrent SystemsActive Object Languages: Current Research Trends10.1007/978-3-031-51060-1_4(92-122)Online publication date: 29-Jan-2024
  • (2019)Formal Approaches to Secure CompilationACM Computing Surveys10.1145/328098451:6(1-36)Online publication date: 4-Feb-2019
  • (2017)Secure Compilation and Hyperproperty Preservation2017 IEEE 30th Computer Security Foundations Symposium (CSF)10.1109/CSF.2017.13(392-404)Online publication date: Aug-2017
  • (2016)JSLINQProceedings of the Sixth ACM Conference on Data and Application Security and Privacy10.1145/2857705.2857717(307-318)Online publication date: 9-Mar-2016
  • (2014)EditletsProceedings of the 26nd 2014 International Symposium on Implementation and Application of Functional Languages10.1145/2746325.2746331(1-13)Online publication date: 1-Oct-2014
  • (2014)SeLINQACM SIGPLAN Notices10.1145/2692915.262815149:9(25-38)Online publication date: 19-Aug-2014
  • (2014)SeLINQProceedings of the 19th ACM SIGPLAN international conference on Functional programming10.1145/2628136.2628151(25-38)Online publication date: 19-Aug-2014
  • (2012)The Jasper Framework: Towards a Platform Independent, Formal Treatment of Web ProgrammingElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.98.598(31-45)Online publication date: 22-Oct-2012
  • (2012)Recent developments in low-level software securityProceedings of the 6th IFIP WG 11.2 international conference on Information Security Theory and Practice: security, privacy and trust in computing systems and ambient intelligent ecosystems10.1007/978-3-642-30955-7_1(1-16)Online publication date: 20-Jun-2012
  • (2011)Cryptographic verification by typing for a sample protocol implementationFoundations of security analysis and design VI10.5555/2028200.2028204(66-100)Online publication date: 1-Jan-2011
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media