使网络编程和保护变得更容易

从安全的web浏览器到有趣的应用程序，每一个web服务的幕后都是程序员编写的代码，这些代码经过精心编写，以确保一切都能快速、平稳、安全地运行。多年来，麻省理工学院副教授Adam Chlipala一直在幕后辛勤工作，开发工具来帮助程序员更快更容易地生成他们的代码——并证明它做了它应该做的事情。

浏览Chlipala网站上的许多出版物，你会发现一些经常重复的关键词，比如“容易”、“自动”和“证明”。他的大部分工作集中在为程序员设计简化的编程语言和应用程序制作工具，为特定任务自动生成优化算法的系统，以及自动证明用代码编写的复杂数学是正确的编译器。

“我希望能拯救很多人很多时间做无聊的重复工作,通过自动化编程工作以及减少的成本构建安全、可靠的系统,“Chlipala说,最近一个终身教授计算机科学,研究人员在实验室计算机科学与人工(权力),和头部的编程语言和验证。

Chlipala最近开发的一个系统自动生成优化的密码算法——并经过数学证明——这让程序员从一个小时又一个小时的手工编写和验证代码中解放出来。该系统现在几乎支持所有安全的谷歌Chrome通信。

但奇利帕拉的代码生成和数学证明系统可以用于广泛的应用，从防止金融交易欺诈到确保自动驾驶汽车的安全运行。他说，这样做的目的是在编码错误导致现实世界的后果之前捕捉它们。

“今天，我们只是假设在所有主要的操作系统中都会不断出现严重的安全问题。但使用正式的数学方法，我们应该能够自动地保证，这类惊喜会少得多，”他表示。“有了固定的工程预算，我们可以突然做得更多，而不会造成尴尬或危及生命的灾难。”

系统基础设施的核心

克里帕拉说，他在宾夕法尼亚州的利哈伊河谷地区长大，编程成了“我自我认同的重要组成部分”。上世纪80年代末，当克里帕拉还年轻的时候，他的父亲，一位为AT&T贝尔实验室做物理实验的研究员，教了他一些基本的编程技巧。他很快就上瘾了。

上世纪90年代末，当克里帕拉的家庭终于接入互联网时，他可以接触到各种各样的开发人员资源，这些资源帮助他钻研“更严肃的东西”，也就是设计更大、更复杂的程序。他致力于编译器——将编程语言翻译成机器可读代码的程序——和web应用程序，“当应用程序是一个前卫的主题时”。”

事实上，应用程序当时被称为“CGI脚本”。CGI是通用网关接口(Common Gateway Interface)的缩写，它是一种协议，允许程序(或“脚本”)与服务器通信。在高中时，Chlipala和一些朋友设计了CGI脚本，并在一个面向年轻程序员的在线论坛中将它们连接起来。“这是我们开始构建自己的系统基础设施的一种方式，”他表示。

作为一个狂热的电脑游戏玩家，对于一个十几岁的Chlipala来说，设计自己的游戏是合乎逻辑的事情。他的第一次尝试是用BASIC编程语言编写基于文本的冒险。后来，他用C语言设计了一款类似“街头霸王”的游戏，名为“硫磺”，以及一些模拟战斗的桌面游戏。

这对一个高中生来说是令人兴奋的事情。“但是我的心一直在系统基础设施上，比如代码编译器和为旧Windows操作系统构建帮助工具，”Chlipala说。

从那时起，Chlipala就一直在web服务的背景下工作，为开发人员构建编程基础。他笑着说:“我是从任何终端用户都感兴趣的计算机编程类型中抽象出来的几个层次。”

对现实世界的影响

2000年高中毕业后，奇利帕拉进入卡内基哈密瓜大学(Carnegie Melon University)学习计算机科学，并加入了一个编程语言编译器研究小组。2007年，他在加州大学伯克利分校(University of California at Berkeley)获得了计算机科学博士学位，他的工作重点是开发能够证明算法数学正确性的方法。

在哈佛大学获得博士后学位后，克里帕拉于2011年来到麻省理工学院，开始了他的教学生涯。他说，吸引克里帕拉到麻省理工学院的部分原因是一个“填补空白的机会，在那里没有人做我那种证明计算机系统正确性的工作”。“我喜欢从头开始创作这个主题。”

现在，测试驱动web服务和计算机系统的源代码需要大量的计算。它主要依赖于通过大量的模拟运行代码，并纠正任何捕获的错误，直到代码生成所需的输出。但是，几乎不可能在所有可能的场景中运行代码来证明它完全没有错误。

相反，Chlipala的研究小组专注于消除对这些模拟的需要，通过设计已证明的数学定理来精确捕捉给定的web服务或计算机系统应该如何工作。在此基础上，他们构建了一些算法来检查源代码是否按照该定理运行，这意味着它完全按照预期的方式运行，主要是在代码编译期间。

尽管这些方法可以应用到任何应用中，Chlipala喜欢像创业一样运营他的研究小组，鼓励学生为他们的研究项目制定具体的、实际的应用。事实上，他以前的两个学生最近加入了创业公司，从事与论文研究相关的工作。 

一名学生正在开发一个平台，让人们可以快速设计、制造和测试自己的计算机芯片。另一个是设计经过数学验证的系统，以确保驱动无人驾驶汽车系统的源代码不包含导致道路错误的错误。Chlipala说:“在无人驾驶汽车中，一个bug可能会导致撞车，而不仅仅是‘蓝屏死机’那样的撞车。”

从今年夏天到今年年底，克里帕拉一直在休长假，他把时间分别花在麻省理工学院的研究项目和自己的创业项目上。他的创业基于帮助没有编程经验的人创建高级应用程序的工具。一个这样的工具，可以让非专业人士构建日程安排应用程序，已经在他自己部门的教职员工中找到了用户。关于这家新公司，他表示:“过去几年我一直热衷于创业。但现在我有了终身职位，是时候开始了。”