8/23/2022 Aaron Seidlitz, Illinois CS
Illinois CS professor Grigore Rosu advises PhD student Xiaohong Chen, with whom he will now work collaboratively on a new research project for Ethereum – the second blockchain after Bitcoin.
Written by 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.
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.