Enhancing Online Service Security through Symbolic Transaction Certification

The research discusses securing multiparty online services through the certification of symbolic transactions, addressing logic flaws and the importance of program verification. The Certification of Symbolic Transaction (CST) approach is presented as an effective way to verify system-wide properties independent of specific protocols, making verification more feasible for developers. Examples and illustrations highlight the challenges and solutions in verification processes.

• Online security
• Symbolic transactions
• Program verification
• Multiparty systems

huff_ot Follow

Uploaded on Sep 26, 2024 | 0 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

Presentation Transcript

1. Securing Multiparty Online Services via Certification of Symbolic Transactions Eric Chen (Carnegie Mellon University) Shuo Chen, Shaz Qadeer, Rui Wang (Microsoft Research) 1

2. Multiparty online services Third-party payment Single sign-on PayPal.com (cashier) Facebook.com (identity provider) shopper user Buy.com (merchant) foo.com (relying party) Authorization login.facebook.com graph.facebook.com user 2 bar.com

3. Unfortunately, Plenty of logic flaws discovered The No.4 cloud computing top threat According to the Cloud Security Alliance Serious consequences purchase without making payment log into other people s accounts obtain unintended authorizations 3

4. Program verification needed! Program verification For many years, researchers have been advocating for it Rarely put in practice by real developers Several practical hurdles Our work Certification of Symbolic Transaction (CST) Significantly lowers the hurdles. 4

5. Why is verification hard in reality? infinite loop top-level Attacker (modeled) a.com spec b.com spec c.com Written in English. spec Public methods b.com source code Verifier (e.g., theorem prover or model checker) Platform (modeled) c.com source code a.com source code Platform (modeled) Platform (modeled) Developers: Does every possible transaction satisfy safety property in spec? A multiparty system based on protocol X 5

6. Certification of Symbolic Transaction (CST) Actual user/attacker A system-wide multiparty property, independent of specific protocols b.com source code Platform (actual) cv c.com source code a.com source code Certifier Platform (actual) Platform (actual) cv cv Does this transaction satisfy the system-wide property? 6

7. A toy example b.com source code int array B[ ] Ambient predicate (C == true) iff ( i. B[i] == A) c.com source code a.com source code bool C secret int A Ambient predicate cannot be concretely checked c.com has no access to concrete values of A[ ] and B CST s approach -- to collect source code to symbolically check ambient predicate

8. A real example: Third-party payment 8

9. Protocol flow and safety property Data: Data: orders[ ] mySellerID Data: Data: client c cashier ashier merchant merchant payments[ ] PlaceOrder_req PlaceOrder() PlaceOrder_resp Pay() Pay_resp CompleteOrder_resp: accept/reject CompleteOrder () Regardless of specific protocols, this property must hold: The order to be checked out on the merchant is paid on the cashier . Ambient predicate i. ( cashier.payments[i].status == Paid && cashier.payments[i].total ==merchant.orders[completeOrder_req.orderID].gross && cashier.payments[i].payee == merchant.mySellerID && cashier.payments[i].orderID == completeOrder_req.orderID ) 9

10. A traditional implementation (without CST) NopCommerce integrating Amazon Payment TStore.com TStore.com (running (running NopCommerce NopCommerce) ) client Amazon Amazon PlaceOrder_req<orderID orderID=123> PlaceOrder() TStore Pay() Amazon CompleteOrder_resp: accept/reject CompleteOrder () The implementation is vulnerable Allows an attacker (Mark) to pay to his own store (MarkStore.com), but check out an order from TStore.com (details in the paper). Every party performs some local checks, but the ambient predicate is not explicitly checked! 10

11. The implementation enhanced by CST TStore.com TStore.com (running (running NopCommerce NopCommerce) ) client Amazon Amazon PlaceOrder_req<orderID=123, SymT= > PlaceOrder() Pay_req<orderID=123,total=35,returnURL=https:// TStore.com/completeOrder.aspx, SymT= > TStore Pay() CompleteOrder_req<orderID=123,status=Paid, SymT= > Amazon CompleteOrder () Final SymT= SymT = SymT = Final SymT= SymT = TStore.com::#PlaceOrder() Amazon.com::#pay(TStore.com::#PlaceOrder()) TStore.com:#CompleteOrder(Amazon.com::#pay(TStore.com::#PlaceOrder())) Note: # #PlaceOrder PlaceOrder, #Pay of the source code of PlaceOrder(), Pay() and CompleteOrder(). , #Pay and # #CompleteOrder CompleteOrder are the SHA1 hash values 11

