11月1日第七届二十一世纪的计算学术研讨会在浙江省人民大会堂举行，国际著名的计算机大师，包括图灵奖获得者，美国国家工程院院士以及美国国家科学院院士等多位科学家莅临大会。本次会议由国家自然科学基金委员会、Microsoft亚洲研究院、杭州市人民政府以及浙江大学联合举办。今天到场演讲的八位嘉宾分别是Rick Rashid、Ronald L.Rivest、Jeannette Wing、Alexander Gounares、Harry Shum、Stanley Osher、Daniel T.ling、Eugene Fiume。

新浪网对此次研讨会进行了全程图文直播，同时新浪还将对其中的几位著名学者进行在线访谈，欢迎各位网友届时参加。

洪小文：各位尊敬的领导、各位来宾、各位同学，大家早上好！很高兴第七届“二十一世纪的计算”学术研讨会能够在浙江省省会美丽的天堂城市杭州市隆重召开，这是有使以来，我们这个会议第一次将主会场放在北京以外的地方来举行。今天大会探讨的主题是无“数”不在的计算，个人电脑、互联网上数据无处不在，将原始的数据处理为有用的咨询。以数据为核心的计算正在改变全球数亿用户的体验。很高兴我们今天邀请了八位著名的学者，与我们共同探讨无“数”不在的计算。今天的安排分成上下午两部分，各有四位演讲人，在四位演讲报告之后我们有一个综合的现场提问，今天的提问环节除了传统的现场提问外，我们还提供了手机SMS的方式，你可以将问题发送到现在屏幕上方所显示的手机号码上面。今天我们很荣幸请到了浙江省、杭州市、浙江大学的多位领导莅临大会，首先有请浙江省副生长茅临生先生为大会致欢迎辞。

茅临生：各位来宾、女士们、先生们，今天“二十一世纪的计算”学术研讨会隆重开幕了，这是中外计算机科学研究专家云集的一次高层次学术研讨盛会，在此我谨代表浙江省人民政府表示热烈的祝贺！向各位科学家，及所有出席本次大会的国内外嘉宾表示诚挚的欢迎！

浙江省为中国东部沿海长江三角洲，全省陆地面积10.18万平方公里，海域和专属区面积26万平方公里，全省有两个副省级城市，9个地级市，改革开放以来在党中央国务院的正确领导下，我省各级党委政府组织带领全省人民发扬自强不息、坚韧不拔、勇于创新、讲究时效的浙江精神，经济、社会等各项事业都取得了各项成绩。自78年到2004年我省GDP年均增长超过10%，去年GDP总量超过1350亿美元，人均900美元，位居全国第四，仅次于上海、北京、天津，列省第一位，全国最具活力的省份之一。当前，全省当下继续以科学发展观为指导，抓紧实施推进全面建设小康社会，提前基本实现现代化建设。近年来，浙江省认真实施科教强省战略，大力发展信息产业，成为中国电子信息产业发展速度最快的地区之一。今天召开了“二十一世纪的计算”学术研讨会是计算科学领域一年一度的盛世，是中外计算机科学专家交流思想的舞台，通过此次研讨会，我希望我省计算机领域的科研人员和相关企业能够进一步掌握计算机发展趋势，了解科学计算前沿领域，提高思维创新能力。也衷心祝愿本次研讨会能够在计算领域有新的发现、新的突破，为人类文明做出应有的贡献。最后，预祝“二十一世纪的计算”学术研讨会圆满成功，祝各位身体健康、万事如意，谢谢！

洪小文：谢谢茅副生长。接下来有请杭州市副市长沈坚先生为我们致辞。

沈坚：尊敬的大会主席，各位领导、各位专家、各位来宾，女士们、先生们，大家上午好！今天计算机领域的世界一流专家学者齐聚美丽的西子湖畔，隆重举行“二十一世纪的计算”大型国际学术研讨会，借此机会，首先请允许我代表杭州市人民政府向远道而来的各位尊贵的嘉宾，向本次活动的主办方——Microsoft亚洲研究院、国家自然科学基金委员会、浙江大学，向出席今天会议的所有专家和来宾表示热烈的欢迎和衷心的感谢！

前唐自古繁华，杭州是一座美丽的历史文化名城和著名的风景旅游城市，古往今来人才荟萃，具有深厚的科技文化底蕴和发展潜力，近年来杭州的经济、社会进入了快速发展的阶段，国民经济始终保持较快的增长，综合实力不断增强，对外开放的步伐迈得更大，城市环境不断优化。近年来，杭州先后荣获联合国人居奖、国际花园城市等荣誉称号，被世界银行评为中国城市投资环境的最佳城市第一名，被福布斯评为2004年度中国大陆最佳商业城市排行榜第一名。

作为全国最重要的信息产业基地之一，杭州致力于打造天堂硅谷，一直以来和Microsoft公司有着良好的合作关系。2003年杭州市政府与Microsoft中国有限公司签订了关于共同促进杭州软件产业的合作备忘录，2004年杭州高新技术产业开发区与Microsoft中国有限公司签署了相关合作协议。近年来，Microsoft公司积极参与并支持杭州市信息产业的快速发展，协助杭州软件业打响杭产软件品牌，加速了杭州信息产业界同国际主流厂商的交流合作，有利地促进了我市信息产业的不断做强做大。

今天，“二十一世纪的计算”学术研讨会首次选择北京之外的城市，选择了杭州，作为大会的主会场，这是杭州的荣幸和杭州的骄傲，举办这次学术界的盛会必将开辟杭州市企业高效与世界著名的IT企业合作的新局面，将进一步推动我市信息技术发展和人才的培养，促进杭州的信息产业发展。我相信杭州市与Microsoft双方的合作必将取得丰硕的成果。最后，预祝“二十一世纪的计算”学术研讨会取得圆满成功，祝各位身体健康、生活愉快、万事如意，谢谢大家！

洪小文：谢谢沈副市长。接下来有请浙江大学常务副校长倪明江先生致辞。

倪明江：尊敬的各位领导，各位嘉宾同仁，女士们，先生们，上午好！由Microsoft亚洲研究院、国家自然科学基金委员会、杭州市政府和浙江大学联合主办的、杭州市科技局协办的第七届“二十一世纪的计算”在杭州召开，在此我谨代表浙江大学欢迎出席会议的各位领导、各位同仁和朋友。Microsoft亚洲研究院自成立以来，在短短的七年时间里取得了骄人的业绩，在从事前沿研究工作的同时，Microsoft亚洲研究院还广泛开展与国内高等院校科研机构的合作，对中国的计算机学科的发展起到了积极的作用。“二十一世纪的计算”研讨会更被媒体誉为中国计算科学研究领域水平最高的学术会议。计算机科学与技术是浙江大学重点发展的领域之一，浙江大学计算机学科自1978年成立以来发展迅速、成绩斐然，在第二轮的国家重点学科综合评比中，浙江大学计算机应用学科以综合实力满分的佳绩获得通过。长期以来，Microsoft和浙江大学开展了各种形式的交流与合作，共同致力于推动计算机科学与技术的发展、人才的培养和学术交流。1999年7月19日，Microsoft亚洲研究院、浙江大学计算机学院联合成立了浙江大学Microsoft视觉感知联合实验室，并于2004年成为教育部Microsoft重点实验室，这也是Microsoft中国研究院在中国设立的第一个联盟。今天我们很高兴迎来了“二十一世纪的计算”大会在杭州召开，这是计算机学界的一次盛会，也将开辟浙江省高校与IT企业合作的新局面，推动国内IT人才培养体系的进一步完善。在此我谨代表浙江大学对出席本次大会的嘉宾，图灵奖获得者Ronald L.Rivest，Microsoft公司高级副总裁Rick Rashid，Microsoft公司亚洲研究院院长沈向洋博士表示热烈的欢迎，对出席和参加这次大会的所有来宾表示诚挚的谢意。我相信会议在杭州的成功举办必将为杭州的计算机产业发展注入新的活力，也将吸引和培养更多优秀的计算机专业人才。最后我预祝这次学术研讨会取得圆满成功，谢谢！

