Recent work directed by professors Ronghui Gu and Jason Nieh introduced a new tool, Spoq, that significantly reduces the complex efforts people must use to verify real-world software and makes it possible to verify existing C systems code without modifications. Formal verification offers a systematic and rigorous approach to software and hardware verification, helping to ensure that systems behave correctly and meet their intended specifications. With Spoq, many aspects of formal verification can be automated, significantly reducing manual proof efforts for verification. The paper was presented at the 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI) Conference on July 12, 2023.

Why it matters

System software forms the software foundations of our computing infrastructure. Modern system software is large, complex, and imperfect, with vulnerabilities that can be exploited to compromise the security of a system. Formal verification offers a potential solution to this problem by mathematically proving that system software can provide critical security guarantees. Unfortunately, it remains too difficult and requires too much human effort to apply in practice.

Previous tools developed by Nieh’s and Gu’s teams introduced verification techniques to make certain proofs possible that could not have been done before. Spoq’s key feature is that it automates the tedious and time-consuming parts of many proofs. “Spoq can generate results in about an hour compared to doing it manually, which can take months or years to formally verify a system,” says Xupeng Li, the paper's lead author and a PhD student with both Nieh and Gu.

What's next

Over the next few months, the lab is focused on making Spoq open-source so that formal verification can be widely deployed to secure the foundations of our computing infrastructure's software.

About the Study

Conference: 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI) Conference (July 10-12, 2023, Boston, MA)

Title: “Spoq: Scaling Machine-Checkable Systems Verification in Coq”

Authors: Xupeng Li, Xuheng Li, Wei Qiang, Ronghui Gu, and Jason Nieh, Columbia Engineering

Funding: This work was supported in part by three Amazon Research Awards, a Guggenheim Fellowship, a VMware Systems Research Award, an NSF CAREER Award, DARPA contract N66001-21-C-4018, and NSF grants CCF-1918400, CNS-2052947, and CCF-2124080. 

COI: Ronghui Gu is the founder of and has an equity interest in CertiK.

Header image: Tang Family Assistant Professor of Computer Science Rongui Gu (left) and Professor of Computer Science Jason Nieh (right).

Over time, the AI system, which the team designed by modifying a state-of-the-art framework, got better at telling when seemingly unique fingerprints belonged to the same person and when they didn’t. The accuracy for a single pair reached 77%. When multiple pairs were presented, the accuracy shot significantly higher, potentially increasing current forensic efficiency by more than tenfold. The project, a collaboration between Hod Lipson’s Creative Machines lab at Columbia Engineering and Wenyao Xu’s Embedded Sensors and Computing lab at University at Buffalo, SUNY, was published today in Science Advances.

Study findings challenge–and surprise–forensics community

Once the team verified their results, they quickly sent the findings to a well-established forensics journal, only to receive a rejection a few months later. The anonymous expert reviewer and editor concluded that “It is well known that every fingerprint is unique,” and therefore it would not be possible to detect similarities even if the fingerprints came from the same person. 

The team did not give up. They doubled down on the lead, fed their AI system even more data, and the system kept improving. Aware of the forensics community's skepticism, the team opted to submit their manuscript to a more general audience. The paper was rejected again, but Lipson, who is the James and Sally Scapa Professor of Innovation in the Department of Mechanical Engineering and co-director of the Makerspace Facility, appealed. “I don’t normally argue editorial decisions, but this finding was too important to ignore,” he said. “If this information tips the balance, then I imagine that cold cases could be revived, and even that innocent people could be acquitted.” 

While the system’s accuracy is not sufficient to officially decide a case, it can help prioritize leads in ambiguous situations. After more back and forth, the paper was finally accepted for publication by Science Advances.

Unveiled: a new kind of forensic marker to precisely capture fingerprints

One of the sticking points was the following question: What alternative information was the AI actually using that has evaded decades of forensic analysis? After careful visualizations of the AI system’s decision process, the team concluded that the AI was using a new kind of forensic marker. 

“The AI was not using ‘minutiae,’ which are the branchings and endpoints in fingerprint ridges – the patterns used in traditional fingerprint comparison,” said Guo, who began the study as a first-year student at Columbia Engineering in 2021. “Instead, it was using something else, related to the angles and curvatures of the swirls and loops in the center of the fingerprint.” 

Columbia Engineering senior Aniv Ray and PhD student Judah Goldfeder, who helped analyze the data, noted that their results are just the beginning. “Just imagine how well this will perform once it’s trained on millions, instead of thousands of fingerprints,” said Ray.

