Katherine Ye wants to bring more science to computer science.
Ye, a senior computer science major at Princeton University, is an advocate of formal methods, the process of using mathematical techniques to specify how software should function and to verify that it meets the specifications. In the computer science community, the use of formal methods in programming has been debated since the 1960s. They have not been widely adopted by software companies due to the perception that they require extensive training, add lengthy stages to practical software development, and are incompatible with certain software packages.
Yet the techniques, Ye says, can expose programming errors in software critical for banking, medicine, communications and voting, and could block hackers and thieves.
Katherine Ye
"A lot of people in industry and even some in academics are really skeptical of formal methods," said Ye, who is from Edison, New Jersey. "Skeptics have the impression that formal methods are useless or too academic," she said.
Ye, whom the Computing Research Association (CRA) named an Outstanding Undergraduate Researcher last December, has made it her goal to apply formal methods to real-world software. Her projects — which cut across a swath of research areas, including different programming languages and cryptography (the science of hiding information from anyone but those who are authorized to use it) — aim to help bridge the gap between academia and industry in realizing the benefits of formal analysis when searching for mistakes in computer systems.
Among these projects is joining a Princeton-led team of computer scientists funded by a $10 million, five-year grant from the National Science Foundation (NSF). The group — which is led by Andrew Appel, the Eugene Higgins Professor of Computer Science at Princeton, and includes researchers from the University of Pennsylvania, Yale University and the Massachusetts Institute of Technology — plans to use formal methods to develop tools to eliminate uncertainty from the task of software development.
"It's really exciting that the NSF has given formal methods this vote of confidence," said Ye, whose mentors include Appel and Adam Chlipala, associate professor of computer science at MIT and a principal researcher on Appel's team.
'A leadership role'
Ye's professors speak of the intellect, curiosity and love of research that led to her recognition by CRA and precocious success in a field dominated by graduate-level researchers, most of whom are men.
"Normally, we are excited when a top student successfully accomplishes one technically challenging research project, but three in one year, working on what is typically viewed as graduate-level technology… sets her apart from almost all other students that pass through Princeton," said David Walker, a professor of computer science at the University.
He added that she has "taken a significant leadership role in the computer science department" — most notably through her efforts to increase the diversity of contributors to open-source projects, or software whose source code can be modified or enhanced by anyone. Ye, who served on the board of a student organization called Princeton Women in Computer Science, said the open- source community is "even more homogenous" than the software engineering community at large, with as few as 1.5 percent of contributors being women, according to the National Center for Women and Information Technology. (At Princeton, 35 percent of seniors majoring in computer science are women.)
Inspired by a similar project at Columbia University, Ye emailed several Princeton listservs and asked for help in organizing an open-source workshop on campus, with the goal of helping students contribute to real projects and boosting diversity among open-source software developers. She received a huge response from the University community, which led to the creation of a student organization called Open Source at Princeton, for which she served as co-president with junior Lisha Ruan during her junior year.
Partnering with software education nonprofit OpenHatch and corporate sponsors such as Bloomberg, Ye and her co-organizers hosted a one-day workshop in November 2014 called Open Source Comes to Campus, which taught students about the tools and culture of open-source development. More than 30 percent of the 40 participants were women, which Ye said was higher than expected.
The student organization has continued its efforts through mentorship programs encouraging students to contribute to OpenMRS, an open-source medical records platform. It recently appointed junior David Gilhooley president, "which I think is really great because the organization can go on without me," said Ye. "It's not going to die after I graduate."
Ye traces her research interests and passion for diversifying the open-source community to the Recurse Center — a free educational retreat in New York City for programmers, where she spent the summer between her freshman and sophomore years. There, she became fascinated by new programming languages such as Haskell, which made programs that were "verbose and tricky" in other languages become "concise and beautiful." A resident at the center introduced her to the Coq proof assistant, which is an "absolutely revolutionary" system that mechanically checks mathematical proofs written by coders, said Ye.
She returned to Princeton and sought to work with Appel, who was known for using Coq in his research projects. "He really took a chance on me," she said, noting that, as an undergraduate student, she had not taken his graduate-level programming language course. Impressed that she taught herself Coq and had specific ideas about using it to write proofs, Appel assigned her to a research project when she was in her junior year, with the goal of determining whether a tool widely used in cryptography to authenticate messages on the Internet was correct and secure.
Ye's task was to prove equivalent two different formal descriptions of the cryptographic tool — "and she got it done," Appel said. "Every week she showed up to our meeting prepared —actually hyper-prepared, with an agenda and progress report emailed in advance."
Her role in the project led to co-authorship of a paper with Appel, Princeton research scholar Lennart Beringer and Adam Petcher, a doctoral candidate at Harvard University. Beringer presented the paper last year at the 24th annual USENIX Security Symposium in Washington, D.C.
Along with her research, Ye found time to deliver a talk on mathematical classifications of knots at Strange Loop 2015, a computer science conference held in St. Louis in September.
'Grad-school bound'
Ye's senior thesis aims to prove the security of a tool called a "pseudo-random number generator," which is a standard algorithm at the heart of cryptographic systems.
Her research is co-advised by Appel and cryptographer Matt Green of Johns Hopkins University. "She's coming up to speed very quickly on this, and as usual she's organized and independent," said Appel. "In this crypto-math research I'm not an expert, so she'll have to be the expert."
Appel added that her research will likely result in a conference paper submission this summer, and a placement in a top graduate school computer science program.
"From the day I met her it was clear she was grad-school bound," he said, noting that she is among the "most capable, motivated, accomplished, smart" undergraduate researchers he has advised during his 30-year research career.
Ye's goal is to continue her formal methods research as a professor of computer science and has been accepted to a number of graduate programs. As a graduate student, she expects to focus on an up-and-coming field in formal methods called "high-assurance cryptography."
"I like the field of high-assurance cryptography because it's useful in practice, has some beautiful theory behind it, and is interdisciplinary," Ye said. "I've been told that people change fields radically in grad school, so I'm open to working in any field that satisfies these three criteria."