洪小文：谢谢倪副校长。现在有请Microsoft亚洲研究院院长沈向洋博士致答谢辞。

沈向洋：尊敬的茅省长、沈市长、倪校长，各位老师、各位同学，各位来宾，大家早上好！首先请允许我对于各位的到来表示热烈的欢迎，特别是对于远道而来的讲者表示热烈的欢迎，昨天我带他们其中的一部分在杭州看了一下，他们对于西湖美丽的感叹非常多。“二十一世纪的计算”学术研讨会举办至今已经第七届了，每一年在每个城市举办“二十一世纪的计算”大会都无一例外地得到了各地同学们的欢迎和各地领导的大力支持，这是大会取得圆满成功的保证，此外我们每年邀请到了图灵奖获得者、诺贝尔奖获得者以及计算机方面的科学家与各位探讨“二十一世纪的计算”资源，也被同学们称为世界顶级的脑力盛宴。“二十一世纪的计算”第七届来到美丽的杭州，从策划初期就得到了浙江大学、杭州市政府、浙江省政府的倾力支持，在此请允许我对于浙江省领导、杭州市领导、浙江大学领导、杭州市科技局的大力支持表示衷心的感谢！再次预祝大会圆满成功，谢谢大家！

接下来我为他们介绍第一位出厂的演讲嘉宾，也是我的老板，Rick Rashid博士，通常介绍自己的老板时要小心一点，讲错了话回去很可能会有问题。介绍Rick Rashid我非常有信心，以前他是我的老师，现在是我的老板，Rick Rashid是Microsoft全球研究院的高级副总裁，当时在西雅图Rick Rashid受Bill Gates的委托成立Microsoft研究院，现在Microsoft已经有很多研究院，硅谷研究院、西雅图研究院、剑桥研究院、中国研究院、印度研究院等等。Rick Rashid在学术领域享有很高的声誉，Rick Rashid也曾经是美国国防部高级研究计划局UNIX指导委员会的委员。Rick Rashid有一个兴趣也是大家都知道的，他在工作之余比较喜欢写游戏，在今天他的演讲当中也会告诉我们自己怎么样在偷偷摸摸地写了很多游戏。

下面有请Rick Rashid博士。

Rick Rashid：对浙江大学的盛情款待和城市的美景以及友好热情非常感谢，而且对我来说有非常好的机会，今天想一下对今后的评估，那就是期待着未来，思索一下如何为我们所有人创造更加美好的未来。还有就是投资于技术研究是如何重要。

现在我想回顾一下90年代的时候，在1990年的时候贝肯，他是Microsoft前首席执行官给Bill Gates写了一封信，建议Microsoft成立一个研究机构。今天从Microsoft的角度来说并不是很难做的事情，今天Microsoft已经有400多亿美元的销售额，但是在2000年的时候Microsoft不是会做基础研究的公司。90年的时候销售额刚刚达到10亿美元，而且只有5000名员工，我们的产品也很单一，主要是在零售一些产品。

这是一张图，可以看一下当时的时候我们Microsoft的工作场所非常小。91年在这种氛围下创立了Microsoft研究院。我在91年加入Microsoft公司，开始赌未来，我的目的是要在新的行业里面建立一种新形式的基础研究实验室。Microsoft研究所实验室对我来说是非常令人振奋的概念，因为这是首次由软件公司建立的实验室，是真正做计算机科学的公司。当我创立了Microsoft研究院之后我有个非常简单的使命宣言，就是扩大我们研究的艺术。这里没有讲到Microsoft公司，使命宣言是关于科学、关于研究的使命宣言，还有是改变研究如何影响到人们生活的这样一种使命宣言。当进行了伟大的研究之后，你想把这个研究成果迅速地投向社会，所以我们使命宣言的第二部分就是要把我们的技术尽快变成产品。我想这里关键的事情是你要把研究成果转换成产品，你不是在现有的产品基础上做研究，所以你现在要把创新的成果真正付诸到实际的成果中。在创立Microsoft研究院的时候，正像我所来自的学校梅隆大学的计算机系，我们有非常简单的组织架构，开放的研究氛围对我来说是非常重要的，而且大量出版学术文章和进行学术评论是很重要的，因为你的研究没有经过同事的评论就不能确保在这个领域取得进展，所以很多成果要获得学者的评论和研究。在今年夏天，Microsoft研究院有200多名实习生，美国每年只有1000名计算机博士毕业生，有200多名美国的研究生一直在Microsoft做实习生，在全球范围内大概有600名，在北京大概有300多名计算机系的博士生去Microsoft研究院，这样就可以了解到Microsoft研究院的成长速度。我是14年前做的这种预测，今天的演变以及我们对此做出的反应，我们有6个实验室，最近我们在印度新开了实验室，有700多名人员在45个不同的实验室工作。许多人从介绍材料里面都看到，我们被许多人认为是世界上领先的实验室之一，这是去年专门介绍北京实验室的情况，说是世界上最有潜力最前端的实验室，我们努力实施我们的第一个使命宣言，就是扩大我们的计算艺术。你如果看一下高级研讨会里面提交的研究文章比任何一个机构和公司都多，我在幻灯片里面提出了这几点，通过不同的研讨会你会发现Microsoft的研究人员发挥的作用有的时候起到的是主导作用。

另外我们也正在实现驱动产品创新的使命，我想突出地讲几件事情，Microsoft的研究的确改变了Microsoft公司的形象。当人们讲到基本研究机构的时候，他们经常说你为什么要基础研究这种机构，它的重要性在哪里。有很多各种不同的方式来思索一下基础研究机构的价值，对像Microsoft公司这样机构的价值，当然这是一种知识产权的来源还有新产品技术的源泉。如果我们看一下专利的情况，Microsoft25%的专利都是来自于研究院，而且是这些基础的研究所产生的，我们当然是一个解决问题的机构，经常产品的调研机构会出现问题，或者我们看到这些问题需要解决这些问题，我们有世界上最聪明的一些人能够解决这些问题。而且我们有早期预警系统，对公司来说，我们的研究人员经常从一些没有参与的角度做研究，我们都是不断展望未来，我们与世界上的学术界密切合作，所以一般来说我们经常是结果对公司有影响之前能够做出坦率的预测。对于基础研究来说，无论是大学来做还是Microsoft公司的实验室来做也好，我想都是提供一种可变性、灵活性，Microsoft研究院能够使得Microsoft对世界发生的变化迅速做出反对，无论是商业变化也好，还是竞争对手变化也好，或者是主要技术的变化，或者是商业模式的变化也好。我们的研究人员已经在这个领域工作了一段时间，他们提供了一系列的技术和专长，还有人才，这样的话Microsoft公司能够在变革时期依赖这些资源，所以我认为这对我们来说是非常重要的部分。