A need for broader datasets

The team is aware of potential biases in the data. The authors present evidence that indicates that the AI performs similarly across genders and races, where samples were available. However, they note, more careful validation needs to be done using datasets with broader coverage if this technique is to be used in practice.

Transformative potential of AI in a well-established field

This discovery is an example of more surprising things to come from AI, notes Lipson. “Many people think that AI cannot really make new discoveries–that it just regurgitates knowledge,” he said. “But this research is an example of how even a fairly simple AI, given a fairly plain dataset that the research community has had lying around for years, can provide insights that have eluded experts for decades.” 

He added, “Even more exciting is the fact that an undergraduate student, with no background in forensics whatsoever, can use AI to successfully challenge a widely held belief of an entire field. We are about to experience an explosion of AI-led scientific discovery by non-experts, and the expert community, including academia, needs to get ready.”

About the Study

Journal: Science Advances

Title: Unveiling Intra-Person Fingerprint Similarity via Deep Contrastive Learning

Authors: Gabe Guo, Aniv Ray, Judah Goldfeder, and Hod Lipson, Columbia Engineering; Miles Izydorczak, Tufts University; and Wenyao Xu, University at Buffalo, SUNY.

The work is part of a joint University of Washington, Columbia, and Harvard NSF AI Institute for Dynamical Systems, aimed to accelerate scientific discovery using AI.

Funding: The study was supported by NSF AI Institute for Dynamical Systems 2112085, and NSF REU Site 2050910.

COI: The authors declare no financial or other conflicts of interest.

Blockchains and the applications they support raise new challenges for economics, computer science, and game theory.

At the 2023 Columbia CryptoEconomics (CCE) Workshop, held December 6-7, practitioners, researchers, and academics gathered at the University’s Manhattanville campus to discuss challenges, recent progress, and opportunities in the economics of blockchain protocols. In keynote presentations, contributed talks, and panel discussions, leading experts discussed topics including proposer-builder separation, MEV, layer 1 security rehypothecation/restaking, and roll-ups.

The workshop, which was co-hosted by the Briger Family Digital Finance Lab at Columbia Business School, Columbia Engineering, and the Ethereum Foundation, underscored Columbia’s commitment to interdisciplinary research that seeks impact beyond the walls of the University. 

“We advocate for the convergent collaboration among academics, practitioners, and industry,” said Shih-Fu Chang, dean of Columbia Engineering and Morris A. and Alma Schapiro Professor of Engineering, in his opening remarks. 

“As interest in the crypto space waxes and wanes, support at various universities has come and gone,” said co-organizer Tim Roughgarden, professor of computer science at Columbia Engineering and the head of research at a16z Crypto. “Columbia has been fairly unique among its peer institutions by having unflagging support for the advancement of this technology and the science behind it.”

Details about the event and a full lineup are available here.

Full recordings of all sessions are available here.

How do you think this will benefit Columbia researchers? 

This is going to infuse lots of energy into our current collaborations. And I think it will spark even more. We have an amazing engineering school and an amazing medical center at Columbia, and we’ve built many long-standing relationships between engineering and medicine. So I think the Biden initiative will give a big boost to the many projects we’re already working on as well as inspire new groundbreaking ones. It's going to rejuvenate the field and encourage the amazing women's health researchers that we already have here to go even bigger. And it will be great for our junior faculty members to come on board and adapt their engineering tools for improving women's health research. 

We have an extraordinary group of researchers working in women’s health here. I’ve been at Columbia Engineering for more than 13 years and have been working very closely with Electrical Engineering Associate Professor Christine Hendon to use imaging to assess the mechanical properties of the cervix in relation to preterm birth. We are also collaborating with Noémie Elhadad, Biomedical Informatics and Department Chair at Columbia’s Vagelos College of Physicians and Surgeons. The core group of engineers and doctors have been working together for many years on women's health, gynecologic health, and pregnancy, using imaging, data, and computational simulations to build a bank of fundamental research that we can draw upon to design new techniques and devices to improve women’s health. Columbia has a community of very dedicated researchers who’ve been around for quite a while, but we've all been plagued by small funding pools. So this initiative will be huge both for us and for all the startups that are looking for funding -- they need fundamental research and financial backing to develop their new products.

How do you see this having an impact on your own work?

