2vyper: Contracts for Smart Contracts
Alexander J. Summers
University of British Columbia
27 Apr 2023, 4:00 pm - 5:00 pm
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 111
simultaneous videocast to Kaiserslautern building G26, room 111
SWS Colloquium
Smart contract languages are increasingly popular and numerous, and their
programming models and challenges are somewhat unusual. The ubiquitous presence
of untrusted external code in such a system makes classical contracts
unsuitable for safety verification, while the intentional presence of
(potentially-mutating) callbacks via unknown code makes standard static
analysis techniques imprecise in general. On the other hand, smart contract
languages such as Vyper (for Ethereum) tightly encapsulate direct access to the
program's state. In this talk I'll present a methodology for expressing
contracts for this language, ...
Smart contract languages are increasingly popular and numerous, and their
programming models and challenges are somewhat unusual. The ubiquitous presence
of untrusted external code in such a system makes classical contracts
unsuitable for safety verification, while the intentional presence of
(potentially-mutating) callbacks via unknown code makes standard static
analysis techniques imprecise in general. On the other hand, smart contract
languages such as Vyper (for Ethereum) tightly encapsulate direct access to the
program's state. In this talk I'll present a methodology for expressing
contracts for this language, in a way that supports sound verification of
safety properties, with deductive verification tooling (converting Vyper to
Viper) to automate the corresponding proofs.
Based on joint work with Christian Bräm, Marco Eilers, Peter Müller and Robin Sierra; see also the accompanying paper at OOPSLA 2021. --- Please contact Office for Zoom link information.
Read more
Based on joint work with Christian Bräm, Marco Eilers, Peter Müller and Robin Sierra; see also the accompanying paper at OOPSLA 2021. --- Please contact Office for Zoom link information.