我现在简要一下对于未来的赌博这几年来进展如何，我想讲一下Microsoft的研究对Microsoft公司还有全世界所产生的变化和发生的影响，我现在讲一下我们的预测究竟现状如何。

Microsoft研究院所涉及的另外一个领域是创立理念，这些理念形成新的服务和产品。讲话之前我发现我在1993年使用的这些老的幻灯片，当时讲到口袋PC理念的时候，这与今天的终端看上去没什么不一样，像PDA、手机等等都差不多，我今天所携带的手机与93年我所持手机的终端没什么区别。我们想形成这样一种环境，在这个环境里面Microsoft公司能够开发新的产品，可以在投入到市场之前就开始研究一些前端性的产品。

剑桥实验室在90年代的时候，切克是创始人之一，他提出了这样一个想法，Tablet PC，他把Sony的电脑切成一半，里面放上数字化的服务，再加上软件，这些软件成了Tablet PC的提出。切克回来回到美国，所有的Tablet PC的关键技术都是来自于我们实验室的成果，从北京、剑桥、温布顿实验室的研究成果。这是93年我当时建立互动团组研究PC，我们有这样一个想法，在网络上面传送互动式电视信号，93年开始我们成立了一个研究小组，到94年的时候我们已经配置了光纤传送网络的提供，很多人可以通过IP提供互动PC。

这是94年时候的幻灯片，这是非常现代化的系统，这与今天我们所建立的互动性系统一样，这是我们称之为Tiger的互动视频流程技术，Tiger是自我组合的系统，能够通过光纤网络支持大的同步视频流程和音频。这样一项工作在当时的环境下我们并没有从商业角度把它确定为一种目标，96年的时候当时世界上并没有准备好接受这些技术，当时我们的研究、我们建立的系统、我们培训的人才显然对Microsoft这么多年来产生了巨大的影响。

我们成立了一个数字媒体部门，它在93年的时候前身是非常小的研究小组，96年进行了扩大，之后不断壮大发展，Microsoft的很多音频视频产生的关键技术都是来自于早期的比如WMA、WMV的产品和技术。我们当时的图像研究技术和设计技术最终成为开发原来XBOX的技术。

在互动性TV这么多年来技术一直在不断改善，现在Microsoft在开发互动TV软件方面已经领先，现在开始在欧洲和美国部属。短的录像片可以看到我们如何迅速从一个频道转换到另外一个频道，今后在实际生活中人们的家庭看上去没什么不一样，但这是Microsoft员工卧室的一个照片，真正发生的事情，任何终端可以变成互动性的表面终端，数字化的LCD的TV与今天的白板相比成本也降低很多，所以我们真正从被动的表面变成互动的表面。这是一个例子，我们的研究院正在调查和研究任何一种表面都可以成为互动式的表面终端，通过投射技术和实时跟踪技术，你可以很简单地把一张桌子变成互动性的表面，你可以玩游戏，你可以提供各种各样的应用，你也可以把一些有形的物质放在桌面上，产生这种虚拟的形式。或者你把一张纸放在桌面上，突然间成为视频区，这样就可以播放视频。

这些例子可以说明我们通过实验室的研究不断研究新的终端和新的技术。我们在学术界也起很重要的作用，在计算机学科领域来讲。比如说图形设计，图形设计方面的研究我们Microsoft亚洲研究院做了很多工作，这么多年来我们比世界上任何一个研究院相比文章都要多，我们不断成为这个领域的领先者，在去年图形方面10%的文章都是来源于Microsoft亚洲研究院，20%是Microsoft的。

现在大家看一下我们这些年开发的技术，有的技术是上个世纪90年代中期。比如说我们可以看到很多的3D工作成果，大家可以看一下，实时的程序结合，还有所谓预计算的照射。大家可以看到，这里是在03年和04年间的情况，大家不必尝试去看文字，我只是让大家了解一下我们这个组织和活动。对公司很多方面会产生影响，这是我们在剑桥研究的一个工作成果，我们把这些研究成果得到应用。居家活动很典型会照成这样，有些人都会照得不错，但是总是会有一个人没上镜头，或者表情比较奇怪，或者不希望照成这个样子，比如说这个人是比较对的，这个人看上去不太好，这次是老奶奶没朝这边看，大家可以看到不同的图像情况，还有小孩在大哈欠，大家实际上是想照这样一个虚拟的照片，把好的照片拿过来，把不好的照片去掉，这是一个虚拟的照片，谁也没有真正照过这个照片，但是经过我们制造以后就达到了很好的效果，通过很多张照片组成了这样一个照片。我们在这里做的工作对Microsoft有了巨大的影响，促进了商业的发展。这是我们在游戏方面广泛使用的技术，而且改进了商业在家里的具体应用。这是在美国再过三周即将推出的游戏赛车第三版，这是Kameo，现在大家可以了解一下图形有什么变化，更多的图形技术都产品化了。

我们不仅仅在图形方面工作，而且我们在一些最基本的计算机科学中也做了很多工作。追溯到1992年，我们进行了一些程序的优化，92年时我们推出了LEGO系统，后来这个名字改变了，因为LEGO公司不喜欢他们的名字作为我们的代号，这个系统在92年的时候有了很大的改善，也就是我们可以把Office95和Windows95同时推出，这使得我们的32位技术领先于我们的竞争对手。

在过去几年中，Microsoft在建立新的工具软件分析方面取得了很大的进展，我们在开发这些工具使用这些工具方面引领着业界的发展。其中一个叫PREfix，是帮助我们分析的一个工具，可以帮助我们找到很多的程序错误，我们在Windows2000发布的时候就开始使用。大家可以看到，在这种软件分析中能够看到什么样类型的错误。这是建模的工具，可以帮助我们找到很多的开发当中的错误。我们一开始做的系统叫做SLAM，用C或者C＋＋程序，如果有足够的数学模型的话，我们可以使这个系统证明它的特性是正确的还是错误的，因为这里的代码很多。这是SLAM的流程，一开始有些具体的规则，你要印证一下到底是真实的还是错误的，实际上你们就是创造了一个所谓叫二元的东西。这是我们在开发软件的时候不断考虑的问题，这是规则。

这个改变了我们开发软件的方式，现在有很大的程序特性，我们可以证明它是正确的还是错误的。这个技术推出的第一个产品叫做竞赛的驱动的验证性，这个代码可以来印证一下我们确定的关键特性。使用同样的技术来印证一下并行计划，叫做KISS系统，基本上他们采取的就是SLAM的技术，把它放在并行的程序中，以了解程序是怎么样的情况。

在这个问题中我们重新对这个问题进行考虑，有了证明技术之后我们可以证明很多的代码、这改变了我们自上而下建立这个系统的思维方式。在我们所有的研究小组中，北京研究院、剑桥和在硅谷都是一样的，建立一个新的操作系统流程的时候，作为一个证明技术，是一个非常关键的软件设计的组成部分。

