ACM recognizes ITI's Meseguer for contributions to the computing field

In a year in which the Association for Computing Machinery (ACM) received more nominations than ever before, ITI researcher Jose Meseguer earned acknowledgement as a 2020 ACM Fellow for achievements in computing.  ACM is the world’s largest educational and scientific computing society. Only the top 1 percent of ACM Members earn Fellow status for their outstanding accomplishments in computing and information technology and/or outstanding service to ACM and the larger computing community. This year, 95 of the organization’s members, including six former Turing Award winners, were named ACM Fellows.

Meseguer credits collaborations with breakthroughs, lifelong connections

When Meseguer joined Illinois computer science in 2001, years of experience already afforded the professor a reputation in formal methods that preceded him.

This reputation derived from his ongoing development of rewriting logic and Maude, a high-performance reflective language and system supporting both equational and rewriting logic specification and programming for a wide range of applications.

“Maude, which I began working on and designed with a research team in the mid-1990s, is now widely used and one of the fastest declarative languages for programming. Over the years I have been at Illinois CS, Maude has connected to a number of different application areas.” Meseguer said. “More importantly, I don’t work with Maude – or in other research projects – in an isolated way. Instead, I have enjoyed and prized very much working with colleagues both in the department and around the world.”

Those connections led to several research achievements, which the ACM Fellow recognized as “the development of logical methods for design and verification of computational systems.” Examples that mean the most to Meseguer include:

• The 2007 publishing of “The rewriting logic semantics project” with fellow Illinois CS professor Grigore Rosu. These two worked together to “bridge the existing gap between language definitions on the one hand, and language implementations and language definitions on the other.” Meseguer said that several substantial applications based off their findings have occurred since, primarily through Rosu’s company Runtime Verification.
• The Maude-NRL Protocol Analyzer (Maude-NPA), a tool for the analysis of cryptographic protocols using functions that obey different equational theories. This security development analyzes the protocols through which consumers conduct financial transactions online.
• A 2005 collaboration regarding Denial-of-Service (DoS) attacks with fellow Illinois CS professors Gul Agha and Carl Gunter, among others, resulting in a report titled, “Formal modeling and analysis of DoS using probabilistic rewrite theories.” Together, the authors described “a way to expand term rewriting theories to include probabilistic aspects that can show the effectiveness of DoS countermeasures.” This pioneering work has led to important subsequent design and verification of other novel DoS protection protocols using Maude.
• The 2007 publication "A Systematic Approach to Uncover Security Flaws in GUI Logic" with former Ph.D. student Ralf Sasse and researchers at Microsoft Research uncovered 13 new types of security vulnerabilities in Internet Explorer (IE) using Maude.  This led to a new version of IE avoiding all these vulnerabilities.
• The Illinois Browser and Operating System (IBOS), which derived from a published report in 2012 with then Illinois CS professor Samuel T. King, Meseguer, and their respective former PhD students Shuo Tang and Ralf Sasse. The authors acknowledged that “current web browsers are complex, have enormous trusted computing bases, and provide attackers with easy access to computer systems.” In response they designed and verified “IBOS: A “Correct-by-Construction Modular Browser.”
• A 2018 cloud based security project – with fellow Illinois CS professor Indranil Gupta, Meseguer's former Ph.D. students Si Liu and Stephen Skeirik and others – entitled “Survivability: Design, formal modeling, and validation of cloud storage systems using Maude.” As this group became among the first to delve into cloud-based security, the group proposed “rewriting logic and its accompanying Maude tools as a suitable framework for formally specifying and analyzing both the correctness and the performance of cloud storage systems.”
• The creation of PALS, (Physically Asynchronous/Logically Synchronous systems) systems with fellow CS professor and Donald B. Gillies Chair in Computer Science Lui Sha and collaborators in the paper “Implementing logical synchrony in integrated modular avionics.” PALS is a “complexity reducing design pattern (that) greatly simplifies the development and verification of fault tolerant distributed applications, ensures optimal system performance, and provides a standard argument for system certification.” PALS solves hard synchronization issues in distributed real-time systems. This work received the IEEE AIAA David Lubkowski Award for Advancement in Digital Avionics, and has been further extended in subsequent research by Meseguer, Sha, and collaborators.

While recognition as ACM Fellow accounts for all these projects and many more, to Meseguer the honor to Meseguer the honor recognizes not just his work, but that of his students and his many collaborators. These partnerships occurred right here at University of Illinois Urbana-Champaign, but also stretched as far as South America, China, Japan, Korea, and many countries in Europe.

“Without the support of collaborators and the Illinois CS department, none of this would’ve been possible,” Meseguer said. “This is much broader than any one individual, and because of that I’ve led a very charmed life. All of the people I’ve worked with share a passion and a love for research that breeds a high level of excellence.

“And the best thing about these people and these collaborations is that they have led to friendships for life.”