IELE: A rigorously designed language and tool ecosystem for the blockchain

Theodoros Kasampalis; Dwight Guth; Brandon Moore; Traian Florin Șerbănuță; Yi Zhang; Daniele Filaretti; Virgil Șerbănuță; Ralph Johnson; Grigore Roşu

doi:10.1007/978-3-030-30942-8_35

IELE: A rigorously designed language and tool ecosystem for the blockchain

Theodoros Kasampalis, Dwight Guth, Brandon Moore, Traian Florin Șerbănuță, Yi Zhang, Daniele Filaretti, Virgil Șerbănuță, Ralph Johnson, Grigore Roşu

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

This paper proposes IELE, an LLVM-style language, together with a tool ecosystem for implementing and formally reasoning about smart contracts on the blockchain. IELE was designed by specifying its semantics formally in the K framework. Its implementation, a IELE virtual machine (VM), as well as a formal verification tool for IELE smart contracts, were automatically generated from the formal specification. The automatically generated formal verification tool allows us to formally verify smart contracts without any gap between the verifier and the actual VM. A compiler from Solidity, the predominant high-level language for smart contracts, to IELE has also been (manually) implemented, so Ethereum contracts can now also be executed on IELE.

Original language	English (US)
Title of host publication	Formal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings
Editors	Maurice H. ter Beek, Annabelle McIver, José N. Oliveira
Publisher	Springer
Pages	593-610
Number of pages	18
ISBN (Print)	9783030309411
DOIs	https://doi.org/10.1007/978-3-030-30942-8_35
State	Published - 2019
Event	23rd Symposium on Formal Methods, FM 2019, in the form of the 3rd World Congress on Formal Methods, 2019 - Porto, Portugal Duration: Oct 7 2019 → Oct 11 2019

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	11800 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	23rd Symposium on Formal Methods, FM 2019, in the form of the 3rd World Congress on Formal Methods, 2019
Country/Territory	Portugal
City	Porto
Period	10/7/19 → 10/11/19

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Online availability

10.1007/978-3-030-30942-8_35

Library availability

Discover UIUC Full Text

Cite this

Kasampalis, T., Guth, D., Moore, B., Șerbănuță, T. F., Zhang, Y., Filaretti, D., Șerbănuță, V., Johnson, R., & Roşu, G. (2019). IELE: A rigorously designed language and tool ecosystem for the blockchain. In M. H. ter Beek, A. McIver, & J. N. Oliveira (Eds.), Formal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings (pp. 593-610). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11800 LNCS). Springer. https://doi.org/10.1007/978-3-030-30942-8_35

IELE: A rigorously designed language and tool ecosystem for the blockchain. / Kasampalis, Theodoros; Guth, Dwight; Moore, Brandon et al.
Formal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings. ed. / Maurice H. ter Beek; Annabelle McIver; José N. Oliveira. Springer, 2019. p. 593-610 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11800 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Kasampalis, T, Guth, D, Moore, B, Șerbănuță, TF, Zhang, Y, Filaretti, D, Șerbănuță, V, Johnson, R & Roşu, G 2019, IELE: A rigorously designed language and tool ecosystem for the blockchain. in MH ter Beek, A McIver & JN Oliveira (eds), Formal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11800 LNCS, Springer, pp. 593-610, 23rd Symposium on Formal Methods, FM 2019, in the form of the 3rd World Congress on Formal Methods, 2019, Porto, Portugal, 10/7/19. https://doi.org/10.1007/978-3-030-30942-8_35

Kasampalis T, Guth D, Moore B, Șerbănuță TF, Zhang Y, Filaretti D et al. IELE: A rigorously designed language and tool ecosystem for the blockchain. In ter Beek MH, McIver A, Oliveira JN, editors, Formal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings. Springer. 2019. p. 593-610. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-30942-8_35