这次讲的主题叫做无“数”不在的计算，我们做了很多研究，也讲到了我们所谓的无“数”不在的计算，不仅仅是Microsoft，还有更广泛的研究界，不仅仅是计算机科学，还有很多其他科学也在考虑这个问题。98年的时候，思科研究院开发了这样一个服务器Terraserver，它第一次把地球图像放在服务器中，最终它可以不断发展，它变得越来越重要，最终变成了这么一个城镇化的东西，我们叫做虚拟地球。左手这张图是我住的地方，98年可以看到这张图，这是Terraserver 1998年照的，当时没有太多的建筑物，都是森林。右手就是虚拟地球现在的发展，大家可以看到我的屋子是在中间，实际上我们做了一些土建工程，有一些建筑工程在进行当中。这是比较大的西雅图的一张图，大家可以看到它的解析度非常高，不仅仅可以让大家获得图形的数据，还可以提供其他的信息，比如说路的名称或者是纪念碑的名称都可以加进去。Terraserver的目的就是要把信息提供给人们，使他们获得以往没有的信息。几年前把这个东西拿到了学术界，甚至是天文界，向外探的Skyserver，也就是建立一个虚拟的观象台，使科学家24小时都可以看观象台的情况，无论他在世界什么地方。Skyserver现在包含很多信息，Skyserver有它自己的网站，大家可以去看一下。如果看这个网站大家可以了解到，这些信息可以用到不同的目的中，比如说一个外行人可以到网上去看一些非常漂亮的图像，这是世界上的那些望远镜看到的天象，同时科学家看到同样信息的时候可以通过链接找到所有的文章或者是文章的缩略来了解到天文现象，科学家可以了解到相关的信息，可以就这些信息方面做一些数据的挖掘。因为以前都是不同的计算机方式来读取信息的，现在一种统一的方式就可以做到了，它都是同样数据的模式，而且是同样的编程。

这也是我们Microsoft研究院的成果，学生可以上这个网站，这都是哈勃发现的信息。大家可以看到很多数据来自天文台，这是一个数据网格，如果到IOVA.NET这个网站去就可以获得很好的数据源。有一个SkyQuery这么一个门户站点对数据进行挖掘，可以针对不同的数据档案进行挖掘，这个数字在不断增加。我们跟美国的信息中心进行合作，还有国家的医疗机构、图书馆以及政府，很多合作都是这样一种方式来联系。

我们讲无“数”不在的世界的时候，必须解决一个关键问题，我们的算法对科学家和其他人思考问题方式的影响。计算科学确实解决了差异的问题，我们的研究人员做的事情，生物问题、生理问题，比如说艾滋病病毒的问题，是不是可以看到疫苗能够很好地解决艾滋病病毒，现在全球有400万人在受到艾滋病病毒的侵害，在华盛顿大学医学院等地方认识到，艾滋病病毒很多问题和计算机科学面临的问题很相似。艾滋病病毒面临的问题它是一种不断变异的病毒，所以很难袭击这些病毒，因为它们不断变种。

还有一个问题，解决垃圾邮件的问题。在这些方面总有人跟我们做斗争，垃圾邮件总是想逃避我们的探测。

我们使用技术，包括机器学习方式，或者有效地管理以后的电子邮件情况，找到一些特点。可以看到，这些邮件可能并不是给你一个人发的，可能是给数百万人发的，我们这里是要解决垃圾邮件的问题，我们要了解这些规律，隔离那些不好的邮件。谈到艾子病毒的时候，其实也是这样，按照它的蛋白质顺序进行隔离是一样的道理。有研究人员发现，计算机科学和技术，大家可以看到，有很多人能够一眼看出来，找到这些问题，用它的这种能力来解决艾滋病的问题，因为它经过很多变种的情况。大家可以看一下次序的情况，看这个问题，找到关键的蛋白质次序，可以认识到很多不同的艾滋病毒的情况。

14年前我们压了一个宝，建立研究院，可能公司认为没有必要，但是我们认为要建立一个开放的环境，跟更广泛的研究界合作，确实在多方面获得了丰富的成果，在产品方面，在市场敏感性方面，我们使我们的公司蓬勃发展，而且改变了人们做研究的思维方式。我觉得越来越多的情况下更多人在考虑Microsoft研究院作为他们的一个范例和榜样。我们展望未来，再次做出这种承诺，不断在未来进行投资，甚至是大大提高我们的投资力度，我们计划发展在未来一年半到两年当中使我们的研究组织发展速度超过我们的历史上任何时期。我们发展的规模差不多相当于四个大学计算机科学系的规模，最近我宣布建立北京的技术中心，这是在亚洲研究院的框架之下解决很多主体信息的问题，我们不仅仅要重要做出承诺来做内部的研究，而且我们重新做的承诺要使他的研究跨入我们研究院之外，使更多的人力和能力投到全球学术界中间去。

今年早些时候我们在日本建立了学术中心，我们也更加支持在中国的研究工作。去年我们的五个联合实验室成了政府的重点实验室，我们继续在中国以及在中国学术系统的未来方面开展投资。

最后，我想对你们学生说几句，这对你们来说也是今后下赌注的机会，计算机科学也是你们可以参与的最令人兴奋的领域之一，不管你是不是本身已经是计算机科学家，或者是在其他方面工作，在计算机科学方面寻找新的想法、新的技术也好，都是这样的，因此鼓励你们继续为未来工作，鼓励你们继续工作，以便通过你所说的研究创造更好的世界。

洪小文：谢谢Rick Rashid博士精采的演讲，下一位演讲者是图灵奖获得者Ronald L.Rivest博士，他也是美国国家科学院院士。Ronald L.Rivest博士是MIT电子和信息科学系讲座教授，他在MIT智能实验信息安全研究。Ronald L.Rivest教授1969年从耶鲁大学获得学士学位，1977年从斯坦福大学获得计算机博士学位。Ronald L.Rivest教授主要从事密码安全、计算机安全算法的研究，他发明了ISA KEY的算法，这个算法在信息安全中获得最大的突破，这个成果也使他在2002年得到图灵奖。他现在担任国家密码学会的负责人。他今天要给我们演讲的题目是在二十一世纪网上上投票的新趋势。

Ronald L.Rivest：早上好，谢谢你们，我到这里来能够感受到空气当中令人兴奋的气氛，这是一个美丽的特别是看着这么多的学生在场我感到特别高兴和兴奋，我也要感谢Microsoft、感谢中国地方政府，感谢你们提供了这么好的会场，这么好的会议，我今天要讲的题目就是二十一世纪的表决或者是投票，这是我最近研究的话题，就是怎么样把票投好，组织好投票的技术，这是我研究的问题。这是本地省市开会的地方，开会的时候如果你参会的话每个人面前是一个投票机，是否同意还是弃权，也可以表决。我对于学生的话题格外感兴趣，对于学生来说，喜欢研究计算机的安全以及人机界面，以及把安全和人机界面问题搞好，用三个不同的做法来解决安全的问题，认证、审计、加密、表决系统等等。

