Announcing Sbuilder Ethereum

Introduction

This post announces sbuilder-ethereum, a tla-sbuilder plugin, to translate Ethereum implementations in Solidity language into in TLA+ language formal models to be model checked using TLA+ Tools.

Overview

sbuilder-ethereum is a tla-sbuilder plugin to translate Ethereum Solidity language implementations into in TLA+ language formal models to be model checked using TLA+ Tools.

The picture below gives an overview, how sbuilder-ethereum is hooked to Ethereum development

overview.jpg

The left hand side box, “Ethereum Development”, shows Solidity source compiled using solc to create byte code executed on Ethrereum Virtual Machinve (EVM) to modify Ethereum block chain.

The right hand side represents processing implemented by sbuilder-ethereum. An Abstract Syntax Tree (AST), created by solc compiler, is combined with correctness criteria and setup configuration by sbuilder-ethereum to produce TLA+ language implementation. The resulting formal model, model.tla and setup.tla, is executed, using TLA-tools, where any violation of the correctness criteria found during model checking is flagged as an error.

Functional Description

sbuilder-ethereum uses API loader extension point and snippet loader extension point in tla-sbuilder to create formal model representing Solidity contracts.

Solidity/TLA translation in sbuilder-ethereum maps Solidity contracts, to tla-sbuilder target system elements:

  • function signatures are mapped to interfaces
  • function implementations are mapped to services
  • state variables are mapped to fields in records modeling data base rows

See document Translation reference in on-line documentation for more details on Solidity/TLA translation.

Criteria to verify correctness in model checking is, currently, not addressed by sbuilder-ethereum, but they can be loaded to formal model using another plugin or services provided by tla-sbuilder core, instead.

To complete a runnable formal model tla-sbuilder uses setups. A setup is a sequence of interface operations, and their input parameters. A setup also defines domain cardinality, or domain values. The tools allows defining multiple setups, each setup resulting to a complete, runnable TLA+ code, allowing application model to be run in various environment context.

A tla-sbuilder configuration file, sbuilder.yaml, binds together the elements needed in formal model generation. Correctness of the resulting formal model is verified using TLA+ Tools model checking.

User’s perspective to using sbuilder-ethereum with tla-sbuilder to is shown in the picture below:

userv-view.jpg

Example Demonstrating Solidity Re-Entract Attack

See blog post for an example using Ethereum Solidity language withdrawal pattern to demonstrate, how tla-sbuilder with sbuilder-ethererum plugin can be used to check for implementation correctness againts re-entrant attack.

Fin

sbuilder-ethereum is just one plugin implementation in tla-sbuilder context. In the future, tla-sbuilder can be exteded with other plugins, such as plugins

  • allowing expressing correctness criteria directly on Solidity contract elements
  • supporting other block chain technology, besides Ethereum, enabling checking correcness of heterogenous block chain environments
Advertisements

One thought on “Announcing Sbuilder Ethereum

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s