ACM SIGOPS名人堂（第三期）
我爱计算机 本文转自 CNSys
前面我们介绍了两期，分别是：
在本期SIGOPS名人堂中，我们将介绍2007年获选的3篇文章：
- J. H. Saltzer, D. P. Reed, and D. D. Clark “End-To-End Arguments in System Design”
- Michael Burrows, Martin Abadi, and Roger Needham “A Logic of Authentication”
- Fred B. Schneider “Implementing Fault-Tolerant Services Using the State Machine Approach: A Tutorial”
前两篇分别发表在1984年和1990年的“ACM Transactions on Computer Systems”，第三篇发表在1990年的“ACM Computing Surveys”。
“End-To-End Arguments in System Design”
Jerome H. Saltzer（左）David P. Reed（中）David D. Clark（右）
本期介绍的第一篇文章是Jerome H. Saltzer、David P. Reed和David D. Clark共同撰写的“End-To-End Arguments in System Design”。这篇文章提出了著名的“端到端原则”：如果某项功能只有在位于通讯系统终端上特定应用的参与下才能被完整且正确地实现，那么将其作为通讯系统的一项自身特性或核心功能是不可行的。一方面，在底层实现这些功能的代价可能很高，而并非所有应用需要这些功能，由此引入的开销就成为了累赘；另一方面，位于底层的实现通常只能应对部分情况，而完整机制的实现依然需要终端的参与。文章从可靠文件传输为例切入，围绕位错误修复、安全加密、消息去重、崩溃修复、投递回执等为了满足通讯可靠性要求的机制，探讨了在通讯系统底层与在终端上实现这些功能的代价，来佐证该原则的合理性。
“端到端原则”为网络设计者开发网络协议及应用程序提供了普遍的指导意义。互联网良好的伸缩性、通用性和开放性正是得益于此。值得一提的是，论文的第三作者David D. Clark在1981～1989年担任互联网架构委员会（Internet Activities Board）的主席并兼任首席协议架构师，对互联网协议的设计与发展产生了深远的影响。第二作者David P. Reed也参与了早期TCP/IP协议的开发，是UDP协议的设计者。第一作者Jerome H. Saltzer是其他两位作者的导师，参与、领导了CTSS、MULTICS、Athena等众多项目，是大名鼎鼎的Kerberos协议的设计者之一。
“A Logic of Authentication”
Michael Burrows（左）Martin Abadi（中）Roger Needham（右）
第二篇文章是来自Michael Burrows、Martin Abadi和Roger Needham的“A Logic of Authentication”。本文提出了一套形式化分析认证协议的逻辑方法，又称“BAN逻辑”（BAN为三位作者姓氏的首字母缩写）。认证协议是众多分布式系统能够安全、可靠地进行运作的基础，因此其正确性至关重要。然而，在BAN逻辑出现之前，人们只能凭借经验或直觉来查找其中的漏洞，导致很多协议的原始设计中出现了安全隐患或是存在信息冗余。BAN逻辑使用形式化语言在抽象的层次上研究认证协议的安全性，让设计者们从此可以通过逻辑推理的方式来检查协议是否存在问题及可改进的空间。
BAN逻辑是一种多类型模态逻辑（many-sorted model logic），处理对象包括主体、密钥和公式。作者在论文中定义了包括消息含义（message-meaning）、临时值验证（nonce-verification）、管辖权（jurisdiction）、消息接受（seeing）和新鲜度（freshness）这五方面的推理规则。具体应用时，我们首先需要将协议“理想化”（idealize），即转化成BAN逻辑的语法所定义的形式，然后使用规则进行推理，判断协议是否能够达成预期目标。文章中包含了对四种常用认证协议（包括前面提到的Kerberos）使用BAN逻辑的分析过程，并在最后以表格的形式列出了更多协议的分析结果。值得注意的是，BAN逻辑尚不完美：后续的研究工作发现，部分通过了BAN逻辑验证的协议事实上依然是不安全的。尽管如此，这篇文章的诞生引领了后续很多系统及安全领域的杰出工作，启发了研究者们使用基于逻辑的形式化分析方法进行系统性的思考。
本文的第一作者Michael Burrows在很多其它领域也有所建树：他设计的Burrows-Wheeler转换算法应用在很多数据压缩技术（例如bzip2）中；作为早期流行的搜索引擎AltaVista的联合创始人开发了其核心系统；后又加入Google，是Chubby、BigTable（获选2016年SIGOPS名人堂）等分布式计算架构相关项目的主要贡献者。第二作者Martin Abadi在系统、安全、程序设计语言领域均发表了大量工作，包括TensorFlow、Naiad、Spi Calculus等。第三作者Roger Needham除了这篇文章外，还有两篇工作分别入选了2008年和2010年的SIGOPS名人堂，我们将在后面几期中予以介绍。遗憾的是，Roger于2003年去世。为了纪念他在计算机科学领域的杰出贡献，英国计算机学会（British Computer Society）和欧洲系统会议（EuroSys）每年都会颁发以其名字命名的荣誉和奖项。剑桥大学的一幢楼也以其名字命名。
“Implementing Fault-Tolerant Services Using the State Machine Approach: A Tutorial”
Fred B. Schneider
本期介绍的最后一篇文章是来自Fred B. Schneider的“Implementing Fault-Tolerant Services Using the State Machine Approach: A Tutorial”。这篇文章以综述的形式详细地阐释了如何使用状态机复制（state machine replication）的方式来实现具有容错能力的服务，向研究者和工程师们提供了一套理解和设计复制管理协议的框架。
容错性是大规模分布式系统能够持久地提供可靠服务的重要前提，因而一直是系统领域的热门研究话题。Fred的这篇文章深入浅出地介绍了如何基于状态机的模型来表示服务，将状态机复制在若干服务器上，并协调客户端和服务器各个副本（replica）间的交互，来实现可以容错的服务。文章针对拜占庭（Byzantine）和失败-终止（fail-stop）两类具有代表性的错误类型，分析了如何设定副本的个数并协调副本的运作。具体的实现围绕两方面展开：请求处理的一致（agreement）和顺序（order），即每个正常运行的副本会收到每个请求，且处理这些请求的相对顺序是相同的。除此之外，文章还讨论了如何对系统的输出和客户端部分进行容错，以及如何允许系统的重配置（例如动态地增加或删除副本），来实现一个完整的具备容错能力的服务系统。有趣的是，作者在最后的相关工作中讨论了如何把很多已有的技术套用状态机的模型来思考，包括著名的Paxos协议（2012年SIGOPS名人堂）、两阶段提交（two-phase commit）协议等。
Fred于今年入选了美国艺术与科学院院士，其主要研究领域包括分布式系统、并发系统与系统安全等。
小结
本期介绍的三篇文章从三个不同的角度讨论了大规模系统实现中的一些基础核心问题，其中的不少内容经过时间的沉淀已经成为了教材中的经典，引领了一批又一批系统领域工作者不断的追寻并展开新的探索。在下一期SIGOPS名人堂中，我们将继续为大家介绍2008年入选的部分论文。
作者
朱晓伟，清华大学计算机科学与技术系，博士生，主要研究方向为并行计算、分布式计算和大数据处理系统。
参考文献
[1] https://www.sigops.org/award-hof.html
[2] http://web.mit.edu/Saltzer/www/home.html
[3] http://www.reed.com/dpr/
[4] https://groups.csail.mit.edu/ana/People/Clark.html
[5] https://en.wikipedia.org/wiki/Burrows%E2%80%93Abadi%E2%80%93Needham_logic
[6] https://en.wikipedia.org/wiki/Michael_Burrows
[7] https://users.soe.ucsc.edu/~abadi/home.html
[8] http://www.cl.cam.ac.uk/archive/ksj21/RogerNeedham.html
[9] https://www.cs.cornell.edu/fbs/
[10] https://en.wikipedia.org/wiki/State_machine_replication