表决就要考虑安全的问题，在美国我们有很长的欺诈历史，有一本书叫做窃取表决票，还有一个路易斯安娜的投票，很多死了的人也可以投票。表决的人不能决定，但是计票的人可以决定很多事情了。表决技术是按照一般的计算机技术进行的，以前只是用纸张来表决，现在仍然广泛使用，在美国我们用打孔机，就是你选择的候选人可以打孔，以前老的系统是打折的，做一个记号，或者是其他的机器识别的，用铅笔画圈的。现在计算机怎么样用于表决呢？这里涉及到一系列复杂的问题，因为明年选举以后有一些问题，美国法律规定不要搞了。现在有一些问题，很多州要求用纸张进行跟踪，因此我想提的主要问题是这个技术可以用了，是不是我们可以把它做好准备，因为图纸表决、电子表决现在还无法找到答案，我们现在还不知道。我想说明一下在美国表决的复杂性，这个地图是在80年选举总统时所提供的不同技术，红色的是打孔系统，现在看到的绿色的是画圈扫描的，紫的是触摸屏的系统。目前美国的表决系统研究开展了不少的活动，Avi Rubin得到了750万美元的奖励，同时我也参加了表决的另外一个项目，我们也使它理解了目前这项技术的好处和弱点。此外还有很多表决技术方面的问题，我在委员会工作，来制定指南，以及确定表决技术，同时还有很多积极分子，需要纸张的跟踪系统，或者是有些人需要其他的系统等等。法国总统贝克先生也成立了一个委员会，需要报告、用户认证系统等等，这里有很多问题是如何使得表决系统更加有效，这个问题是涉及到很多不同方面的。另外还有表决人隐私的问题，他投谁、选择谁他不知道，因为你不能给他一个所谓的收据，还有就是卖票，因为美国人以前总是把票卖出去的，同时可用性也涉及到有没有表决系统，因为有些人不能到那些地方，这就给他们提供了表决的可能性。这些问题当中我特别要强调的是隐私性，从安全性的角度来看这个问题是非常难解决的，没有收据就无法知道在表决投票之后有些人更正了什么东西，因为搞电子商务收据也是一方面的问题。考虑表决系统的时候要考虑谁要改变答案，几乎所有的人，包括政治上的积极分子，都希望他们自己的候选人获胜，甚至外国都会想影响到结果，因为结果会影响到他们，因此这个过程所有的人，过程当中涉及到的每一部分都需要研究，需要有过程技术来防止各个方面不能够出问题，这就是这个问题的严重性所在了。

现在的问题是令人相信的程度有多少，目前我们还不知道，现在网上有一些软件，用这些软件可以分析，有些加密问题还是搞得不好，因此所谓的最先进技术还是要改善的。这些系统非常复杂，安全方面也非常复杂，二者之间也是有矛盾的。有几百万的单位在地方上加以使用，有时候是偶尔加以使用，在选举的时候才拿来使用，因此管理这些机器对有关人员也是很难的。还有一个过程，因为这些机器和系统目前不是很好，还需要改善。从另外一个投票的角度来看，那么多票是不是记录下来了，比如说摸一下屏幕是不是把我的票计下来了，这也是一个问题，因为这个东西应该是更加透明、更加令人相信的。

最终我们可以想到三个方面。第一个在美国还是比较受欢迎的，纸张跟踪系统，有一个打印的东西，投完票以后打印出来一张纸，你再检查一下让表决人看看是不是对，这个是比较受欢迎的，也比较实用的。第二，是我研究的领域，就是加密系统，我还有一个研究生也在进行这方面的研究，我会更好地介绍这个表决系统，也就是把标准提得更高一点，使得系统更加有效更加安全。一开始是VVPAT，是一个博士生写的论文，就是你投完了票以后可以打出一张纸，看看是不是你选的东西，如果是你选的东西就放在那个地方，可以成为正式的计票了。David Dill教授搞了一个软件项目，而且在这方面成为了积极分子，他主要在加州工作，现在已经有20个州开始要求这个系统了。这些还是有些争议的，需要注意到票，要保护好。实际上有两个表决程序，第一个看屏幕，第二看打印纸张，这对于有些人比较艰难，特别是对于残疾人比较麻烦。另外不能把所有的问题都解决，比如这个单子上没有这个人，如果投票人说打印的东西不是在屏幕上显示的东西，那么他就会怀疑这个机器，或者这个机器让他不能用，这时候造成服务器系统表决系统不能使用了，因此不能提供端对端的安全保障，表决人投了票也不能够说看看记录上的票是不是他的意愿，然后把他的意思表决出来、反映出来。你在保证他想怎么投之前需要电子系统加以确认，最后进行投票、进行了记录之后，你怎么知道这些没有问题，表决的问题怎么能够做得更好，能不能够提供端对端的安全保障，相信投的东西是你希望投的。我的同事们搞了加密的表决系统，加密计算机有三个做法，一个是盲签，就是当局闭着眼睛签字了，我们叫FOO，因为加密的方式可以把这个加在一起，投票以后加密，加在其他人的票上，是一种加密的形式。你可以加进去你的候选人，你可以把任何你喜欢的候选人加到选票当中去，从这个意义上来说这个要求没办法满足。最后Chaum提出了建议，Mixnets是提供一种逆遴，可以进行投票计算，但是不能追溯回谁投的票，所以要在计算的时候加密，显示出了逆遴的特点。Mixnets是一个新的理念，这是二十一世纪或者是再往前的时间里我们要看到的一种趋势。我们还有一个想法，要合适投票人的身份，官方的票是电子票而不是纸张票，所以完全是电子形式的投票，因此官方的票是电子票，你投票的时候你的票是加密的，而且是在公共广告栏里面可以看到你的投票加密回执的。另外还有纸张回执，如果票面与你希望的不符合，你可以用纸张回执更改。我们要确定投票人要投的票确实是他想要投的票，所以确实要了解有一系列的数据给它加密，这可能比较难，他可能不太信任这种投票机器，所以他没有办法对这种加密的顺序进行计算，计票机提供这一系列的数据可能不是很完善，所以他需要拿着这个证据发现一下看看是否他所投的票进行了完整的加密，所以这样的话就能够处理这两个部分，对它进行加密，对他所投的加密票进行计算。给大家一个很简单的方式，如果我们给投票人两种打出来的加密，电子的方式随意选一个放进去，另外拿出来进行加密，可能有一些投票积极分子剪掉，然后选择一个拿出来，两只手可以像猜硬币一样的，你也可以猜硬币在我的左手还是在我的右手，你没有看见我的硬币，但是硬币确实在我的手里面，这样就会对投票系统有信心。如果欺诈的话就容易发现，为了影响投票结果很可能会有欺诈。

