Table of Contents
The picture below gives an overview, how
sbuilder-ethereum is hooked to Ethereum development
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,
setup.tla, is executed, using TLA-tools, where any violation of the correctness criteria found during model checking is flagged as an error.
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.
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
tla-sbuilder to is shown in the picture below:
Example Demonstrating Solidity Re-Entract Attack
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