New Academic Research Grant Through Ethereum Will Increase Safety of Smart Contracts and Blockchain Applications

8/23/2022 10:42:01 AM Aaron Seidlitz, Illinois CS

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

Headshots of Illinois CS student Xiaohong Chen on the left and professor Grigore Rosu on the right.
Illinois CS student Xiaohong Chen (left) and professor Grigore Rosu.

The latest example of his progress is an academic research grant through Ethereum – the second blockchain after Bitcoin – that Chen earned with advisor and Illinois CS professor Grigore Rosu. The two will delve into a research topic entitled, “Trustworthy Formal Verification for Ethereum Smart Contracts via Machine-Checkable Proof Certificates.”

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

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

Chen specifically described the approach to 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-checkable proof certificates as independent correctness certificates of the smart contracts, consensus protocols, and virtual machines.”

Chen is fully confident that the results of the project will pay major dividends.

“The study will greatly improve the safety of the existing smart contracts and blockchain applications to an unprecedented level,” he said. “Every on-chain activity will be justified by a proof certificate, which can be independently checked by any 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 on every node of the chain as it currently stands.”

As blockchain technology continues to emerge, Rosu believes it will be 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 increasing the quality of computing systems.