27/12/2017 11:30Taub 301


Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts

Guy Golan-Gueta

VMware Research

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 efficient 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.

This is a joint work with Shelly Grossman, Ittai Abraham, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv and Yoni Zohar. The full paper will appear in POPL '18.

Bio: Guy Gueta is a Senior Researcher at VMware Research Group. His research interests include distributed systems, synchronization techniques, and programming languages. Recently, he has focused on consensus algorithms and execution models for Blockchain technologies. Prior to VMware, Guy was a Researcher at Yahoo Labs, and a software architect in several large software projects. Guy received a Ph.D. degree in Computer Science from Tel Aviv University in 2015.

31/12/2017 11:30Meyer 1061


A Fast Interface for SGX Secure Enclaves

Ofir Weisse

University of Michigan

[Note unusual date - the talk is on a Sunday!]

Secure execution technologies, such as Intel SGX, offer an attractive solution for protecting one's private data in the public cloud environment. In this talk, we will explore how SGX mitigates various attack surfaces and what are the caveats of naively using the technology to protect applications. Specifically, we will discuss the performance implications of SGX on common applications and understand what are the new bottlenecks created by SGX, which may lead to a 5x performance degradation. We then describe an optimization mechanism, HotCalls, that provides a 13-27x speedup compared to the builtin mechanism supplied by SGX SDK. Overcoming the performance bottlenecks is not enough to construct a useful secure distributed system. We will talk about the missing pieces in SGX to manage multiple entities securely, and how can we fill in the gap.

Bio: Ofir is a Ph.D. candidate at the University of Michigan. His current research focuses on the feasibility of secure execution in the cloud: Enabling low-cost security in the cloud environment, without compromising performance. His recent publications include HotCalls (ISCA 2017) and WALNUT (EuroS&P 2017). Ofir worked for Intel in Haifa as a security researcher in the SGX group. He received his Master's in Computer Engineering from Tel-Aviv University and B.Sc from the Technion. His previous research focused on differential power analysis of cryptographic devices, which was published in CHES and HASP.

3/1/2018 11:30TBA


Side Channel Attacks on Implementations of Curve25519

Daniel Genkin and Yuval Yarom

University of Pennsylvania and University of Maryland; University of Adelaide

In recent years, applications increasingly adopt security primitives designed from the start with built-in side channel protection. A concrete example is Curve25519, which has been recently standardized in RFC-7748. Dealing away with obvious leakage sources such as key-dependent branches and memory accesses, RFC-7748 dictates that implementations should use a highly regular Montgomery ladder scalar-by-point multiplication, a unified, branchless double-and-add formula and a constant-time argument swap within the ladder. Moreover, as Curve25519 provides innate protection from small subgroup attacks, it is recommended that implementations do not validate the inputs, completing the Diffie-Hellman protocol irrespective of the input's mathematical properties.

In this talk we demonstrate that the failure to perform input validation, combined with the unique mathematical structure of Curve25519, can be used to amplify side channel leakage from several RFC-7748 compliant implementations. As case studies, we investigate two RFC-7748 compliant implementations: libgcrypt and the reference implementation provided as part of the NaCl library. We show effective attacks on both of these implementations, recovering secret key material from just a single leakage trace.

Joint work with Daniel Genkin, Niels Samwel, Luke Valenta, and Yuval Yarom.