We are one of the first groups in the world to take maternal anatomy measurements throughout pregnancy, working with patients in a clinical trial at Columbia University Irving Medical Center (CUIMC) and then creating a digital twin of that individual pregnancy to understand how much mechanical load is on the uterus in the cervix and what might lead to a preterm birth. I'm a mechanical engineer and study design, practice design, and teach design to students, so I’m always looking at materials and wondering about their mechanical properties. When I was pregnant eight years ago, I lay there on the examining table, thinking “Hey, can I just spend five more minutes with this ultrasound and measure key anatomical features of me, the mom?” So that’s what we did. We started a clinical study in 2019 and our last patient in the study delivered last May.

President Biden’s announcement is really bringing awareness to the synergies that we researchers all have in women's health, engineering, research, and innovation. One of the interesting things resulting from this increased awareness of women’s health is the fact that the NIH issued a policy less than 10 years ago that states that sex as a biological variable must be factored into research designs, analyses, and reporting in vertebrate animal and human studies. Now you can't study only male monkeys, rodents, etc., which is a really important direction, especially in gynecologic health. In the past, many women’s symptoms such as uterine pain or heavy menstrual bleeding were dismissed -- people just thought of these as a normal part of life, that they didn’t indicate disease. But if we had more basic research data, we would have a much better idea of what healthy physiological functioning looks like, of what really is “normal.”

So I need more colleagues -- I can’t do it all myself. Everytime I fund a graduate student, I'm creating a new researcher in this field and increasing the pipeline. It’s critical for researchers like me to educate the next generation of engineers to solve these problems. And I'm excited about this announcement because my future trainees, my grad students, will read about this in the news and say, “Hey, I want to be in this field, and I can easily adapt what I'm already doing at the bench and work to improve women's health.

Image

Tell us about your journey from engineering into women’s health and how you decided to focus on the cervix.

I started off as a traditional mechanical engineer in the automotive industry, where I did research projects on things like exploding tires, thinking about how rubber heats and degrades. Once I got to graduate school as a young woman at MIT, I wanted to differentiate myself. I wanted to work on a project that was meaningful to me as an engineer, and I was introduced to the pregnancy mechanics project. This was an easy jump for me because the great thing about engineering is that we learn tools to solve problems. And in this case, I learned about structural mechanics. I was using the same analysis, tools, and material equations to think about how the cervix changes its material properties when exposed to the hormones of pregnancy. This is the work that my NSF Early Career grant was on, and I won the PECASE award for my research on exploring material mechanics of materials and the cervix, and how the cervix remodels itself. The cervix is analogous to rubber, with elastomers heating, degrading, and potentially breaking and becoming catastrophic. 

Working on the cervix and preterm birth issues with my colleagues at Columbia, we ran clinical studies on pregnant women who were eager to participate. Once we got the data from our studies, we made a digital twin by replicating the uterus virtually on the computer. We then ran simulated experiments on the computer to see what might happen under varying conditions. This is much more complicated than it sounds because the human body is really complex and there are so many things we still don’t know. This work will probably take my whole career because I'll keep improving my models with discoveries I make at the biological level with my collaborators. For instance, I’m working with a molecular biologist at the University of Texas Southwestern Medical Center in Dallas to understand the biology of tissue remodeling and I’m trying to figure out what the environmental triggers for that remodeling are. Over the last five years, I’ve integrated factors into my models such as anatomy shape and size, or structural anatomy and tissue material properties. We’ve actually done the measurements and taken the data of how the uterus and the cervix physically deform -- in fact, we’re the only team in the world with this kind of data.

Where will this data take your research next? What’s in store for the future? 

I now have a new hypothesis that we’ll be presenting at a conference in February. My group is going retrospectively into the imaging database at CUIMC in partnership with Mount Sinai, and we're planning to use AI to read all the ultrasounds of pregnancy to pick out a key anatomical feature that might lead to preterm birth. It’s great because we can test our hypothesis because the imaging database also has clinical outcomes -- this is where the AI and bioinformatics work comes in. Then we hope to create digital twins of phenotypes that are related to preterm birth. If we have a phenotype that's related to preterm birth based on this retrospective database, I can design a new therapeutic or a device to structurally bolster the cervix. 

I hope that in five years we'll have new diagnostic and therapeutic innovations and that our work will be translational. I want to reiterate that I can’t get there without first taking the data. I needed the observational study because nobody's measured these features before -- this is why fundamental research is so critical.

I want to lower the barrier of entry for engineers to work in the women's health and pregnancy space. I feel privileged that I have a longstanding relationship with a top-tiered research ob/gyn department and I want to bring more people into the field. The only way to do that is to open source and release all of our raw data sets, all of our models, and all of our model byproducts. 

Is this a long time coming?

Yes!