Securing Multiparty Online Services via Certification of Symbolic Transactions

论文笔记 Multiparty Verification

作者：Eric Y. Chen, Shuo Chen, Shaz Qadeer, Rui Wang

单位：Carnegie Mellon University, Microsoft Research

Introduction

CST(Certification of Symbolic Transactions)是一种验证第三方认证过程安全性的方法，然而不同于过去那种不断进行循环测试，观察认证过程是否存在问题的方法，它通过保证认证过程的每一步都完全正确来确保其安全性。

好处：

1. 不再需要为了存在的错误或系统平台而专门建立模型，因为每一次验证都是真实在发生的对话。
2. 因为没有通过CST的请求会直接被回绝，所以程序员只要保证程序能够运行即可，这样他们只需考虑如何实现预期的结果，而无需考虑那些在预期之外的场景。

工程主页：https://sites.google.com/site/symbolictransaction/

Overview of CST

简单来说，CST的工作原理就是，它增添了一个名为SymT（Symbolic Transaction）的消息域，附在每一条消息后，用来收集每一方所执行的源代码（仅仅只是一些协议实现的方法），然后将它合成一个程序，显示了整个消息传递过程。这之后，CST再检查该程序是否符合ambient predicate。

威胁模型：

攻击者拥有自己的浏览器和服务器，但并不能控制非攻击方的服务器，所有通信用HTTPS保护，攻击者无法读取或篡改。

The CST Certifier

Certifier是用来验证Symbolic Transaction的一个方法，其定义如下：

bool certify(string FinalSymT,
            string AmbientPredicate,
            string[] TrustedParties)

Symbolic Transaction

假设a.com的一个输出，对b.com是一个输入。那么在这一步中最重要的问题就在于，为什么b.com要相信它所收到的输入来自于a.com。

对这一问题，只有2个可能的答案：

1. 这一输入被a.com签过名
2. b.com自己向a.com发起了一次server-to-server的通话

这里定义SymT在不同场景下的形式：

Scenario A：一个未经过签名的请求（不安全）

b.com:#method2(a.com:#method1(...))

Scenario B：一个经过签名的请求

b.com:#method2(a.com::#method1(...))

Scenario C：一个由b.com发起的server-to-server请求

b.com:#method2((a.com:#method1(...)))

签名验证：
既然有签名存在，那签名验证就是必要的。
接收者需要保证：

1. SymT这一消息域也被签名所覆盖
2. 如果SymT写的是a.com::#method1(...)，那这就可以确定改签名的确是由a.com所签的

在这里，CST的做法是：如果现有的实现中，消息没有被签名，那就什么都不做，如果消息有被签过名，那CST就将SymT作为一个参数附上，然后将整个消息送去给下层的签名层进行签名。

Synthesizer

Synthesizer的作用，是找到SymT中第一个（最外层的）不可信任环节，这一查找过程可以归结为2点：

1. 发现一个不属于TrustedParty的party id
2. 这一个方法无法防止篡改（即符合Scenario A中的“PARTY-ID:METHOD-CALL”模式）

一旦发现这样的环节，那其自身，包括其内部的所有方法都应该被去掉。

以SymT=TStore:#completeOrder(Cashier.com::#pay(TStore.com::#placeOrder()))为例，其综合而成的程序如下图所示：

假设一种攻击场景：攻击者在自己的服务器MarkStore.com上发出了一张订单，并把钱付给了攻击者自己，却在最后completeOrder的时候把订单发给了TStore。
此时SymT=TStore:#completeOrder(Cashier.com::#pay(MarkStore.com::#placeOrder()))
那在综合时，就会发现此中存在一个不属于TrustedParty的MarkStore.com，这一部分则将会被去除，从而在综合出来的程序里，L1和L2将不复存在，最终导致assert出错。

另外一种场景，placeOrder这一步并没有进行防篡改的措施，即SymT=TStore:#completeOrder(Cashier.com::#pay(TStore.com:#placeOrder()))。同样地，L1和L2将不存在，同样导致assert出错。

Verifier

Cache

由于程序验证需要花费比较长的时间（10-30秒），这不可能每次交易都运行，所以缓存是必要的。Certifier将缓存每一个三元组（FinalSymT，AmbientPredicate，Trustedarties）的结果（true/false）。

Put it together

1. 构造SymT：这一步主要是被动地去对整个过程进行记录，包括所有的重要信息（比如消息是否有签名，是重定向还是服务器间的通信）。
2. vProgram综合：综合过程就是从SymT重新还原整个计算过程，并去除不安全的环节
3. vProgram验证：检查还原出来的程序是否足够确保ambient predicate被实现。

一些重要的实际考虑

Ambient Predicate和重放攻击：

仅仅依靠上面的3个步骤，是无法抵御重放攻击的，所以为了防止重放，一个序列号（或者随机数）应该被加入到ambient predicate中去，从而保证同一个请求不会被多次提交。

去除验证失败所造成的影响：

CST验证失败将导致某一步操作无法执行，所以程序必须另外地加入验证失败处理操作。由于即便是协议本身，有时候也可能会发生认证失败的情况，所以开发者不需要另外撰写处理程序，直接将CST验证结果加入到拒绝请求的条件中去即可。