New Academic Research Grant Through Ethereum Will Increase Security of Smart Contracts and Blockchain Applications | Computer science

Now in his seventh and final year of the PhD program at Illinois Computer Science, Xiaohong Chen has steadily built on his interest in formal semantics of programming languages.

The latest example of his progress is an academic research grant through Ethereum—the second blockchain after Bitcoin—that Chen received with advisor and Illinois CS professor Grigore Rosu. The two will delve into a research topic titled “Reliable formal verification for Ethereum smart contracts via machine-checkable proof certificates.”

Their project became one of 39 grants in seven different categories, where Ethereum allocated more than $2 million.

“I have always found formal semantics of programming languages ​​to be a fascinating area of ​​research because it studies the security and correctness of computer programs – which are ubiquitous these days – using the most rigorous and reliable method we have even known: mathematics and logic,” Chen said. “For me, Ethereum’s support through this grant is an important recognition that my PhD research is useful for real-world industrial applications and is valued by the industrial community.”

Chen specifically described the approach of this research effort as something aimed at “improving the trustworthiness of Ethereum smart contracts and blockchain applications and making formal verification results more transparent and accessible to all stakeholders.”

The plan is to do so by “generating machine-verifiable proof certificates such as independent correctness certificates for smart contracts, consensus protocols, and virtual machines.”

Chen is absolutely certain that the results of the project will pay big dividends.

“The study will greatly improve the security of the existing smart contracts and blockchain applications to an unprecedented level,” he said. “Every activity in the chain will be justified by a certificate of proof, which can be independently verified by all stakeholders.”

He also foresees another impact the research can create.

“In the long run, the study will make the existing blockchain architecture more energy efficient, because smart contracts only need to be executed once,” Chen said. “The execution results can then be trusted, thus eliminating the need to re-execute them at each node in the chain as it is now.”

As blockchain technology continues to emerge, Rosu believes it will become increasingly important for Illinois CS to remain relevant in this area.

He is proud that his Formal Systems Laboratory continues to aim for projects like this to continue to increase the quality of computer systems.