Smart contracts, or computer programs, are thought to be safer for online transactions than traditional contracts, although they are not error-proof. Smart contracts automatically carry out specific agreed-upon actions when certain circumstances are satisfied. As part of a multi-institution effort, researchers from the Penn State College of Information Sciences and Technology (IST) created an end-to-end model-based framework in place of conventional programming code to make smart contracts simpler to create, simpler to verify, and ultimately safer to use.
In the IEEE Transactions on Dependable and Security Computing, they published their proposal.
“As with most software, the code used to program smart contracts is prone to error and vulnerabilities,” said Aron Laszka, assistant professor in the College of IST and the project’s primary researcher. In particular, when working with other smart contracts, “our project focused on the significant technical challenges involved with ensuring that code accomplishes what it was intended to accomplish.”
Blockchain platforms, which are also used to store digital currencies like Bitcoin, are where smart contracts are kept. According to Laszka, the blockchain platform is designed to increase the security of smart contracts, which frequently manage valuable assets. Although the platform promises that the smart contract will work as intended, it does not check that the contract’s code is accurate.
A specific action is carried out on a blockchain and updated such that the transaction cannot be changed when the predetermined conditions of a smart contract are satisfied. Determining the issue, however, can be difficult when the smart contract does not operate as predicted, the researchers claim.
He claimed that manually created smart contracts in programming languages were difficult to validate. “Software bugs might not be discovered until after the smart contract has been deployed, at which point it can be used against it.”
Laszka used an online auction as an illustration. The conditions spelled out in the auction code prevent additional bids from being made after the auction has ended. But when used, the auction permits the winning bidder to be changed after it ends. Post-deployment verification tools may find that the programming language—the instruction—is incorrect, but they do not specifically point out where the error is or what the programmers need do to remedy it.
Developers want more effective verification tools to make sure that a smart contract will function as intended, according to Laszka, who cited security breaches in recent years in which attackers stole assets from smart contracts or completely destroyed them.
Programming language and machine code verification tools abound in both academia and industry, and there are businesses that may be hired to carry out contract audits, according to Laszka. However, the feedback offered by these products and services “can be mediocre and not always helpful.”
Despite the fact that earlier research on smart contract verification, vulnerability finding, and secure development often only takes individual contracts in isolation, Laszka claims that occurrences like security breaches frequently take advantage of the connection between numerous smart contracts.
To close this gap, Laszka and his team developed VeriSolid, a framework for formal contract verification utilizing an abstract-state machine-based model that executes the contract precisely as specified. According to the authors, “this approach enables developers to think about and verify the behavior of a set of interacting contracts at a high level of abstraction.”
The researchers claim that this alteration starts during the development phase. Developers might specify how the contract should function in a straightforward, user-friendly manner using a high-level abstract model.
As opposed to lines of computer language code, abstract concepts are easier for humans to work with, according to Laszka. “We can provide feedback at this higher level of abstraction to identify the problem if verification tools within the model find that something is wrong,” the author says.
The highest bidder changed since the bidding functionality is still available after the sale has ended in the case of the online auction, as revealed by the model’s verification feedback.
“With our proposed model, the smart contract can be verified before deployment,” stated Laszka. Additionally, as if the developer had manually created the source code in programming language, the tools can actually produce it from the model to be distributed on the blockchain.
Solidity code, a programming language used to implement smart contracts on blockchain platforms, was created by the researchers using VeriSolid.
“This code is functionally and behaviorally equivalent to verified models, enabling the creation of correct-by-design smart contracts,” stated Laszka. Deployment diagrams, a graphical formalism for describing potential interactions between contract types, were also added.
A framework for the automated verification, creation, and deployment of contracts that adhere to a deployment diagram was thus presented by the researchers in this position.
“The high-level model form allows developers to specify desired properties—for both standalone and interacting smart contracts—in a way they are unable to do with low-level programming language,” added Laszka. Additionally, “as a common framework, we synchronize verification and deployment, enabling a contract to be published on a blockchain network once verified.”
Links
