ACM通信
实践
实践研究:私人网络交流系统验证要点
来源:盖蒂图片社
这一期的实践研究涵盖了现代计算机系统中两个令人兴奋的主题:私有通信系统和验证系统编程。
首先,艾伯特Kwon提供用于安全和私有通信的最新系统的概述。尽管Signal等消息传递协议提供了隐私保障，但Albert所选的研究论文阐明了尖端技术的可能性:更透明的端点身份验证、更好的通信元数据保护和匿名广播。这些论文将最先进的密码学与实用的、保护隐私的协议结合起来，让我们对未来的安全消息传递系统有了初步的了解。
第二,詹姆斯·r·威尔科克斯带我们参观了验证系统设计的最新进展。现在可以构建经过验证的端到端编译器、操作系统和分布式系统证明地在定义良好的规范方面是正确的，提供定义良好的、行为良好的代码的高度保证。由于这些系统组件与低级硬件(如指令集体系结构和外部网络)交互，每篇论文都引入了新的技术来平衡形式正确性和实际适用性之间的紧张关系。随着编程语言技术的进步和更多的现代计算堆栈的继续具体化，期望这些进步能够进入生产系统。
一如既往，我们在这个专栏的目标是让我们的读者在一个周末下午的阅读中成为计算机科学研究最新主题的专家。为了促进这一过程，我们提供了ACM数字图书馆对这些选择的相关引用的开放访问，以便您可以充分享受这些研究成果。请享受!
彼得百利
私人在线交流:Albert Kwon著
当我们在网上交流时，我们希望得到和线下一样的隐私和匿名性。然而，最近泄露的信息表明情况并非如此，因为大规模的监视威胁着我们日常交流的隐私(参见“NSA文件解码;”https://docubase.mit.edu/project/nsa-files-decoded/，“美国国家安全局的幻灯片展示了对海底电缆的监视;”http://wapo.st/2zFYuKQ，以及“国安局间谍活动”;https://www.eff.org/nsa-spying）.
尽管如此，研究人员和开源社区在保护隐私方面也做出了重大努力:Tor帮助数百万用户在网上保持匿名(https://www.torproject.org/)和Signal协议(https://whispersystems.org/)已经为超过10亿用户提供了端到端加密安全聊天服务。
然而，在确保在线交流隐私方面仍存在许多重要挑战。这里展示的几组论文强调了近期解决一些挑战的工作。第一组论文是关于CONIKS和证书透明度(CT)的，解决了端到端加密公钥的安全分发机制。下一篇论文介绍了Vuvuzela，展示了两个相互信任的人如何在不透露任何对话内容或元数据(例如，与谁以及何时交谈)的情况下进行在线交流。最后一篇文章讨论了Riposte，这是一个用户可以匿名发送消息的系统，这意味着没有人(甚至消息的接收者)可以了解任何消息的发送者。
公钥基础设施
梅拉拉，M.S.等人。
CONIKS:为最终用户带来密钥透明性。在24日的议事程序thUsenix安全研讨会, 2013;https://www.usenix.org/node/190975
劳瑞，b等人。
证书的透明度。Ietf RFC 6962, 2013;https://tools.ietf.org/html/rfc6962；
端到端加密在今天的Internet中已经很普遍了(例如，https/TLS)，但是仍然存在一个重要的引导捆绑问题:如何确保为正确的端点加密?传统上，我们信任少量实体，如ca证书颁发机构(ca)或PGP (Pretty Good Privacy)密钥服务器来维护有效的公钥列表。然后，用户可以查询它们以获取密钥并启动加密通信通道。不幸的是，正如我们在实践中多次看到的那样(参见“伊朗中间人对谷歌的攻击显示了证书权威机构的危险弱点;”http://bit.ly/1sbdGWk)和“如今HTTPS有多安全?”它多久被攻击一次?”http://bit.ly/1LegDNa)，这些实体可能被破坏，从而向用户提供不正确的密钥。
ALBERT KWON:在确保在线交流隐私方面仍存在许多重要挑战。
CONIKS与证书透明度(http://sigops.org/sosp/sosp15/current/2015-Monterey/printable/136-hooff.pdf)的目的是消除单点信任，并分别为终端用户密钥和传输层安全(TLS)证书的公开密钥基础设施增加透明度。尽管细节不同，但高层思想是相似的:它们都使用透明日志，这是作为Merkle树存储的公钥集。当第三方(例如，用户、专用监视器等)从CA或密钥服务器请求公钥时，响应附带可以有效验证的证明，以确保密钥是正确的。这两种系统都是实用的，只需要额外几千字节的数据来验证密钥;特别是，CT已被许多ca部署，而且许多流行的浏览器(如Chrome和Firefox)已经提供了内置支持。
私人的点对点通信
Lazar, D.等。
Vuvuzela:可扩展的私人消息，抵抗流量分析。在二十五次会议的会议记录th操作系统原理研讨会, 2015年
加密可以隐藏消息的内容，但它不能隐藏潜在的重要元数据，例如与谁以及何时交谈。Vuvuzela是最近的一项工作，它通过在网络中添加噪音来模糊用户的动作，尽可能地隐藏元数据。
该系统由几个呜呜祖拉服务器组成，它们共同充当隐私提供者。呜呜祖拉用户通过呜呜祖拉服务器向系统中的其他用户发送信息。当每个服务器路由消息时，它还会添加许多虚拟消息(与真实用户发送的消息无法区分)，这样，只要其中一个服务器保持诚实，对手就无法知道两个用户是否在相互通信;本文的一个关键见解是使用差别隐私来确定提供可证明的强隐私保证所需的虚拟消息的数量。呜呜祖拉可以通过市面上的机器为数百万用户提供短信式的短信服务，用户可以容忍一定的延迟。据我所知，这篇论文是在私人交流中首次使用差别隐私的论文之一，这本身就令人兴奋。
JAMES R. WILCOX:近几十年来，研究界已经开发出了一些技术，允许人们验证真实系统的重要属性。
匿名通信
科里根-吉布斯，H.等人。
反驳:处理数百万用户的匿名消息系统。在2015年IEEE安全和隐私研讨会论文集；http://dl.acm.org/citation.cfm?id=2867658．
有时，一个人可能还想对消息的接收者隐藏他或她的身份。例如，举报人可能希望向一大群人或观众或一个特定的端点发送消息，而不透露发送者的身份。Riposte是一个匿名广播系统(想想匿名的Twitter)，它为数百万用户提供了这样的服务。
与Vuvuzela类似，Riposte使用少量服务器，其中一台需要诚实才能保证匿名。为了发送消息，用户将他或她的消息分成多个共享，每个共享分配给一个服务器。然后每个服务器将每个共享存储在一个数据库中。在大量用户提交消息后，服务器聚集在一起，同时显示所有消息，而不向任何人显示消息的发送者。该系统每天可以支持数百万条tweet长度的消息，是理论与实践如何结合的一个很好的例子:该系统具有安全性的正式证明、原型实现和评估。
最终的想法
随着世界的联系越来越紧密，私人交流的重要性将继续增长。这里介绍的论文只是最近关于这个主题的一些例子。许多其他有趣的论文都是关于私人交流的。箱型雪撬(https://www.usenix.org/conference/osdi16/technical-sessions/presentation/angel)是另一个私有点对点通信系统，它在一个更强大的威胁模型下以延迟为代价提供隐私。其他匿名网络，如异议(https://www.usenix.org/node/170846)及Riffle (https://dspace.mit.edu/handle/1721.1/99859)提供类似于Riposte的匿名保证，但有不同的权衡。
然而，实现每个人的私人交流仍存在许多重要的挑战。举几个例子:我们如何将私人通信扩展到数十亿用户?我们如何在不牺牲用户隐私和匿名性的前提下让用户承担责任?我们如何使隐私用户友好?毫无疑问，在不久的将来会有更多有趣的作品问世。
系统验证的亮点:由James R. Wilcox
人类现在在生活的各个方面都依赖软件，包括安全关键应用程序。程序员使用一系列的技术来找出错误，最常见的是测试或静态分析。在这一领域中，最严格的是正式验证，几十年来，它一直试图通过数学证明来确保没有错误。
近几十年来，研究界开发了一些技术，使人们能够验证真实系统的重要特性。在审查这项工作时，不仅要考虑每个系统的保证，还要考虑它们的假设，这是很重要的;这些假设被称为可信计算基础或TCB。
本文的其余部分将重点介绍验证技术在普及系统基础结构中的三种应用:编译器、操作系统和分布式系统。这些项目预示着一个未来，实际的系统可以由现有的经过验证的组件构建，消除从硬件到应用逻辑的整个类错误。
验证编译器:Compcert
勒罗伊,X。
一个实际编译器的形式验证。ACM的通信52 .单击“确定”， 7(2009年7月)，107115;//www.eqigeno.com/magazines/2009/7/32099-formal-verification-of-a-realistic-compiler/abstract
编译器bug是有传染性的:一个有bug的编译器可能会使本来正确的源程序在运行时行为不端。这对于任何程序员来说都是值得关注的，特别是如果程序员想要在源级进行推理或使用源级程序分析。任何分析结果都有因编译器疾病而失效的风险。
CompCert是一个C编译器，它已经被正式证明永远不会错编译源程序。更准确地说，CompCert保证生成等价于C源程序的汇编代码。使用Coq证明助手对CompCert进行编程和证明。
像所有经过验证的系统一样，CompCert相信某些其他软件是正确的。经过验证的系统的TCB通常包括用于进行验证的工具、规范和垫片这是用来连接系统与世界其他地方的粘合代码。CompCert的TCB包含Coq本身、OCaml编译器和运行时以及操作系统等工具;规范，包括C语言和目标汇编语言的语义;以及它的垫片，这是一个未经验证的OCaml程序，负责从磁盘等读取文件。
验证操作系统:seL4
Klein, G.等。
seL4:操作系统内核的正式验证。ACM的通信， 6(2010年6月)，107115;http://dl.acm.org/citation.cfm?id=1743574
操作系统bug，如编译器bug，可能会导致正确的程序出现错误。更糟糕的是，OS的传染性bug可能会导致进程之间无意的交互。这样的交互可能会导致安全漏洞，例如跨进程边界泄露敏感数据。
seL4是一个操作系统内核，它经过了完全功能正确性的验证。更准确地说，seL4被展示为细化其行为的抽象规范。这种细化保证了任何系统都不会意外地调用panic、无限循环或返回错误结果。这些保证足以建立诸如访问控制和进程隔离等安全属性。
在Isabelle/HOL证明助手中完成的细化证明首先表明C实现细化了用Haskell编写的可执行规范;然后展示Haskell规范以完善抽象规范。
seL4的TCB包括Isabelle/HOL本身、C编译器、硬件、抽象规范和shim(由数百行手写汇编组成)。
已验证的分布式系统:威尔第
Wilcox, j.r.，等人。
Verdi:用于实现和正式验证分布式系统的框架。在程序设计语言设计与实现会议论文集, 2015;http://homes.cs.washington.edu/~mernst/pubs/verify-distsystem-pldi2015-abstract.html
至少编译器和操作系统bug是本地化在特定节点上的。相反，避免分布式系统的错误需要对节点之间的交互进行推理。此外，分布式系统必须容忍底层硬件的故障。
Verdi通过对网络的建模支持对分布式系统的推理网络的语义，它正式捕获节点可能遇到的潜在故障，包括消息丢失、机器崩溃等。Verdi采用经过验证的系统变压器(VSTs)，例如，它可以为现有系统增加容错能力。Verdi已被用于验证Raft共识协议作为从单个节点到复制系统的VST。
Verdi信任Coq本身、OCaml编译器和运行时、网络遵守错误模型这一事实，以及它的shim(负责底层网络和磁盘访问的未经验证的OCaml程序)。
未来的发展方向
研究界现在已经验证了许多公共基础设施。展望未来，我们如何将这些部分连接起来，以构建更大的经过验证的应用程序?
作为一个简单的例子，想象一下将来自这里突出显示的域的经过验证的系统组合起来，以构建经过验证的复制键值存储。这样的系统将使用Raft进行复制;用经过验证的编译器编译;并在经过验证的操作系统上运行。如今，由于几个原因，人们还不清楚如何执行这一计划。
首先，这些系统是用不同的证明assistantsCompCert和Verdi在Coq中，seL4在Isabelle/ hol中编写的，所以不能直接推断它们的组成。
其次，系统很可能对彼此或共享环境做出微妙的不兼容假设(例如，seL4可能使用CompCert不支持的C特性)。类似地，系统的正确性定理并不是设计为逻辑上一起工作的;例如，威尔第对操作系统的假设不太可能完全是seL4所证明的。
最后，许多技术需要以支持验证的方式从头重新实现系统，但这在大型遗留系统的世界中是不切实际的。
我们需要技术从经过验证的组件构建更大的经过验证的系统。这方面的一个亮点是最近的DeepSpec项目，它寻求跨多个抽象层连接验证项目。未来的工作应该寻求将经过验证的系统集成到一个可靠的组件库中，这些组件可以组合在一起构建无bug的应用程序。这样一个库的存在也将降低验证系统的门槛，最终导致一个验证系统并不比彻底测试系统更昂贵的世界。
数字图书馆是由计算机协会出版的。版权所有©2018 ACM, Inc.
没有发现记录