Behind the scenes of every web service, from a secure web browser to an entertaining app, is a programmer’s code, carefully written to ensure everything runs quickly, smoothly, and securely. For years, MIT Associate Professor Adam Chlipala has been toiling away behind behind-the-scenes, developing tools to help programmers more quickly and easily generate their code — and prove it does what it’s supposed to do.
Scanning the many publications on Chlipala’s webpage, you’ll find some commonly repeated keywords, such as “easy,” “automated,” and “proof.” Much of his work centers on designing simplified programming languages and app-making tools for programmers, systems that automatically generate optimized algorithms for specific tasks, and compilers that automatically prove that the complex math written in code is correct.
“I hope to save a lot of people a lot of time doing boring repetitive work, by automating programming work as well as decreasing the cost of building secure, reliable systems,” says Chlipala, who is a recently tenured professor of computer science, a researcher in the Computer Science and Artificial Laboratory (CSAIL), and head of the Programming Languages and Verification Group.
One of Chlipala’s recent systems automatically generates optimized — and mathematically proven — cryptographic algorithms, freeing programmers from hours upon hours of manually writing and verifying code by hand. And that system is now behind nearly all secure Google Chrome communications.
But Chlipala’s code-generating and mathematical proof systems can be used for a wide range of applications, from protecting financial transactions against fraud to ensuring autonomous vehicles operate safely. The aim, he says, is catching coding errors before they lead to real-world consequences.
“Today, we just assume that there’s going to be a constant flow of serious security problems in all major operating systems. But using formal mathematical methods, we should be able to automatically guarantee there will be far fewer surprises of that kind,” he says. “With a fixed engineering budget, we can suddenly do a lot more, without causing embarrassing or life-threatening disasters.”
A heart for system infrastructure
As he was growing up in the Lehigh Valley region of Pennsylvania, programming became “an important part of my self-identity,” Chlipala says. In the late 1980s, when Chlipala was young, his father, a researcher who ran physics experiments for AT&T Bell Laboratories, taught him some basic programming skills. He quickly became hooked.
In the late 1990s, when the family finally connected to the internet, Chlipala had access to various developer resources that helped him delve “into more serious stuff,” meaning designing larger, more complex programs. He worked on compilers — programs that translate programming language into machine-readable code — and web applications, “when apps were an avant-garde subject.”
In fact, apps were then called “CGI scripts.” CGI is an acronym for Common Gateway Interface, which is a protocol that enables a program (or “script”) to talk to a server. In high school, Chlipala and some friends designed CGI scripts that connected them in an online forum for young programmers. “It was a means for us to start building our own system infrastructure,” he says.
And as an avid computer gamer, the logical thing for a teenaged Chlipala to do was design his own games. His first attempts were text-based adventures coded in the BASIC programming language. Later, in the C programming language, he designed a “Street Fighter”-like game, called Brimstone, and some simulated combat tabletop games.
It was exciting stuff for a high schooler. “But my heart was always in systems infrastructure, like code compilers and building help tools for old Windows operating systems,” Chlipala says.
From then on, Chlipala worked far in the background of web services, building the programming foundations for developers. “I’m several levels of abstraction removed from the type of computer programming that’s of any interest to any end-user,” he says, laughing.
Impact in the real world
After high school, in 2000, Chlipala enrolled at Carnegie Melon University, where he majored in computer science and got involved in a programming language compiler research group. In 2007, he earned his PhD in computer science from University of California at Berkeley, where his work focused on developing methods that can prove the mathematical correctness of algorithms.
After completing a postdoc at Harvard University, Chlipala came to MIT in 2011 to begin his teaching career. What drew Chlipala to MIT, in part, was an opportunity “to plug in a gap, where no one was doing my kind of proofs of computer systems’ correctness,” he says. “I enjoyed building that subject here from the ground up.”
Testing the source code that powers web services and computer systems today is computationally intensive. It mostly relies on running the code through tons of simulations, and correcting any caught bugs, until the code produces a desired output. But it’s nearly impossible to run the code through every possible scenario to prove it’s completely without error.
Chlipala’s research group instead focuses on eliminating the need for those simulations, by designing proven mathematical theorems that capture exactly how a given web service or computer system is supposed to behave. From that, they build algorithms that check if the source code operates according to that theorem, meaning it performs exactly how it’s supposed to, mostly during code compiling.
Even though such methods can be applied to any application, Chlipala likes to run his research group like a startup, encouraging students to target specific, practical applications for their research projects. In fact, two of his former students recently joined startups doing work connected to their thesis research.
One student is working on developing a platform that lets people rapidly design, fabricate, and test their own computer chips. Another is designing mathematical proven systems to ensure the source code powering driverless car systems doesn’t contain errors that’ll lead to mistakes on the road. “In driverless cars, a bug could literally cause a crash, not just the ‘blue-screen death’ type of a crash,” Chlipala says.
Now on sabbatical from this summer until the end of the year, Chlipala is splitting his time between MIT research projects and launching his own startup based around tools that help people without programming experience create advanced apps. One such tool, which lets nonexperts build scheduling apps, has already found users among faculty and staff in his own department. About the new company, he says: “I’ve been into entrepreneurship over the last few years. But now that I have tenure, it’s a good time to get started.”
