סוג האירוע

בחר הכל

הרצאות פומביות

מבחן/תחרות

סמינרים

קולוקוויום

כנסים וימי עיון

צהרי יום א'

ימים פתוחים וייעוץ

טקסים ואירועים מיוחדים

הרצאות לקהל הרחב

מועדון קשרי אקדמיה-תעשייה

תחום האירוע

בחר הכל

הפקולטה למדעים מדויקים

ביה"ס למדעי המתמטיקה

ביה"ס לפיזיקה ולאסטרונומיה

המועדון האסטרונומי

ביה"ס לכימיה

מרכז לחקר אינטראקציות אור חומר

סימפוזיונים והרצאות מיוחדות

החוג למדעי כדור הארץ

ביה"ס למדעי המחשב

ביה"ס למדעי כדור הארץ

The TAU Programming Languages and Systems Seminar - Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts

Shelly Grossman, TAU

10 בדצמבר 2017, 14:00 
בניין שרייבר, חדר 309 
הרצאה לקהל הרחב

Abstract:

 

Callbacks are essential in many programming environments, but drastically complicate program understanding and reasoning because they allow to mutate object’s local states by external objects in unexpected fashions, thus breaking modularity. The famous DAO bug in the cryptocurrency framework Ethereum, employed callbacks to steal $150M. We define the notion of Effectively Callback Free (ECF) objects in order to allow callbacks without preventing modular reasoning.An object is ECF in a given execution trace if there exists an equivalent execution trace without callbacks to this object. An object is ECF if it is ECF in every possible execution trace. We study the decidability of dynamically checking ECF in a given execution trace and statically checking if an object is ECF. We also show that dynamically checking ECF in Ethereum is feasible and can be done online. By running the history of all execution traces in Ethereum, we were able to verify that virtually all existing contract executions, excluding the DAO or contracts with similar known vulnerabilities, are ECF. Finally, we show that ECF, whether it is verified dynamically or statically, enables modular reasoning about objects with encapsulated state.

אוניברסיטת תל-אביב, ת.ד. 39040, תל-אביב 6997801
UI/UX Basch_Interactive