Lolisa: Formal Syntax and Semantics for a Subset of the Solidity Programming Language in Mathematical Tool Coq

Zheng Yang and Hang Lei

Mathematical Problems in Engineering, 2020, vol. 2020, 1-15

Abstract:

The security of blockchain smart contracts is one of the most emerging issues of the greatest interest for researchers. This article presents an intermediate specification language for the formal verification of Ethereum-based smart contract in Coq, denoted as Lolisa. The formal syntax and semantics of Lolisa contain a large subset of the Solidity programming language developed for the Ethereum blockchain platform. To enhance type safety, the formal syntax of Lolisa adopts a stronger static type system than Solidity. In addition, Lolisa includes a large subset of Solidity syntax components as well as general-purpose programming language features. Therefore, Solidity programs can be directly translated into Lolisa with line-by-line correspondence. Lolisa is inherently generalizable and can be extended to express other programming languages. Finally, the syntax and semantics of Lolisa have been encapsulated as an interpreter in mathematical tool Coq. Hence, smart contracts written in Lolisa can be symbolically executed and verified in Coq.

Date: 2020
References: Add references at CitEc
Citations:

Downloads: (external link)
http://downloads.hindawi.com/journals/MPE/2020/6191537.pdf (application/pdf)
http://downloads.hindawi.com/journals/MPE/2020/6191537.xml (text/xml)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:hin:jnlmpe:6191537

DOI: 10.1155/2020/6191537

Access Statistics for this article

More articles in Mathematical Problems in Engineering from Hindawi
Bibliographic data for series maintained by Mohamed Abdelhakeem ().