Kasampalis, Theodoros ; Guth, Dwight ; Moore, Brandon et al. / IELE : A rigorously designed language and tool ecosystem for the blockchain. Formal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings. editor / Maurice H. ter Beek ; Annabelle McIver ; José N. Oliveira. Springer, 2019. pp. 593-610 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{de6d5b1c01ee4235828f99a45918f128,

title = "IELE: A rigorously designed language and tool ecosystem for the blockchain",

abstract = "This paper proposes IELE, an LLVM-style language, together with a tool ecosystem for implementing and formally reasoning about smart contracts on the blockchain. IELE was designed by specifying its semantics formally in the K framework. Its implementation, a IELE virtual machine (VM), as well as a formal verification tool for IELE smart contracts, were automatically generated from the formal specification. The automatically generated formal verification tool allows us to formally verify smart contracts without any gap between the verifier and the actual VM. A compiler from Solidity, the predominant high-level language for smart contracts, to IELE has also been (manually) implemented, so Ethereum contracts can now also be executed on IELE.",

author = "Theodoros Kasampalis and Dwight Guth and Brandon Moore and Șerb{\u a}nuț{\u a}, {Traian Florin} and Yi Zhang and Daniele Filaretti and Virgil Șerb{\u a}nuț{\u a} and Ralph Johnson and Grigore Ro{\c s}u",

note = "Publisher Copyright: {\textcopyright} Springer Nature Switzerland AG 2019.; 23rd Symposium on Formal Methods, FM 2019, in the form of the 3rd World Congress on Formal Methods, 2019 ; Conference date: 07-10-2019 Through 11-10-2019",

year = "2019",

doi = "10.1007/978-3-030-30942-8_35",

language = "English (US)",

isbn = "9783030309411",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "593--610",

editor = "{ter Beek}, {Maurice H.} and Annabelle McIver and Oliveira, {Jos{\'e} N.}",

booktitle = "Formal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings",

address = "Germany",

}

TY - GEN

T1 - IELE

T2 - 23rd Symposium on Formal Methods, FM 2019, in the form of the 3rd World Congress on Formal Methods, 2019

AU - Kasampalis, Theodoros

AU - Guth, Dwight

AU - Moore, Brandon

AU - Șerbănuță, Traian Florin

AU - Zhang, Yi

AU - Filaretti, Daniele

AU - Șerbănuță, Virgil

AU - Johnson, Ralph

AU - Roşu, Grigore

PY - 2019

Y1 - 2019

N2 - This paper proposes IELE, an LLVM-style language, together with a tool ecosystem for implementing and formally reasoning about smart contracts on the blockchain. IELE was designed by specifying its semantics formally in the K framework. Its implementation, a IELE virtual machine (VM), as well as a formal verification tool for IELE smart contracts, were automatically generated from the formal specification. The automatically generated formal verification tool allows us to formally verify smart contracts without any gap between the verifier and the actual VM. A compiler from Solidity, the predominant high-level language for smart contracts, to IELE has also been (manually) implemented, so Ethereum contracts can now also be executed on IELE.

AB - This paper proposes IELE, an LLVM-style language, together with a tool ecosystem for implementing and formally reasoning about smart contracts on the blockchain. IELE was designed by specifying its semantics formally in the K framework. Its implementation, a IELE virtual machine (VM), as well as a formal verification tool for IELE smart contracts, were automatically generated from the formal specification. The automatically generated formal verification tool allows us to formally verify smart contracts without any gap between the verifier and the actual VM. A compiler from Solidity, the predominant high-level language for smart contracts, to IELE has also been (manually) implemented, so Ethereum contracts can now also be executed on IELE.

UR - http://www.scopus.com/inward/record.url?scp=85076119712&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85076119712&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-30942-8_35

DO - 10.1007/978-3-030-30942-8_35

M3 - Conference contribution

AN - SCOPUS:85076119712

SN - 9783030309411

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 593

EP - 610

BT - Formal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings

A2 - ter Beek, Maurice H.

A2 - McIver, Annabelle

A2 - Oliveira, José N.

PB - Springer

Y2 - 7 October 2019 through 11 October 2019

ER -

IELE: A rigorously designed language and tool ecosystem for the blockchain

Abstract

Publication series

Conference

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this