接下来讲一下Mixnets是如何运作的。左边是一个很简单的文字选择，每横线是代表每个投票人，机器进行加密，加密完之后提供一系列的数据，是条形码，这些条形码放在公共布告栏上，我们要把票数重新排列，名字放在一边，这样没人知道怎么样进行排列，中间的Mix—Servers可以提供混杂的Server，最后我们可以对每个票进行加密，把加密过的票进行计算。所以是三部分，先是投票加密，然后服务器进行随意组合，最后比较重要的就是计算。问题是你如何能信任这里面每一步，因为你需要证据来表明所有工具、所有步骤都是有效运作的，我们讲到了第一部分，你投的票确实是你想头的票，但是你必须要争取证明，我们如何能知道这些混杂的服务器确实能够进行运作。因为重新加密，所以我们大出了一系列编码，但是编码不能混在一起，如果看一下条形码的话已经是经过服务器重新加密和服务器的重新混杂，他可能就会把一些重复投票过滤掉，最后加密的时候是否能做出合适的加密，实际上最后一部分是并不是很难做的。但是如何检查Mix能够正确发挥它的功能，一个叫做Robust的混杂，它可以提供混杂的序列排列，你要知道进来的东西和出去的东西是一样的，如果使用不同的加密形式出现的结果是不一样的。我和Jakobsson还有其他同事一起做的研究，加密有不同的做法，原来是剪，后来就是选择使得每个mix服务器能够显示一半进出系统，这样投票人的身份能够得到保护。如果我们把Mix服务器进行配对，比如Mix服务器1和Mix服务器2配成一对，这两个之间有编程码的流程，然后我们可以随意决定Mix服务器1或者Mix服务器2应该显示出两个服务器中间的结果，第一个服务器和第二个服务器之间是共通的，所以每个服务器都只显示它所交流信息的一半，如果配对之后服务器2对服务器1提出挑战的话就不会被接受，所以就会被抓住，所以我们就机率的计算来检查投票系统的公正性，如果我们发现数替能够做假的话，但是机率就会变得很低，这是很好的方式。

有的时候我们会做到更好，Public Mixing是我在MIT的学生做的一个研究，现在还没有成果。我们做了矩阵的排列，每一行有11，这代表了这样一种情形的排列，然后进行生成。矩阵本身也会进行加密，所以才生出这样一种加密后的矩阵，所以加密过的0使每个项目都变成0或者1。这样代表的就是票数，我们需要一种过程进行加密或者计算，加密过的Vector然后得出加密过的结果。最后你会有非常好的想法，Nissim跟我介绍了这样一种结果，所以矩阵就可以进行成倍数的计算，这样的进程就可以确保投票人的身份被保护，能够提供一些被加密过的信息，但是所有这些矩阵都是被加密过的，代表的顺序都是随意排列过的，我们有公布过的矩阵，有这样一个Public进行加密，所以所有的人都能够提供出这样一个Mv，v的领域是进入，Mv是加密之后v的结果，所以谁都不会知道M和v之间的关系，但是谁都知道这是加密过的。这是一种非常好的想法，这样人们就可以取消在投票时候对混杂服务器加密的信息，这就可以使用最新的算法来确保投票人的身份得到保护的方式，这是一种非常好的系统。

这是使用密码学解决投票的，另外一个做法就是必须达到标准的程序，这样可以被美国认证为被投资者加以使用，当然在美国的情况比较复杂一点，因为联邦的标准不适用于各个州，但是许多州还是实施联邦制定的保准。最近我思索了一下整个过程，这很像提供开发出高性能软件和硬件的方式，我们正在提供软件体系和硬件体系，因为你必须对它的软件和硬件体系有信心，尤其是它代表你来发挥一些作用，比如说在E商务方面进行投票的时候，所以必须建立这种性能。投票是一个非常好的例子，提供高性能的软件和硬件，我觉得Microsoft公司在开发安全的计算技术方面起到的重要作用和安全技术跟我刚才讲的都是相关的。我们必须思考一些问题，在考虑投票标准的时候不仅仅要使投票人可以对投票过程进行追踪，也可以进行无线的，你如何建立可信赖度的体系，你是把代原码公布还是把坏的原码都拿到，所以代原码可能会公开，制造商总体来说不愿意公布它的代原码，还有文件的要求，供应商在测试的时候应该提供什么样的文件。安全性是一个非常有意思的特点，因为现在不是要求它有多少功能，坏人如果攻破这套系统之后会做些什么，许多聪明的人是没有办法突破它的安全设置的，所以没有办法影响到投票的结果，这是一个非常困难的事情，我们现在拥有的Tiger小组的评论，他们是非常聪明的人，他们可以了解所有的文件，然后说想试图突破安全系统看看能不能够解决，以前在美国没有这些既定的标准，我们需要了解一下应该采取什么样的努力，Tiger小组的成员应该是谁，是如何选择的。最佳的做法不仅仅是硬件的问题，投票系统还牵扯到管理这些硬件的人以及投票选务官员，是帮助选民和投票的这些人，这是一系列不同的因素。我们经常看到安全系统不奏效，因为由人进行的界面要么是很难使用，要么就是安全性不够，投票体系经常有一些商业上的运行，比如说Microsoft的数据库或者是Microsoft的操作系统，这些商业上要运行的数据有它自己的脆弱性，所以投票系统要确保整个体系的每个组成部分，如果有任何脆弱存在的话都要进行加强，还有就是要管理一下谁来管理这个系统，这里面牵扯到了诸多的问题，还有要解决标准化的问题，我们看到系统有多重功能，可以用电子和非电子的方面来做。刚刚也讲到了软件开发问题，Microsoft在这方面开发出安全代码，我想投票系统基本上需要实施这种类似代原码的方式，这样可以产生正确的结果，你所希望达到的结果。投票系统软件开发之后你如何确保投票体系里面所用的软件确实是被认证和批准过的，还有数字认证、数字签字等等这些技术都在这里面发挥重要的作用。整个系统的认证合适也是非常重要的，作为一个选务官员，你如何能够知道这个投票系统里面所装的软件都是对的，这个系统第一天在仓库里呆着第二天用，你怎么知道这个机器里装的软件是对的，怎么能够确认它的设置是对的，这并不是很简单，机器要弄过来的话你问有些什么文件可能会向你撒一些谎，所以要确认这个机器有没有被人动过手脚，这也是今后发展的一个重要方面，希望这方面的技术在今后的表决系统当中可以加以使用。我们往前看的时候也可以看到其他的问题会继续出现，包括远程的表决，这也是美国的一个热门话题，有很多的州包括墨尔本州是通过邮寄方式表决的，我特别不喜欢这种方式，因为邮寄和网上投票现象是最容易使腐败现象发生的，所以在互联网方面的投票压力也是很大的，我希望大家思考这些技术，通过什么样的方式能够减少改变投票结果的影响，最好的方法就是不止是第一次表决，只算最后一次表决，比如说早上有人给你付了钱去表决，下午又要表决了，对于标准化的问题，同时系统要认证，同时这也说明商务性的软件有很多的脆弱性。

最后我做个结论，我现在给大家简单地介绍一下在表决系统方面的技术以及研究工作，表决系统从技术角度来说是很大的挑战，我们现在处于一个过渡阶段，以前是纸张打孔卡的系统走到电子系统，现在还不是很清楚，有一个很清楚的迹象，加密可以起到很好的作用，可以使得界面更加清晰，整个东西模块化，容易测试、容易评估，但是今后发展的步骤还不是很清楚，我们要相信机器是好的，不需要书面的东西重新计数，靠电子的就行，又可以不影响表决者的隐私。怎么能够把这些做好还不是很清楚，因此希望搞这方面研究的学生选这方面的题目进行研究，这方面还有很多工作需要做。谢谢！

