CybersecurityMaking it Easier to Program and Protect the Web

By Rob Matheson

Published 23 July 2019

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. MIT Professor Adam Chlipala builds tools to help programmers more quickly generate optimized, secure code.

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.”