an item at a lower price, shop for free after paying for one
item and even avoid payment. We reported our findings to
the affected parties and received their acknowledgements.
Our further analysis revealed the logic complexity in CaaS-
based checkout mechanisms, and the effort required to
verify their security property when developing and testing
these systems.
We believe that our study takes the first step in the new
security problem space that hybrid web applications bring to
us. Even for the security analyses of merchant applications,
we have just scratched the surface, leaving many intriguing
functionalities (e.g., cancel, return, subscription, auction,
and marketplace) unstudied. An interesting question might
be, for example, whether we can check out a $1 order and a
$10 order, and cancel the $1 order to get $10 refunded. We
are also considering the security challenges that come with
web service integrations in other scenarios, e.g., social
networks and web authentication services. Fundamentally,
we believe that the emergence of this new web
programming paradigm demands new research efforts on
ensuring the security quality of the systems it produces.
A
CKNOWLEDGMENT
We thank Martín Abadi, Brian Beckman, Josh Benaloh, Cormac
Herley, Dan Simon and Yi-Min Wang for valuable discussions,
Akash Lal for important advices on Poirot, Beth Cate for the legal
assistance and Robert Schnabel for the support that makes this
work possible. We also greatly appreciate Trent Jaeger for
shepherding. Authors with IU were supported in part by the NSF
Grant CNS-0716292 and CNS-1017782. Rui Wang was also
supported in part by a Microsoft Research internship.
REFERENCES
[1] Amazon Security Advisories. Amazon Payments Signature Version 2
Validation. https://payments.amazon.com/sdui/sdui/security
[2] Martín Abadi. Security Protocols: Principles and Calculi (Tutorial
Notes), Foundations of Security Analysis and Design IV, FOSAD
2006/2007 Tutorial Lectures, Springer-Verlag (2007), 1-23.
[3] N. Asokan, Victor Shoup, and Michael Waidner. Asynchronous
protocols for optimistic fair exchange. In Proceedings of IEEE
Symposium on Research in Security and Privacy, pages 86–99, 1998.
[4] Karthikeyan Bhargavan, Cédric Fournet, Andrew Gordon. Modular
verification of security protocol code by typing. ACM Symposium on
Principles of Programming Languages (POPL), 2010
[5] Karthikeyan Bhargavan, Cédric Fournet, Andrew Gordon, Riccardo
Pucella. TulaFale: A security tool for web services. In Symposium on
Formal Methods for Components and Objects (FMCO), 2003
[6] BigCommerce. http://www.bigcommerce.com/
[7] Michael Burrows, Martín Abadi, and Roger Needham. 1990. A logic
of authentication. ACM Trans. Computer Systems 8, 1, 18-36.
[8] Ecommerce Statistics Compendium 2010. http://econsultancy.com/
us/reports/e-commerce-statistics/downloads/2076-econsultancy-
ecommerce-statistics-uk-sample-pdf
[9] Prithvi Bisht, Timothy Hinrichs, Nazari Skrupsky, R. Bobrowicz, and
V. N. Venkatakrishnan, "NoTamper: Automatically Detecting
Parameter Tampering Vulnerabilities in Web Applications," ACM
Conf. on Computer and Communications Security, 2010
[10] Dominique Bolignano. “Towards the Formal Verification of
Electronic Commerce Protocols,” Proceedings of the IEEE Computer
Security Foundations Workshop, 1997.
[11] David Chaum, Amos Fiat, and Moni Naor. Untraceable electronic
cash. In Proceedings on Advances in cryptology (CRYPTO '88).
[12] Stephen Chong, Jed Liu, Andrew C. Myers, Xin Qi, K. Vikram,
Lantian Zheng, and Xin Zhen, "Secure Web Applications via
Automatic Partitioning," ACM Symposium on Operating Systems
Principles (SOSP), October 2007.
[13] Benjamin Cox, J. D. Tygar, and Marvin Sirbu. 1995. NetBill security
and transaction protocol. In Proceedings of the 1st conference on
USENIX Workshop on Electronic Commerce (WOEC'95).
[14] Danny Dolev and Andrew C. Yao. 1981. On the Security of Public
Key Protocols. Technical Report. Stanford University, Stanford, USA.
[15] Santiago Escobar, Catherine Meadows, and Jose Meseguer. 2005. A
rewriting-based inference system for the NRL protocol analyzer:
grammar generation, the 2005 ACM workshop on Formal methods in
security engineering (FMSE '05). ACM, New York, NY, USA, 1-12.
[16] Viktoria Felmetsger, Ludovico Cavedon, Christopher Kruegel, and
Giovanni Vigna, "Toward Automated Detection of Logic
Vulnerabilities in Web Applications," USENIX Security Symposium,
August 2010.
[17] Fiddler Web Debugger. http://www.fiddler2.com/fiddler2
[18] Phillip M. Hallam-Baker. Electronic Payment Schemes.
http://www.w3.org/ECommerce/roadmap.html
[19] Nevin Heintze, J. D. Tygar, Jeannette Wing, and H. Chi Wong.
Model checking electronic commerce protocols. The 2nd USENIX
Workshop on Electronic Commerce , Berkeley, CA, USA. 1996.
[20] Interspire Shopping Cart. http://www.interspire.com/shoppingcart
[21] Live HTTP Headers. http://livehttpheaders.mozdev.org
[22] Gavin Lowe. An attack on the Needham-Schroeder public key
authentication protocol. Information Processing Letters 56(3), 1995
[23] Shiyong Lu and Scott A. Smolka. 1999. Model Checking the Secure
Electronic Transaction (SET) Protocol. The 7th International
Symposium on Modeling, Analysis and Simulation of Computer and
Telecommunication Systems (MASCOTS '99).
[24] Catherine Meadows. Applying Formal Methods to the Analysis of a
Key Management Protocol. Journal of Computer Security, 1992.
[25] Catherine Meadows and Paul F. Syverson. "A Formal Specification
of Requirements for Payment Transactions in the SET Protocol,"
Financial Cryptography 1998
[26] Jonathan K. Millen. The Interrogator Model. IEEE Symposium on
Security and Privacy 1995..
[27] K. K. Mookhey, "Common Security Vulnerabilities in e-commerce
Systems," http://www.symantec.com/connect/ articles/common-
security-vulnerabilities-e-commerce-systems
[28] Steven Murdoch and Ross Anderson, "Verified by Visa and
MasterCard SecureCode: or, How Not to Design Authentication,"
Financial Cryptography and Data Security, January 2010
[29] NopCommerce. http://www.nopcommerce.com/
[30] Poirot: The concurrency sleuth. http://research.microsoft
.com /en-us/projects/poirot/
[31] Resources – Amazon Payments. https://payments.amazon.com/sdui
/sdui/business/resources#cba
[32] SecurityFocus.com. "3D3.Com ShopFactory Shopping Cart Cookie
Price Manipulation Vulnerability," http://www.
Securityfocus.com/bid/6296/discuss
[33] Vitaly Shmatikov and John C. Mitchell, Analysis of a fair exchange
protocol, Symposium on Network and Distributed Systems Security
(NDSS '00), San Diego, CA, Internet Society, 2000.
[34] Softpedia, "Choose the Best Open Source CMS for 2010,"
http://news.softpedia.com/news/Choose-the-Best-Open-Source-CMS-
for-2010-158440.shtml
[35] TopTenReviews. eCommerce Software Review 2011.
http://ecommerce-software-review.toptenreviews.com
[36] K. Vikram, Abhishek Prateek, and Benjamin Livshits, "Ripley:
Automatically Securing Web 2.0 Applications Through Replicated
Execution," ACM Conference on Computer and Communications
Security (CCS), Nov. 2009.
[37] Rui Wang, Shuo Chen, XiaoFeng Wang, Shaz Qadeer. “How to Shop
for Free Online -- Security Analysis of Cashier-as-a-Service Based
Web Stores”. Technical Report, IU-CS-TR690. Supporting materials
are available at http://research.microsoft.com/~shuochen/caas/supp/
[38] Rui Wang, Shuo Chen, XiaoFeng Wang, Shaz Qadeer. “A Case Study
of CaaS Based Merchant Logic,” http://research.microsoft.com/en-
us/people/shuochen/caaslogiccasestudy.aspx
[39] Wikipedia, "Secure Electronic Transaction," http://en.
wikipedia.org/wiki/Secure_Electronic_Transaction
480