A Case Study of Cashier-as-a-Service Based Merchant Logic

Introduction

We have a paper in IEEE Symposium on Security and Privacy 2011 about logic bugs that allow a malicious shopper to shop for free online. Section 5 of the paper contains a model of a merchant software and cashier services. We feel that the supplementary materials of the section may have educational values for students who are interested in real-world problems for verification techniques.

The model

The model is specified in this header file: MerchantAndCaaS.h. It defines a set of functions with "wAPI" prefix. These are the only functions that an attacker can call.

The code is an abstraction of the logic of Interspire and the four payment methods that we discuss in the paper. It may not be easy to understand before you spend sufficient time on it. However, we guranttee you that it is much simpler than the original source code that we studied. Please try to make sense out of the code.

Task No.1

Can you implement function main() of ConcreteAttackerTemplate.c so that at some point in the execution of the program, function Check() will print the message "order xxx was not paid in full"? Such a message indicates a successful exploit.

You have two restrictions though:

  • You can only call functions prefixed with wAPI (and functions that you define of course).
  • You cannot do "new SignedObject(...,CaaS)" or "new SignedObject(...,TargetStore)", nor can you modify a data structure of SignedObject type unless the signer is Attacker.

A Solution to Task No. 1

There are several valid attacks. Here is an example. Its main() function is shown below:

  void main() {
    int gross;
    int tokenID,sessionID,orderID;
    Init();
    gross = 20;
    TargetStore_Checkout(gross,PayPalExpress);
    tokenID = currentTokenID - 1;
    sessionID = currentSessionID - 1;
    TargetStore_PPLExp_ReturnHandler(tokenID,customer,sessionID);
    orderID = currentOrderID - 1;
    gross = 1;
    TargetStore_UpdateCart(gross,sessionID);
    PPLExp_SetBillingInfo(tokenID,customer);
    TargetStore_PPLExp_ReturnHandler(tokenID,customer,sessionID);
    TargetStore_PPLExp_UpdateOrderStatus(orderID,sessionID);
  }

Task No. 2

Can you systematically find all attacks up to a given limit of wAPI calls (e.g., each attack may only make X-or-less wAPI calls)?

Our Solution to Task No. 2

We implemented a symbolic attacker program, and used Poirot to do bounded verification on this program. The details of our verification steps are described on this page. During the verification, attack traces will be exposed by Poirot.

If you like to confirm that the attack traces exposed by Poirot are valid, you can compile and run this concrete attacker program.

Download

All files needed for this case study are contained in this zip file. Unzip and copy the folders to your local disk.

Contacts

Rui Wang [lastname63@indiana.edu]
Shuo Chen [firstnamelastname@microsoft.com]
Shaz Qadeer [lastname@microsoft.com]