Online Detection of Effectively Callback-Free Objects with Applications to Smart Contracts
Explore the concept of effectively callback-free objects and their significance in smart contracts. Delve into modular reasoning, evolving systems, Ethereum applications, and the notion of correctness within this innovative framework.
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. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
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.
E N D
Presentation Transcript
Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts Shelly Grossman Ittai Abraham Guy Golan-Gueta Yan Michalevsky Noam Rinetzky Mooly Sagiv Yoni Zohar
Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts Shelly Grossman Ittai Abraham Guy Golan-Gueta Yan Michalevsky Noam Rinetzky Mooly Sagiv Yoni Zohar
Modular Systems int X = 100 .... dec(a){ log(a) } inc(b){ X += b } int Z = 4 log(b){ Z = b } int T=0 f(q,e) { f(t, e) }
Modular Systems dec(100) int X = 100 .... dec(a){ log(a) } inc(b){ X += b } int Z = 4 log(b){ Z = b } int T=0 f(q,e) { f(t, e) } f(1,2)
Evolving Modular Systems int X = 100 .... dec(a){ log(a) } inc(b){ X += b } int Z = 4 log(b){ z = b } int T=0 f(q,e) { f(t, e) } .
Evolving Modular Systems int X = 100 .... dec(a){ log(a) } inc(b){ X += b } log(b){ dec(b) } int T=0 f(q,e) { f(t, e) } .
Evolving Modular Systems are Real int X = 100 .... dec(a){ log(a) } inc(b){ X += b } log(b){ dec(b) } int T=0 f(q,e) { f(t, e) } Ethereum .
Notion of Correctness? int X = 100 .... dec(a){ log(a) } inc(b){ X += b } log(b){ dec(b) } int T=0 f(q,e) { f(t, e) } .
Modular Correctness: ?.Blue? P int X = 100 dec(a){ log(a) } inc(b){ X += b }
Modular Reasoning int X = 100 dec(a){ log(a) } inc(b){ X += b }
Encapsulation Modular Reasoning? module Blue int X := 100 void dec(a) if (X >= a) log(a) X := X a @Inv:X 0?
Encapsulation Modular Reasoning? module Blue int X := 100 void dec(a) if (X >= a) log(a) X := X a @Inv:X 0?
Encapsulation Modular Reasoning? module Blue int X := 100 X 0 void dec(a) if (X >= a) log(a) X := X a @Inv:X 0?
Encapsulation Modular Reasoning? module Blue int X := 100 X 0 void dec(a) if (X >= a) log(a) X := X a X 0 X a @Inv:X 0?
Encapsulation Modular Reasoning? module Blue int X := 100 X 0 void dec(a) if (X >= a) log(a) X := X a X 0 X a @Inv: X 0?
Encapsulation Modular Reasoning module Red module Blue int X := 100 void log(a) if (*) dec(a) void dec(a) if (X >= a) log(a) X := X a
Encapsulation Modular Reasoning module Red module Blue int X := 100 void log(a) if (*) dec(a) void dec(a) if (X >= a) log(a) X := X a X a X a Store: X=100 X=0 X=-100 dec(100) Blue Red Blue Red Stack/ Trace: log(100) dec(100) log(100)
The Challenge: Callbacks int X = 100 dec(a){ log(a) } int Z = 4 log(b){ dec(b) } ... dec(100) Blue log(100) Red Blue or inc(100) dec(100)
Do We Really Need Callbacks? Yes Essential when there is no shared state
Do We Really Need Callbacks? Yes Essential when there is no shared state Increasing usage in Ethereum Ethereum
Effective Callback Freedom (ECF) Modular correctness condition(s) Final-State ECF (ECFFS) Conflict ECF (ECFC) Tames callbacks Enables modular reasoning
Complete Executions An execution? = s0 sn is complete if ?0 ?? ? =
Final State Effective Callback Freedom A completeexecution? is ECFFS for an object O if ? = ?0 ?k . i. ?i is complete ? has no callbacks first(? )|O = first(?)|O last(? )|O = last(?)|O
Final State Effective Callback Freedom A completeexecution? is ECFFS for an object O if ? = ?0 ?k . i. ?i is complete ? has no callbacks first(? )|O = first(?)|O last(? )|O = last(?)|O ?0 ?? ? =
Final State Effective Callback Freedom A completeexecution? is ECFFS for an object O if ? = ?0 ?k . i. ?i is complete ? has no callbacks first(? )|O = first(?)|O last(? )|O = last(?)|O ?0 ?? ? = Callback
Final State Effective Callback Freedom A completeexecution? is ECFFS for an object O if ? = ?0 ?k . i. ?i is complete ? has no callbacks first(? )|O = first(?)|O last(? )|O = last(?)|O ?0 ?? ? = ? = ?0 ??
Final State Effective Callback Freedom A completeexecution? is ECFFS for an object O if ? = ?0 ?k . i. ?i is complete ? has no callbacks first(? )|O = first(?)|O last(? )|O = last(?)|O ?0 ?? ? = ? = ?0 ?? |? |? ??|?= ?? ?0|?= ?0
Final State Effective Callback Freedom A completeexecution? is ECFFS for an object O if ? = ?0 ?k . i. ?i is complete ? has no callbacks first(? )|O = first(?)|O last(? )|O = last(?)|O O? O? ? ?
A Non ECFFS Execution for Blue module Red module Blue int X := 100 void log(a) if (*) dec(a) void dec(a) if (X >= a) log(a) X := X a X=100 X=0 Store: X=-100 dec(100) Blue Red Blue Red Stack/ Trace: log(100) dec(100) Callback log(100)
A Non ECFFS Execution for Blue Every Execution is ECFFS for Blue module Red module Blue int X := 100 void log(a) if (*) dec(a) void dec(a) if (X >= a) log(a) X := X a log(a) X := X a X=100 X=100 Blue Red Blue X=0 X=0 Store: Store: X=-100 X=0 dec(100) dec(100) Blue Red Blue Red Stack/ Trace: Trace: Stack/ log(100) log(100) dec(100) dec(100) Callback Callback log(100)
Real World Example: The DAO Attack 20June 2016: software bug in DAO, an Ethereum contract, led to a (temporary) theft of 3,500,000 ETH DAO attack exploited not ECF callbacks The DAO Ethereum
Gist of DAO Attack DAO_withdraw(to) { if (shares[to] > 0) { to.send(shares[to]); shares[to] = 0 } }
(Dynamic) ECFFS A completeexecution? is ECFFS for an object O ?0 ?? ? = if ? ? = ?0 ?? |? |? ??|?= ?? ?0|?= ?0
(Dynamic) ECFFS A completeexecution? is ECFFS for an object O ?0 ?? ? = The state (of O) produced by the execution with callbacks can also be produced by a callback free execution if ? ? = ?0 ?? |? |? ??|?= ?? ?0|?= ?0
Static ECFFS An objectO is static ECFFSif every complete execution is ECFFS for O
Static ECFFS Modular Reasoning An objectO is static ECFFSif every complete execution is ECFFS for O module Blue int X := 100 X 0 void dec(a) if (X >= a) X := X a log(a) X 0 X a @Inv:X 0
(Dynamic) ECFFS Modular Reasoning Provided we enforce ECFFSin runtime module Blue int X := 100 X 0 void dec(a) if (X >= a) log(a) X := X a X 0 X a @Inv:X 0
Final-State Effective Callback Freedom Static ECFFS is undecidable Decidable if we have a finite data domain (Dynamic) ECFFS is undecidable We cannot check if an arbitrary execution is ECFFS
Conflict Effective Callback Freedom A completeexecution? is ECFC for an object O if ? . ? is a permutation of the O invocations in ? preserving order of conflicting events
Conflict Effective Callback Freedom A completeexecution? is ECFC for an object O if ? . ? is a permutation of the O invocations in ? preserving order of conflicting events ? =
Conflict Effective Callback Freedom A completeexecution? is ECFC for an object O if ? . ? is a permutation of the O invocations in ? preserving order of conflicting events ? =
Conflict Effective Callback Freedom A completeexecution? is ECFC for an object O if ? . ? is a permutation of the O invocations in ? preserving order of conflicting events ? = ? =