12. The certifiers job Assume {TStore.com, Amazon.com} are the only trusted parties; Prove the following theorem: TStore.com:#CompleteOrder(Amazon.com::#pay(TStore.com::#PlaceOrder())) i. ( cashier.payments[i].status == Paid && cashier.payments[i].total ==merchant.orders[completeOrder_req.orderID].gross && cashier.payments[i].payee == merchant.mySellerID && cashier.payments[i].orderID == completeOrder_req.orderID ) 12

13. The certifier de-hash table {TStore.com, Amazon.com} miss cache TStore.com:#CompleteOrder( Amazon.com::#pay( TStore.com:#PlaceOrder( ) ) Program synthesizer: hit 1. 2. 3. Discard untrusted steps Stitch together trusted steps Assert the ambient predicate i. ( blah blah blah blah ) R1=PlaceOrder(arbitrary); R2=Pay(R1); R3=CompleteOrder(R2); Assert( i. ( blah blah blah blah ) ); Result: Verified. Transaction accepted. Off-the-shelf C# program verifier 13

14. If the attack is launched de-hash table {TStore.com, Amazon.com} miss cache TStore.com:#CompleteOrder( Amazon.com::#pay( MarkStore.com::#PlaceOrder() ) ) Program synthesizer: hit 1. 2. 3. Discard untrusted steps Stitch together trusted steps Assert the ambient predicate i. ( blah blah blah blah ) //PlaceOrder is discarded R1=Pay(arbitrary); R2=CompleteOrder(R1); Assert( i. ( blah blah blah blah ) ); Result: Not verified. Transaction rejected. Off-the-shelf C# program verifier 14

15. Applying CST in the real world 15

16. Applying CST on open-source ASP.NET solutions 3rd-party payment: Standard Single sign on: in in OAuth 2.0 SDK A gambling scenario integrating four services Game token manager Coin tosser Gambling site cashier CST s project page http://research.microsoft.com/en-us/projects/CST/ 16

17. Evaluation Lines of code (LoC): In every project, the LoC of added and changed code for each party < 200. Performance Near-zero amortized runtime overhead, thanks to caching. Security Analyzed cases: unbiasedly selected 14 vulnerabilities. 12 of them are logic flaws that CST is able to prevent. Two of them are not addressed by CST A signature validation flaw A client-side same-origin access violation. Protocol independence We come up with several implementations obviously violating OAuth 2.0, but CST makes sure that they all do authentication right! 17

18. Do I have to precisely understand OAuth 2.0 to be secure? client Identity Provider Identity Provider Relying Party Relying Party auth_req auth_req <sessionID, AppID, redirect_uri> auth_resp auth_resp < code > token signIn_req signIn_req < code > token token_req token_req <code, AppID, AppSecret, redirect_uri> Check AppID, AppSecret, redirect_uri Check AppID and redirect_uri, then accept user_ID Question 1: is AppSecret needed for authentication? Question 2: can we use token for authentication? Question 3: what if identity provider doesn t check AppID and return_uri for the token? system-wide property. Difficult to understand exactly which party should do what, and why about a complex protocol. Much better to just verify that all parties collaboratively satisfy a 18

19. Conclusions CST sits on the middle-ground between static verification and runtime checking Static verification CST Runtime checking offline, symbolic runtime, concrete runtime, symbolic CST reduces burdens for developers to do verification Able to verify a system-wide multiparty property Reduces the burden of modeling attacker and platform. The proof obligation is greatly reduced Not to prove safety for all possible transactions , but only the transaction that occurs at the moment. Visit: http://research.microsoft.com/en-us/projects/CST/ 19

20. Backup slides 20

21. The verifier and the cache The program verifier .NET Byte Code ASP.NET C# Boogie Code ByteCode Translator (BCT) Visual Studio C# compiler Corral Caching is important. Synthesis and verification take 10-30 seconds Fortunately, SymT is symbolic. Caching is therefore effective. The cache is shared across all transactions of all users 21

22. Performance Per-transaction cost Per-transaction runtime overhead One-time cost compilation, byte-code translation and verification 18 sec 15 sec Program synthesis using a local de- hash server 3ms 5ms 0ms 0ms Live Connect SDK OpenID 2.0 on DotNetOpenAuth 0ms Facebook SSO using ASP.NET MVC 4 NopCommerce Simple Pay NopCommerce Standard Coin tossing gambling 12 sec 5ms 0ms with Amazon 15 sec 2ms 0ms with PayPal 10 sec 8ms 0ms 32 sec 3ms 22