洪小文：谢谢Ronald L.Rivest博士的精采演讲。下一位演讲者是Jeannette Wing，她的中文名叫周以真，我20年前去CMA念书的时候他刚刚到CMA担任教授，她今天的长相和20年前完全一样，养生有道。Jeannette Wing在1979年得到MIT的学士学位，83年在MIT得到博士学位。她的研究方向非常广，包括变频式分布系统的规范和认证，以及编程语言，他目前主要的研究是提升软件安全技术的设计与评价工作。Jeannette Wing教授曾经参与编写了11本书，100篇的期刊会议，以及博士论文，他在很多国际研究机构都担任顾问的要职，例如在国家科学院计算机科学与通讯部担任主席，他也是Microsoft可信度计算委员会成员之一，同时他也在国家实验室和国土战略安全咨询委员会的会员。他今天要演讲的题目是我们如何能够把我们的软件做得更可以预知，使得它更加安全。现在我们有请Jeannette Wing教授。

Jeannette Wing：大家早晨好！非常荣幸能够今天早上到这里为这么多公众以及非常优秀的人士发言，我想感谢Microsoft组织了这次会议，也要感谢浙江大学，以及感谢地方官员，作为东道主在杭州这个美丽的城市举办这个会议。

我保证我要讲的是可预测的软件，这基本上是一个摘要，但是我想借此机会向在座的学生、系主任、校校长、计算机科学的研究人员，本着这次会议的主题，也就是“二十一世纪的计算”来介绍一下我的想法，这一点也是与计算机科学有关的。开始的时候我先用一分钟跟大家讲一下计算的讲法，之后讲一下可预见的软件。

我对这个领域总的想法是这样的，计算机科学要超过任何行政、任何国家的边界，这是我对于计算机科学的一个远大想法。计算机应该是在二十一世纪中期每个人都应该掌握的一个技能，就像读书写字一样，这也是我的梦想。大家可以想象每个孩子都知道如何像计算机科学家那样思考，这会是怎样的世界呢？要实现这个梦想，计算和计算机就要一起来工作，我要给大家讲一下计算思维的例子。每一次面对一个问题的时候我们都要面对一个问题，这个问题的难度有多大，每一次我们都有精确的问这个问题的方式，也有回答这个问题的方式。计算的想法就是把看来更加困难的问题换成一种我们知道是如何解决的问题，通过嵌入、转换、模拟等等，计算的方法就是选择一个适当的代表或者模型反映出这个问题的有关方面，使得它有不可更总性，计算的想法就是把解决复杂的问题分开来解决，同时也要判断它的设计和好处，简单化。同时也要检查分析多面的一般化的问题，计算机的思维就是要防止出现最大问题的时候如何恢复，这种东西也涉及到多用户，这也涉及到僵局，然后是涉及到解决非常难的人们的困难等等。总的来说，计算机思维就是采取方法解决问题，并且理解人类的行为，而且是和计算机科学非常关键的一些想法，有些计算机思维最喜欢的例子你也可以告诉我们。在学习方面，计算机思维也使得统计问题革命化了，美国的一些统计部门也在用计算机科学家，因为他们知道今后他们的未来在这个职业。美国的计算机学院也开始拥抱现有的部门了，我们的梅隆大学和Microsoft公司开展了合作，我们认为算法和结构以及计算机思维方式将有助于生物学的发展。也有专家在游戏理论以及计算机方面进行广泛的研究。

下面我就讲可预计的软件，这也是有想法在里面的，这和前头相比不如那个那么宏伟，但是更加实际，我主要想对在座的学生讲这些内容，因为希望你们能够面临我们研究的一些挑战，使我们的软件更加有个性，就这个问题使你们能够兴奋起来。软件应该是无“数”不在的，不能对软件周围画一条线，它周围应该是有小的应用程序母本构成的，还有大的一些东西，包括操作系统数据库，很难定起来难以找到的东西，比如移动编码当然是永远存在的，但是是有记录的。很难找到谁是这个软件的写者，令人不能相信的是不能知道来源和创造者，同时也是认证的编码，所以相信是第三方的编码。不久就会有一些这样的图画，我会逐渐把这个变得更大。这是医院的一个病人，给他输液，输液管道是由软件控制的，医院的病人也是有专门的房间，同时医生也带着PDA走来走去，另外还有一个远程病房会有医院档案记录的地方，比如记录一下这个病人花了多少钱。同时医生也可以拿着手机开着车远程对病人治疗情况进行监护。这个远大想法并不是不太现实，我们不久就会看到这些，可能还会很快看到，问题就是到处都有很多软件，我们如何相信软件能够把工作做好。有一些非常有意思的想法和评论，一个是嫁接系统，这种系统在关键系统当中是有的，特别是控制性的软件来确定是不是做了某些移植，在核反应堆控制系统当中也是用这种软件，在智能汽车、智能高速公路上都用这样的系统，这是多样通讯系统，涉及到很多不同的装置，包括使用什么样的机制、什么样的协议，我们到处都可以看到分布式的系统，每天都可用，并且可靠安全。前面也讲到隐私的问题，要使得隐私在表决票上加以保护是很难的。关于人机界面这一块，要注意到社会上能够接受。最后，所有人都注意到我们今天做的这些事情都会需要面对，甚至是更多这方面的问题，也许今后的问题会更加大了。

我想讲一下多重系统这方面的挑战，嫁接混合系统这方面环境是多重的、难以预测的，这个环境的复杂性是由于自然造成的，有些非常复杂的东西要做模拟，还有一些不同的变量都要加以反映。系统完整性的特点不是考虑到功能了，要使得计算能够更具有出色的结果，但是根据其他资源的限制还要考虑到硬件。看这张关于混合系统，比如说刚才那张照片，都可以意识到非常复杂。怎么保证这一点，到处都用的软件有什么影响，一个是纸张问题要加以保证，当然还有可靠性，除了可靠性之外还有安全的问题，在我们的编码当中还有很多方面。我认为安全性、可靠性、可用性这几个问题就构成了令人可相信的计算组成部分，Microsoft公司可以说在这方面是领导公司之一，领导着令人可以置信的计算，领导着我们的软件发展。到处都有软件，这还有什么影响？我们如何来确定这些特点如何拥有的，对软件体系做一个什么样的定位，性能很好以及正确这两个方面我们说了几十年了，正确就是对不对，性能就是快不快，我想正确性和性能还是不够的，我们是否能够实施可信赖的技术。什么叫正确和信赖，这意味着什么，这个听起来不错，是不是可以及时做正确的事情，比如说Google是已经不错的结果了，但这还不行，对于Google来说并不需要结果是完全准确的，只是需要这些差不多的回答第一时间出现在浏览器上面就行了，但是在技术方面还是不够的。我们应该尝试可预测性的标签，是否可预测，意思就是说正确的行为、而且是可接受的行为，和不可接受的行为，而且可预测可接受，这是由最终用户，是人或者机器来决定的，当然不同的用户之间对这个有不同的界定。这些方法我已经用了很多年，你必须从一个体系的模型入手，这样的话你可以通过很多的模型进行预测，所以是企业这样的一个方法，这里有两个方面，一个是体系方面的模型，另一方面是他的这种特征，就是你希望这样的体系有什么样的特征，所以两个信息放到两个选择里，而且是自动的，你或者说是或者说不是，你输入的信息是看是否能用，这些检查装置是看这些检查方式你可能会获得一些模棱两可的结果。有时候你的过程不够有力可以是你得到准确的答案。另外企业方面的，你需要具体的说明你想让系统展现的特征，企业方面的另外是一个竞争和谐方面的进程，我们显示这些特征是有效的，对特定的系统模型来说是可行的。如果我想我的客户从中有所获益的话，使他们了解系统要起的作用，或是把核查软件系统进一步的推动，模型核查有很多的好处，速度快，可以处理大量的文件，你不必有一个完整的对特征的具体规格的说明，或者说在做任何的工作之前，不必做很细的规定。那么，他的范围是非常的广。从安全的特点，那么安全性的特点是说不会有任何不好的事，另外，最终一些好的东西可能会出现。我想这个模型核查的主要的优势在于这种核查系统，可以告诉你这些特征的成立或者是不成立，但是他在告诉你不成立的时候，他就会提出一些反对的例子，就是说这种核查的价值，恰恰是为什么说像Microsoft这样的公司使用这种模型核查，因为这些反例子告诉了我们为什么这种软件设计是不对的，他是作为一种消除错误的机制。

