EAGER: Synthesizing and Optimizing Declarative Smart Contracts

This project studies the design and implementation of a new class of smart contracts. Smart contracts are a kind of contract used in Blockchain, where a transaction is automatically triggered when the contract's conditions are met. Reliable and efficient smart contracts are essential for the robustness of any financial infrastructure and supply chains running on blockchain platforms.

Errors in smart contracts have resulted in millions of dollars in loses. The project will enable global financial transactions to be carried out in a safe and efficient manner, benefiting mission-critical capabilities of secure supply chains and ensuring the delivery of goods such as medical products. The resulting tool will be open-sourced for widespread adoption.

This project aims to develop DeSCO, a Declarative Smart Contract Optimizer that integrates novel optimization techniques and conventional database optimization strategies into designing and implementing efficient smart contracts. DeSCO will be based on Datalog, a declarative logic programming language. The declarative smart contract written in Datalog is then compiled into efficient Solidity programs for actual implementation.

DeSCO is part of a trend toward adopting higher-level domain-specific languages with strong guarantees. Datalog frees programmers from low-level implementation details, allowing them to reason about the contract at the specification level via inference rules. The first thrust aims to extend the Datalog language to support domain-specific language features necessary for implementing complex smart contracts.

Language extensions to be explored include support for complex functions, recursion and iterations, and event-based programming, amongst others. The second thrust explores techniques for synthesizing smart contracts from input/output example scenarios. The third thrust explores techniques for optimizing smart contracts via minimizing resource consumption.

Cost models estimate resource consumption, inform novel single-query and multi-query optimization techniques, and reduce the likelihood of resource exhaustion attacks.

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.