但是有一个很大的不利之处。就是空间扩展的问题，对模型核查来说，假定你认为你输入的东西，在每次作核查的时候，另外一个人可以说他处理这个系统的时候，他的量比你多，这个量的问题是来源于不同的渠道，比如说有平行错误的时候，你有很多这种线程的控制，比如说在软件区域很丰富的时候，你需要看每一个系统到处理多少的程序。这个问题成为过去20年来模型研究员所关注的对象。

比如说分解和分解的技术，还有多模型的技术，这张图显示的是这有两个输入的信息，这两个信息放到黑盒子里面去，他被成为模型检查器，模型的问题是代表一些最后的结果，这些问题是你是否对MS成立。

给大家分享一下模型中的一些成功的程式，这是我的学生找到了很多模型的错误，其中很多在获得博士学位的人在80年代就提出了一个理念，94年的时候INTEL公司如何发现Pentium流程的问题。许多公司进行模拟测验，来设计何时可以看到软件的错误。而且最激动人心的故事，最近几年里面由Microsoft公司所做的工作，在2000年的时候，我们的发言人已经讲过的，这些结果非常成功，Bill Gates说在2002年的OOPSLA里面提出的故事。模型核查在过去30年里面取得了很大的进展。

这是最近两年的结果，一个是针对我所在的安全性方面的工作，作为模型检查的一种扩展，怎么解决安全性的问题，之后会给大家显示一下我在卡内基大学的同事所表明的一种新的技术，就是把混合模型核查的新系统。

模型核查是通过提供反例子告诉你为什么你的系统就某个特定的特征来说是不对的，在我所做的工作里面，我们爱查出所有的反例子，特定的模型和特征不止是一个。这个图从左到右先开始最初的一些状态，之后进入最后的阶段。红色团队是由美国国家实验室建立的，现在在开发这样一种图形，它把红色团队加入进来，告诉他攻击者如何进攻我的体系，它提供一种攻击路线图，这个图的提供是手工做的，这意味着一些不一致性、重叠性，以及一些不完整性。做任何手工工作的时候我们一直在说能否自动来做，这是我和我的学生一直在问的问题，所以我们采用模型核查来自动产生所谓的攻击路线图，反例子就把它形成一种攻击。反例子是来自一系列Stat组成的，这种攻击就形成了一系列的Stat。就是说违反了特定的安全特征的。这是单一的简单反例子，入侵者能够成功的道路。具体来说，在所有的Stat里面入侵者没有获得托管系统的准入。最后的M就是安全特征，攻击违反了行动，所以M是一系列的攻击。

我来介绍一系列的办法，我们有M的攻击，以及G的图形。最后一种办法我们用M和G进行计算，然后产生LM和(I)，然后我们得出G，最后我们就形成这样一个G的供给图，这是一种非常简单的算法，然后得出我们所需要的东西。

性能很不错，而且是达到了这样一系列的技术。这个例子是我们如何把模型核查扩展到各种各样的反例子里面，然后用到安全性能当中去。下一个例子是新的技术，证明所有的模型核查都是试用的。在这里给大家介绍一下混合体系。这帐技术是专门用于处理大的Stat，尤其是无线Stat。现在有一个具体的系统，M，先得出Mh，如果违反了(I)，你可以继续去找，一直到停止的时候。这里面有个理论，叫做危机理论。如果能够满足(I)的话，那就证明最初的模型M能够满足(I)。这项技术已经在硬件里面得到使用，尤其在核查的时候得到了应用，以及其他一些例子得到了应用。我给大家显示的例子是一种混合的系统，混合系统属于无线系统，你必须处理各种各样的变量、状况，以及气压、气温、流通速度，以及其他一些因素，告诉你处于什么样的模型中。通过这种控制图，一系列的反例子技术肯定有个对应的途径，实际发生的情况是你先开始M系统，然后把原先的进行界定，之后找到你的反例子，最后对模型进行测验，如果没有对应的途径的话，就要继续去找。你要确定在抽象当中所找到的例子是可以用不同的技巧做到的，可以用不同的方式，更重要的是你可以用不同的技术，只是审查反例子当中的一部分就可以了，因此我们把技巧适用于那种平常性的控制。

在美国有些高速公路是连接不同城市的，这些高速公路通常上面没有车，或者车是非常少的，这是很难令人置信的一件事情。也许从纽约到西雅图去，或者是开到旧金山去，这个距离比较远了，你坐在车里还是很累的，车上有这么一个功能，你累了时候就按一下按纽，脚就不用加油了，这时候定个寻航，比如70脉，因为前面没有车，你就不用总踩着油门了，这就叫平衡控制。至于说前面没有车，或者是车比较远你不会追尾，这种系统就比较好了，但是在城市里开就不行了，在杭州开就更不行了，在杭州根本就不可能用寻航控制系统。但是美国的一些人会提出，我们会想办法，来找一种适应性的寻航控制，前面有车你离他比较近的时候，而且你的速度在不太安全的情况下，如果你靠他比较近了的话，这时候我们用一种自动方式你的车就会减速，我们把这个叫做适应性的平衡控制系统。

这里要确定这个系统当中的一些特点，实际上特点也很简单，没有追尾就行了。我们对这个系统做了一个模拟，是非常简单的一种混合式的系统，你可以看到这里左上角的状况，我会把这个结果再说明一下。在左边可以看到状况，用一种反例子的做法，就是说你可以用刚才检查反例子的一些状况，这时候几乎没有什么要检查的状况，因此这个技术是非常令人兴奋的，我们可以用于一些非常困难风险非常大的系统当中。

我给他们提出一个挑战，这并不是软件检查的挑战，软件模型检查为什么变得那么具有挑战性？有哪些因素呢？包括编程语言，以及今后到处都有的软件，这本身就是软件模型的复杂性和挑战性。这里列了这么多问题，这里其中一个有可能会成为你们今后写论文的方向，这些都是值得研究的挑战领域，也是面向我们这个社会的，Microsoft也在解决很多这方面的问题。你可以问一下要检查什么，是检查编码还是检查编码的设计，有些人可能会说，不要去管码了，只要检查设计就好了，因为设计错误了，检查编码也是没有用的。有的人关心的是软件架构模式检查，或者叫审查。我的同事还有一个问题，那些特性如何进行检查，因为今后的软件越来越复杂，他们今