【图片】回复：【大型专题】计算的极限【chobits吧】

计算的极限（七）：宛如神谕
图灵的哑谜
说到底，谕示是什么呢？我们来看看图灵在他的博士论文中的定义：
“假定我们拥有某种解决数论问题的未知方法；比如说某种谕示。我们不深入这个谕示的本质，除了它不可能是一台机器这一点。通过谕示的帮助，我们可以构筑一种新的机器（叫做o-机），它的基本过程之一就是解决某个给定的数论问题。”
在这里，图灵说的“数论问题”，其实是指描述自然数的一类特殊的逻辑命题，用现在的术语来说叫Π01命题。“数论问题”只是图灵取的一个名字，与真正的数论研究关系不大。
图灵的这段文字其实定义了一种新的图灵机，图灵把它叫做“o-机”，而它的现代术语叫“谕示机”。一台谕示机就是一台有点特别的图灵机，仅仅多了一个新功能，就是能“免费”得到某一个特定的判定问题的答复。比如说，一个带有素数判定谕示的谕示机，除了能做普通图灵机能做的一切事情以外，还能瞬间判定纸带上写的某个自然数是否素数，而不需要实际去计算。
那么，是不是谕示机就一定比普通的图灵机强大呢？就像两位学生参加同一场范围不定的不限时开卷考试，他们的能力与掌握的知识相同，一位学生带了一本参考书，而另一位则什么资料都没带，带了书的那位是不是一定比另一位更有优势呢？

这就要看参考书到底是什么了。如果两位学生都懂参考书中的所有内容的话，那么参考书并不会带来什么优势，可能带书的学生会答得快一些，但既然考试不限时，没带书的学生多用点时间也总能答出来。但如果参考书是两位学生都没有见过的内容的话，带了书的学生自然略有优势。如果考试题目中包含了参考书中的一些内容，而两位学生本来都不懂的话，带了书的可以翻书回答，没带书的就只能干瞪眼了。
同样，在我们比较一台谕示机与一般的图灵机的能力时，也要看看谕示回答的具体问题是什么。如果谕示解决的问题本来就是可计算的话，一般的图灵机即使没有谕示，也能多花点时间把答案计算出来，这时谕示机毫无优势；但如果谕示能解决一个不可计算的问题，比如说停机问题的话，谕示机显然能解决同样的问题，而一般的图灵机则无法解决，因为问题本身是不可计算的，这时谕示机的能力显然比没有谕示的图灵机要强。
所以说，谕示机的力量蕴含在它拥有的谕示能回答的问题，而谕示机中谕示的具体问题可以是任意的。我们可以考虑带有停机问题谕示的谕示机，如果这台机器的纸带上写着一台普通图灵机的“代码”以及输入，那么它不需要计算就能可以瞬间知道，这台普通图灵机遇到指示的输入时到底会不会停机。所以，对于谕示机而言，它不受普通图灵机的可计算性的限制，能够“计算”超越机械计算本身极限的问题。当然，这也意味着，对于一个不可计算的问题，我们不可能实际地建造一台谕示机。
也就是说，谕示机这个概念，只是一个单纯的数学概念，仅仅用于数学上的探索，而不可能实实在在地出现在我们面前。图灵当然也意识到这一点，在他的论文中，也确切声明谕示机并不属于机械计算的范畴。也许这就是图灵使用“谕示”这个名字的原因。“谕示”的原文oracle，来自拉丁语中的oraculum，从orare加上物化工具后缀-oculo得到。orare的意思是“祈求”或者“祷告”，而oracle的意思就是“神的宣布”，也就是神谕。图灵是一位无神论者，他相信神是不存在的，所以神谕当然也不存在。用它来命名一台不可能实现的机器，实在是再适合不过了。

23楼2016-05-14 23:10

正如初中几何证明一样，任何证明都要先列出它使用的公理，也就是说，它默认了什么是“真”的命题。然后，我们知道在肯定前件规则中，如果P和P→Q都是真的，那么Q也是真的，所以我们可以推出Q。那么，只要从公理出发，不停地应用这个规则，因为我们的出发点都是“真命题”，我们通过规则得到的命题也必然是真命题。从真理走向真理，这就是证明，难道不是吗？

的确，一个证明，就是一个从真理走向真理的过程，但这建立于符号的意义之上。如果我们不知道这些符号的意义的话，一个证明又是什么？因为我们已经知道一阶直觉主义命题演算实际上只是日常生活的形式化，所以我们能堂堂正正地说那些公理都是真的。但对于一个从来不知道这些符号的意义的人，甚至是几分钟前的我们来说，这些符号、命题、规则又是什么？当我们遇到一个全新的逻辑体系的时候，我们不知道新体系中的符号、命题、规则到底有着什么意义，这时我们又应该如何看待新体系中的一个证明呢？
不同的逻辑体系有着不同的符号，即使是相同的符号，在不同的体系中也不一定有着相同的意义。如果我们希望找到一个能囊括所有逻辑体系的定义，那么，这个定义中显然不能包含“意义”。但一个剥除了意义的形式体系到底是什么？当“P和P→Q可以推演出Q”的这个规则剥除了它的意义，剩下的又是什么？一个证明，如果剥去它“证明某项真的陈述”的这一重意义，它又是什么？
但如果将形式证明的意义剥除，剩下的不就仅仅是一些无意义的、盲目的符号推演么？当我们看到P和P→Q，我们就能写出Q，仅此而已。本来这个逻辑体系是为了将日常生活中的推理形式化、精确化而存在的，现在要将“日常生活推理”这一意义抽去，只剩下符号搭成的框架，这不是舍本逐末吗？
的确，符号搭成的框架本身没有任何意义。但也正因如此，它可以承载任何意义。已有的逻辑体系蕴含着形形色色的意义，未有的逻辑体系可能蕴含着我们现在无法想象的意义。它们唯一的共同点，就是那个符号搭成的框架。公理就是作为起点的，由符号组成的公式；推理规则就是将一些符号串写成另一些符号串的机械规则；证明就是从公理出发，通过推理规则的不断改写，得到一个新公式的过程。如果有P和P→Q，就写出Q，丝毫不需要思考意义。而在另外一个逻辑体系，如果有P和P→Q，就写出Q→P，这又有何不可？
这就是波斯特的答案：逻辑体系，不过是由一些符号、变量、起始符号串（公理）以及将这些符号串不断改写的规则（推理规则）。它们没有意义，但可以承载任何意义。通过对它们的研究，即使我们完全不知道某个逻辑体系的意义，也能通过对这些符号以及变换的研究，来得到关于这个逻辑体系的一些结论，比如它的一致性（是否存在一些不能写出的符号串），还有它的完备性（是否存在一个符号串，将它添加到起始符号串中就能改写出所有符号串）。只要研究这种完全形式化的符号系统，就能得出关于最广泛、最一般的逻辑体系的结论，无论它们的意义是什么。

作者David Rosenthal，来自http://facpub.stjohns.edu/~rosenthd/

27楼2016-05-14 23:12

计算的极限（九）：叹息与奋斗
时代逝去的叹息
波斯特断言，存在一些形式系统，我们无法在有限的时间内知道其中某个命题能不能被证明或否证。可以说，他的断言与10年后哥德尔的不完备性定理非常相似。那么，为什么在数学史中，“不完备性定理”前面的名字不是波斯特，而是哥德尔呢？因为波斯特虽然在1921年得到这个结果，但要等到1943年，在哥德尔、图灵、丘奇的黄金时代过去之后，才得以在极省略的篇幅下发表。
他没有跟上时代的节拍。
当时的美国数学界普遍对数理逻辑没有太大的兴趣，波斯特与他的导师凯泽在当时算是异类。要等到第二次世界大战前夕欧洲数学家大幅迁移到美国，这种状况才开始改变。波斯特曾经将他的想法写成上下两篇论文，并且将上篇提交到《数学年刊》（Annals of Mathematics）。但他得到的回复十分令人失望，同行评议的报告对是否应该发表各执一词，而编辑部也没有给出具体的决定。如果没有上篇的理论奠基，那么下篇就仅仅是空谈。
但无人问津还不是最致命的问题。实际上，波斯特根本没有一个实打实的证明。也就是说，他并没有实际证明他的结论，那只是一种推测再加上关于证明的一些想法而已。虽然以我们的后见之明来看，他的结论与想法都是正确的，但他毕竟没有一个能让别人详细检验的证明。
在数学界，证明就是一切。没有证明，即使看上去再确定无误的结论，哪怕拥有再多的间接证据，哪怕是最优秀的数学家的想法，都只能是猜想，而不是定理。要确立一个定理，就必须有一个滴水不漏的证明。这就是数学界的规则。而很不巧，波斯特的研究风格比图灵更依赖直觉，换种说法就是更不严谨。波斯特的直觉足以预见超越时代的结论，但他却没有对应的能力来将他的直觉在当下整理为严谨而有条理的证明。他的雄心壮志超越了哥德尔，甚至超越了图灵与丘奇，但他当时没有足够的工具，也没有足够的能力来完成这样远大的目标。
但也许波斯特多花些时间整理他的思路，就能写出完整的证明来说服数学界。可惜命运没有给他这样的机会。
就在波斯特取得突破之后不久，也许是由于这个结果的冲击性太大，他的心理失去了平衡。而论文未能成功发表更是为这种失常雪上加霜。他患上的是双相情感障碍，患者会在无端愉悦与无故抑郁中震荡。此后十多年，他一直受双相情感障碍的困扰，在数学上毫无产出，申请到的大学教职也因为发作而不得不放弃。这段时期，他只能当一名中学教师聊以糊口。直到1935年，他才算是回到了学术界。
从1921到1935，波斯特错过了哥德尔，错过了图灵和丘奇。在他迷惘之时，时代巨轮已经呼啸而过，他错过了数理逻辑的黄金年代。在1941年，他写了一篇文章，详细叙述了他此前在逻辑的不完备性方面的工作，投往了《美国数学期刊》。时任编辑赫尔曼·外尔（Hermann Weyl）拒绝了这篇文章：
我毫不怀疑在二十年前你的工作，部分由于它的革命性，没有得到应有的尊重。但我们无法将时针往回拨；在这段时间，哥德尔、丘奇与其他人完成了他们的工作，而美国数学期刊并不是发表历史回顾的地方。
作为编辑，外尔的决定是正确的。探索的前线并不是向迷失者施予救济的地方，历史才是。历史不会忘记这些被忽视的探索者，他们所有的功绩、辛劳与忧伤。波斯特厚厚的研究笔记，就是历史的见证。当时发生的一切将化为铅字，被人们一遍一遍以不同的形式复述，成为集体记忆的一部分。
为传说撰写诗篇，并一直传颂下去，这就是我们能做的一切。

来自Wikimedia

30楼2016-05-14 23:13

33楼2016-05-14 23:15

无限绵延的层级
波斯特很快就将他的部分发现以摘要的形式发表在1948年的《美国数学学会通报》上。克林读到了这篇摘要，自然为波斯特的新发现而兴奋，但他对这份摘要并非毫无意见。
数学家尽管做的都是数学，但他们的处事方式却是各式各样。在提笔写作方面，有的数学家勤于下笔，每获得了新的结果，就会很快写出论文，并通过期刊或者私下流通预印本的形式让同行尽快知道他的结果；有的数学家却惜字如金，即使有了一整套新结果，也记录了相关的定理和证明，但却迟迟不肯下笔，也许是希望更好地打磨这些结果。著名数学家埃尔德什和欧拉是前者的典型代表，两者分别是数学史上发表论文第一和第二多的数学家。而同样著名的高斯和怀尔斯则是后者的典型代表。高斯是个完美主义者，他希望他的著作中毫无瑕疵，“将所有的脚手架去掉”，于是他发现的结果往往在抽屉里一躺就是几年，直到高斯终于满意他的写作，或者别的数学家再次发现这个结果为止。而怀尔斯独自一人在八年时间内钻研，完成费马大定理的证明主体，这早已传为佳话，被认为是怀尔斯坚韧性格的证明。这些不同的风格，也许在不同的环境下有着不同的适应性，但却没有绝对的对与错之分。
波斯特属于惜字如金的那个类别，但与高斯和怀尔斯不同，他喜欢在发表的论文中提及他已经得到的结果，承诺会写出相关的论文，但这个承诺却迟迟不见兑现的踪影。在他发表的这篇摘要里，他除了提到上述超穷的层级结构之外，还提示了更多的结果。也许波斯特是想吊一下别的数学家的胃口，但对于同样在这个领域工作的人，这很不公平。如果你也是研究这个方向的学者，你读了波斯特的这篇文章，可能希望在这些结论上生发出更深入的定理。但因为这些结论的证明并没有正式发表，你并不知道波斯特的这些结论到底是有凭有据，还是仅仅是虚张声势，从而陷入想用但没法用的两难境地。更糟糕的是，如果你发现了相同的结论，希望发表的话，又会出现优先权之争，而这是大家都不希望看到的。无论如何，仅仅提示结果而长久拖延正式论文的发表，对学术整体的发展相当不利。
克林对波斯特这篇摘要的意见也正在于此。他给波斯特写了一封信，除了赞扬他的结果以及一些讨论之外，还提及了不发表的这个问题。克林的信也许使波斯特的良心有些不安，他很快给克林寄去了一份包含他的新结果的手稿。这份手稿延续着波斯特一直以来的风格：依赖直觉，不太严谨，结构也很凌乱。因为这是一份手稿，混乱程度更甚。波斯特自己可能也知道这一点，他给克林的建议是：找个研究生，让他把内容整理出来，然后以合作者的身份一起发表这篇文章。克林依计行事，但这份手稿实在是太难理解，克林找来的研究生实在无能为力，最后克林只好捋起袖子自己动手。
克林是丘奇的学生，也继承了丘奇的那种追求严谨的研究风格。当年丘奇对严谨性的要求曾经让更依赖直觉的图灵吃了不少苦头，这次轮到克林被波斯特的手稿中的各种直觉描述所困扰了。但最终，克林还是将手稿中的内容整理出来，将缺少的证明补齐，并且做了一些延伸的研究，最后写成了一篇论文：
《递归不可解度的上半格》（The upper semi-lattice of degrees of recursive unsolvability）。
所谓的“递归不可解度”，其实就是不可计算的那些图灵度。而“上半格”是一种序结构。波斯特与克林证明了，所有图灵度其实组成了一个非常复杂但有序的结构。我们此前看到，通过图灵跳跃得到的图灵度层级与算术层级关系非常密切，但与算术层级不同的是，在每个图灵度层级之间，还有更加令人惊讶的结构存在，也就是说，阶梯与阶梯之间并不是空无一物，还有更多的结构蕴含其中。这也是显然的，因为自然数的子集有不可数无穷个，但每个图灵度中最多包含可数个子集。所以，图灵度的个数是不可数的，比我们想象中的无穷还要多得多。图灵度层级必然不能概括所有图灵度的结构，那么，必然有更多的结构存在于层级之间。

35楼2016-05-14 23:17

这篇论文，最终发表在久负盛名的《数学年刊》（Annals of Mathematics）上。可以说，它开创了图灵度研究这个新领域。到现在，图灵度理论已经成为了数理逻辑中非常活跃的一门分支，而其中主要的研究方法——被称为“优先方法”——同样起源于这篇文章。
这就是作为数学家的波斯特，他的数学研究的顶峰。

36楼2016-05-14 23:18

黄金时代
但波斯特并没有能够亲眼在《数学年报》看到他和克林的这篇论文。
双相情感障碍一直困扰着他，即使每天只工作三小时，即使用尽办法平伏情绪，每得到一些新的数学结果，这些发现和创造都让他激动不已，处于症状发作的边沿。对于数学家来说，这可能是最扭曲最恶毒的诅咒。数学家的使命在于发现新的数学，这种发现必然带来的喜悦，对于波斯特来说，却会危及他为了发现数学所必须的清醒头脑。
在1954年初，又一次的发作将他带到了纽约的一家精神病院。当时治疗精神疾病的主要疗法有两种，波斯特接受的是电休克疗法，而同样受精神疾病困扰的另一位数学家纳什接受的则是胰岛素休克疗法。电休克疗法在当时还很原始，虽然以相当高的症状缓解率得到了医生的青睐，但原始的疗法过程痛苦可怕，也有一定的副作用。
在1954年4月21日，波斯特接受了又一个疗程的电休克治疗。在他不停抽搐之时，他的心脏失去了控制。
他没有挺过去。
刊登着他和克林的论文的《数学年报》，则是在5月出版，只差不到一个月。

来自Wikimedia
除了波斯特以外，可计算性理论这个领域的其他开拓者，哥德尔、图灵、丘奇这些先驱，他们的结局又如何呢？
由于二战即将爆发，哥德尔在1939年偕同家人移居到了普林斯顿，恰好在图灵回英国之后。之后，他一直作为普林斯顿的教授活跃在数理逻辑学界。但在四十年代后期，他的关注点渐渐从数理逻辑转移到了哲学，也不再发表他的数学工作。可以说，这就是他的数学生涯的终点。而他的人生的终点要等到近四十年之后。在晚年，他的心理变得不稳定，总是怀疑别人要毒害他。在他的妻子因病入院六个月时，他竟然不接受任何人的食物，活活饿死在普林斯顿的医院里。
图灵在1939年博士毕业后回到剑桥，旋即被英国军方聘用，专注破译德军密码，为二战胜利立下了汗马功劳。在战争结束后，他尝试制造一台计算机，但在英国政府的不作为，被在美国的冯·诺依曼抢了先。除此之外，图灵还提出了有关人工智能的图灵测试，并且一直思考前沿的数学问题。作为一名同性恋者，在被警方发现之后，图灵被迫接受治疗。最后在1954年6月8日，他的生命永远地终止了，床边放着一个沾着氰化物的苹果。
丘奇可能是最幸运的人。他一直在数理逻辑这个领域里奋斗，直到生命的尽头，并且硕果累累。这也许是一名数学家能希望拥有的最好结局。他也是一位优秀的博士导师，门下的31位博士中，就有图灵、克林和罗瑟这样的大师。在生命中困扰着他的，也只有晶状体混浊导致的视力问题，与其他几位先驱相比，实在无足轻重。
正因为丘奇卓越的成果，以及其他人的缺席，他以及他的学生在当时的数理逻辑学界中有着举足轻重的影响。自然，丘奇那种过分追求严谨的作风以及他的λ演算在当时也支配了整个学界。但作为计算模型，λ演算不仅不直观，而且过分形式化，很多实际上很简单的结论，用λ演算证明的话会无比繁复。数理逻辑本来就是一门艰深的学科，证明稍稍复杂一些也相对正常。但当图灵机这样直观的模型出现之后，许多定理换用图灵机模型就能被更直观更容易理解地证明，但许多人由于惯性仍然使用λ演算做研究，即使他们对此也颇有微词。
λ演算在当时的影响之大，就连图灵当时在丘奇门下攻读博士时，毕业论文中用到的计算模型也完全是丘奇的那一套λ演算，尽管他自己提出的图灵机概念更加清晰直观。有些数理逻辑学家甚至认为，图灵的序数逻辑当时不受关注，部分原因要归结于用到了λ演算这套形式语言。就连克林，他自己作为丘奇的学生，也对λ演算很不满意，可能是因为他的文章总是遭到读者的冷遇。他在1935年之后很快就抛弃了λ演算，改为用递归函数的模型来阐述结果，读者的反响果然迅速改善。而丘奇过分严谨的作风对学界的统治，使得图灵和波斯特那种诉诸直观（但能被轻易严格化）的证明，在当时被视为异类。
学界的惯性是强大的。丘奇在1935年提出λ演算，而他追求完全严谨的作风对学界的统治要直到五十年代中后期才开始慢慢松动。其中有两个原因：第一是随着可计算性理论的发展，这个领域的定理越趋复杂，λ演算这个框架在严谨性方面带来的好处，逐渐被它的复杂性所抵消；第二是随着基于图灵机模型的现代计算机的发展，人们对图灵机越来越熟悉，对图灵机的研究也越来越深入，人们对于图灵机模型的使用也越来越得心应手。这两个因素一推一拉，渐渐改变了学界的风气。时至今天，在可计算性理论中，人们更偏向于使用图灵机，而λ演算早已不见踪影。但λ演算并没有就此消失于学术界，人们很快就发现它的另一个用武之地，但这是后话，留待后文详述。
哥德尔、图灵、丘奇、波斯特、克林……这些开创者们，告诉了我们“计算”到底是什么，而计算之外又有什么。我们今天能惬意地躺在床上用平板电脑看视频打游戏，能与千里之外的朋友互通消息，也都部分地归功于他们打下的理论基础。但平心而论，我们给这些开拓者的颂扬还远远不够。在一般人心中，他们仍然寂寂无名。这些开拓者们，生前大多没有什么好的结局，就连死后也没有得到多少廉价的赞赏。他们为我们开拓了一个信息化自动化的黄金时代，但他们又得到了什么呢？
但也许他们也并不在乎。就像少年的波斯特那样，也许在他们眼里，数学比尘世间的一切都要美丽，只有万亿光年外宇宙的奇迹才能与之媲美。

图片来源：NASA
这就是信息时代开拓者们的故事。

37楼2016-05-14 23:19

当然，数学家并不会停止他们探索的脚步。可计算性理论的下一篇章，将会在大洋彼岸被揭开。但在继续追寻之前，我们先来看看，这些开拓者们的遗产到底给我们的生活带来了什么。

38楼2016-05-14 23:19

形式证明
有一种激进的做法：让程序员在编写代码的同时，给出这段代码确实完成了给定任务的数学证明。
要给出这种证明，首先要解决的就是如何将“代码完成了给定任务”转换成数学命题。程序代码可以相当容易用逻辑表达，但代码需要完成什么任务，这只有程序员才知道。所以，要让程序员在编写代码的同时给出证明，为的是让程序员能用逻辑的形式确定这个函数的功能，如此才能得到要证明的命题。这种想法不仅仅是数学家的纸上谈兵。对于某些关键系统，多么微小的疏失都会导致极其严重的后果，人们愿意几乎不惜一切代价防止错误的发生，而对于计算机程序而言，又有什么比数学更坚实的基础呢？
要贯彻这种想法，在编写程序之前，必须先选择一种逻辑体系以及描述它的一种形式语言。这种形式语言必须贯穿整个代码编写的过程：先用形式语言描述程序的输入、输出、功能与限制，然后利用这种与形式语言相近的编程语言去具体编写代码，最后还要利用形式语言给出编写的代码能完美无瑕疵地实现所需功能的数学证明。这种做法又被称为演绎验证，是所谓的“形式化验证”的手段之一。
但数理逻辑毕竟不是一门容易的学科，数学证明对于很多人来说大概比编写代码要困难得多。所以，演绎验证多数也只会用在那些不容有失的关键系统，比如说牵涉人数众多的公共交通设施。例如，在1998年开始运营的巴黎地铁14号线，就是一条全自动的地铁，列车上没有司机，安全行驶也全靠传感器和软件，调度也只需要在控制室点点鼠标就能增加或减少投入运营的列车数量。于是，安全在很大程度上在于软件的可靠性。在控制列车的计算机中，某些与乘客安全休戚相关的关键代码是利用演绎验证编写的。在2012年，巴黎历史最悠久的地铁1号线也从人工运营转到与14号线同系列的全自动化系统。现在，这两条地铁线每天接待的人数加起来超过一百万，但从未因为自动化系统的错误导致乘客伤亡。从笔者的经验来说，它们可以算是巴黎最可靠的地铁线。

巴黎地铁14号线，图片来自Wikipedia
但仅有代码的正确性可能还不足以保证程序同样正确，因为代码毕竟不是程序，计算机不能直接执行代码。我们需要另一种名为“编译器”的程序。编译器是将程序员写的代码翻译成计算机能读懂的、用机器语言写就的程序。即使代码是正确的，如果编译器有问题，得出的程序还是可能出错。要避免这个问题，我们同样需要利用数学方法加固编译器这一环。
贯彻这种设计理念的一个例子是一个叫CompCert的C编译器，它由法国计算机科学家Xavier Leroy和他的小组编写。编译器的任务就是进行忠实的代码翻译，确保源代码和目标代码的行为一致。这一点至关重要，否则即使代码是正确的，也不能保证编译生成的程序不出问题。然而，现代的编译器在优化模式下，其实并不能确保忠实的编译。CompCert要解决的就是这个问题。在编写CompCert的时候，对于编译程序的每一步操作，都附带一个数学证明，确保代码的语义不变。因此，数学证明的正确性保证了CompCert编译器会完全忠实地将代码翻译成机器语言。
但即使机器语言是正确的，也还不能完全保证最后执行结果的正确性，因为程序总需要输入输出，而这些功能是由操作系统保证的。如果操作系统本身有错误，即使执行的程序本身是正确的，由于操作系统的问题，也不能保证我们看到的结果是正确的。如果想将数学证明的保证贯彻到底，还需要对操作系统下工夫。这就是seL4所做的事情。seL4是一个微内核，可以看成操作系统的核心。它的每一个功能都附带一个数学证明，在对硬件做一定的假设之后，数学证明的正确性可以保证它提供的功能都会产生我们预先设定的行为。只要硬件不出错，seL4就会正确运行。
当然，一个自然的问题是，如果硬件出错怎么办？硬件的错误可以分为逻辑性错误和物理性错误。前者例如Intel当年在芯片上除法的错误，现在主流硬件厂商早已吸取教训，用演绎验证的方法加固他们的硬件设计；后者例如宇宙射线令硬盘数据出错，这即使是多复杂的证明也避免不了，只能自求多福。尽管数学方法不能保证错误不存在，但至少将可以避免的问题全数避免，这本身就有着莫大的价值。

（或者可以利用宇宙射线……？）（图片来自xkcd）
未完待续.......

41楼2016-05-14 23:20

计算的极限（十二 A）：数字空间的幽灵
当汤玛斯（Robert Tomas）在1971年写下他的“小小实验”所用的代码时，肯定不会想到，他写下的Creeper代码会开启数十年后的一门“黑色产业”。现在，面前的计算机上，掌心的智能机中，广阔的互联网内，有着无数幽灵飘来荡去，凯觎一切有价值的信息，操纵一切能**纵的机器。这是一个庞大的产业，而同样庞大的是为了防御这些幽灵而生的守护者。计算机病毒和杀毒软件，两者你追我赶，永无止尽。注定这两者命运的，正是一条数学定理。
到处乱窜的代码
在计算机发展的早期，计算资源非常珍贵，只有军队或者大学才拥有计算机，还要排队才能用上。但如此宝贵的计算资源有时候却会被白白浪费。计算机不需要休息，但是人却必须睡眠。人不在的时候，计算机往往就空下来了，这就造成了需求的不平均。有某些计算需要特定的数据，但如果只为了一次计算去传输未免太浪费，这就是数据的不平均。要想将计算资源压榨到最后一滴，就需要消除这些不平均的因素。用现代术语来说，就是负载平衡的问题。
1969年见证了一样新奇事物的诞生。为了共享资源，美国军方开发了阿帕网（ARPANET），旨在将散落在美国各地的军用计算机连结起来。那就是网络的石器时代。我们现在习以为常的各种概念，比如说电子邮件、网络协议等等，当时还不存在。程序员手中所掌握的，就是几台大型计算机，以及连结它们的简陋而原始的网络。
但条件匮乏并不能阻碍程序员的脚步，他们是开辟新天地的先锋。既然信息可以在网络中流动，那么运行的程序本身可不可以在计算机之间转移呢？可行的话，某个程序在一台计算机繁忙的时候，可以自动跳到空闲的计算机上，而如果这台计算机上没有需要的数据，它也可以自动跳到有相应数据的计算机上执行。“程序自动转移”的这个想法，一下子就能同时解决需求和数据不平均的问题，岂不美哉？
当时汤玛斯在一间名为BBN的公司里，与同事为阿帕网内的计算机编写操作系统。这个操作系统叫TENEX，其中内置了网络功能，汤玛斯琢磨着，能不能利用相应的功能，写出一个能自动转移的程序呢？
他成功了。
他写了一个叫Creeper的程序，功能很简单：首先在当前计算机上读取一个文件，然后寻找网络上的另一台计算机，将程序本身和附带的文件都打包传送过去，在当前计算机上删除自身，最后留下一句话：
I'M THE CREEPER : CATCH ME IF YOU CAN.
（我是CREEPER：有本事就来抓我吧。）

-说我？ -走开，不是说你！ -不开心，要炸了……（图片来自gamepedia）
Creeper说明“程序自动转移”确实可行。但问题是，放出来的Creeper不太好收拾，一时间它在阿帕网上跳来跳去，令人烦心。
但糟糕的还在后头。没几天，新版本Creeper出现了，它在传送的时候不会在原来的计算机上删除自身，也就是说它将自己复制到了另一台计算机上。据说始作俑者是汤玛斯的同事雷·汤姆林森（Ray Tomlinson）。可以说，新版本的Creeper满足了广义上病毒的定义：在用户不知情的情况下自我复制的程序。
跟所有病毒一样，新版本Creeper也惹来了大麻烦：它很快就感染了网络上的所有计算机，而且即使人们在一台计算机上将它清除，也很快会受到来自网络上另一台计算机的感染。也许是为了人道主义的补锅，汤姆林森很快写出了另一个名为Reaper的程序，它基本上就是Creeper的变种，会以同样的方式感染网络上的计算机，但在感染完成后，会尝试移除计算机上的Creeper，最后自行关闭。
这就是第一个计算机病毒。

46楼2017-12-11 00:09

从玩笑到犯罪
在计算机发展的早期，因为用户群体相对小，宵小之徒还没来得及盯上这个领域。当时大部分病毒被编写出来的目的，其实是为了炫耀技术，或者搞搞无伤大雅的恶作剧。所以，当时的计算机病毒通常不会造成什么大损失，而且经常带着一丝幽默。比如说1982年出现的Elk Clone病毒，“危害”就是会自动显示一首诗。还有1990年前后肆虐的Cascade病毒，就会使终端命令行的字符“掉下来”（当时的界面也差不多只有命令行）。这些病毒都是通过软盘传播的，现在已经成为了时代的眼泪。
另一些病毒则是阴差阳错的结果。比如说第一个木马病毒ANIMAL，它在1975年出现，本体是一个猜动物的小游戏。为了进行自动更新，作者另外编写了另一个小程序PERVADE，执行时会将自身和ANIMAL复制到当前用户能访问的所有文件夹之中，包括共享文件夹，与其他用户共享。每当用户运行ANIMAL游戏时，它会自动执行PERVADE程序来完成复制，通过共享文件夹，整套程序就完成了从用户到用户的感染。要放到现在，这应该就叫P2P自动更新推送。另一个例子就是1986年出现的Brain病毒，本来是防盗版措施，但在作者加入自我复制的功能之后，它就成了名副其实的病毒。
随着计算机的普及，奸诈之徒也开始出现，病毒也越来越有破坏性。强行关闭计算机和删除文件自然不在话下，加密文件以勒索赎金也早就有人干过。甚至直接破坏计算机硬件的病毒也出现了，比如臭名远扬的CIH病毒，是经历过上世纪90年代洗礼的人们心中难以拂去的梦魇。
进入21世纪之后，犯罪分子编写病毒的目的也逐渐改变，从单纯的破坏转为牟利。将感染转化为利益有很多方法，最直白的就是勒索软件，它们通过强大的加密“劫持”重要数据和操作系统这些“人质”，只有受害者支付一笔“赎金”之后，才能“赎回”计算机的正常使用。最近的WannaCry就是一个例子。另一种方法就是搜索和截获信用卡的账号和密码等有价值的信息，然后直接通过这些重要信息牟利。还有一种方法就是操纵被感染的机器，把它们用在其他恶意用途上，比如DDOS[link]或者发送垃圾邮件，而黑客可以出售这些“服务”来牟利。无论哪种方式，都是一本万利的生意。

重利之下，病毒的始作俑者也变得团队化和全球化，对信息安全造成了重大威胁。只要是可以运行程序的机器，他们都不放过，比如新近出现的物联网，由家用电器组成的网络。因为物联网上的设备通常疏于更新而且留有后门，入侵起来实在易如反掌。目前最大的僵尸网络Mirai（日语中意即“未来”），大部分就是由物联网设备组成的。就规模而言，似乎这个模式的确是恶意软件的未来。
盯上病毒的除了贼还有兵。为了进行情报活动，各大国对计算机安全的研究都进行了巨大的投入，编写出前所未有精巧的新病毒，危险性远远超出了犯罪团伙。最近美国国家安全局“囤积”的大量漏洞和黑客工具被泄露，更是说明了国家力量可以造成多大的损失。其中仅仅一个漏洞“永恒之蓝”（Eternal Blue），就给我们带来了WannaCry这个勒索软件，使世界各地的许多机构陷于瘫痪。
有矛必有盾
有无相生，先后相随。既然有病毒，用户就有清除病毒的需要，也就有了杀毒软件。可以说，杀毒软件追随着计算机病毒而生。杀毒软件的任务就是识别并清除病毒。
面对如此麻烦的病毒，人们自然想追求一劳永逸的解法。是否能写出一个完美的杀毒软件，它不仅能查杀一切已知的病毒，还能查杀以后可能出现的任何病毒呢？
然而，牵涉到判断计算机程序具体行为的问题，基本上都是不可能完美解决的。我们之前已经看到，不存在一个程序能够判别任何一段代码在执行时是否会出错。同样，不存在这样的杀毒软件，能完美无缺地辨别任何计算机病毒，不论是已知的还是未知的。这实际上是Frederick B. Cohen在1987年证明的定理，他又被誉为计算机病毒防御技术的创始人。对于本系列的读者来说，这个定理其实是停机定理的推论，这也许并非意料之外。
所以，对于任何杀毒软件来说，下面两种情形至少有一种会发生：要么把正常的程序当作病毒消灭了，要么在眼皮底下放过病毒，前者叫误杀，后者叫漏杀，两者此消彼长。当然，不存在完美的杀毒软件，并不阻碍我们精益求精，做出越来越精密的杀毒软件。再加上逐利不竭的犯罪分子，可以说，杀毒软件这个行业永远不会停止发展。
那么，人们是如何一步一步改进杀毒软件的呢？杀毒软件的目标，在于区分正常程序和计算机病毒。不同的病毒查杀技术，实际上就是各种将病毒从正常程序中区分出来的方法。
最早的杀毒软件可以追溯到1987年，当时的病毒很简单，数量也很少，要将它们同正常程序区分开来也很简单。当时的病毒通常有一些特定的程序代码，用以执行感染和发作的步骤。安全研究人员可以先定位并提取不同病毒中这些有特征性的代码（又称为“特征码”），放到杀毒软件的数据库里。杀毒软件的工作，就是检查每个文件是否存在相应病毒的特征码，如果存在，这个文件十有八九就包含了病毒。

47楼2017-12-11 00:09

幻化万端难辨识
但道高一尺，魔高一丈。病毒的制作者当然也观察到了这样的现象，他们开始想尽办法制作不同的变种，改变病毒的代码，比如在病毒体内加入没有实际效用的所谓“花指令”，或者将不同的指令变换为功能相同的指令，以此躲避杀毒软件的检测。但这样的手段，即使一时骗过了杀毒软件，在新病毒被研究人员捕获并分析之后，杀毒软件很快就能更新到能查杀新的变体。
病毒制作者自然不会善罢甘休。既然特征码针对的是病毒代码之中的固定部分，那么如果病毒在每次传播时，具体代码都会改变，那不就能逃脱特征码查杀的套路了？沿着这种思路开发的病毒，又叫自修改病毒。
最早的自修改病毒叫1260，早在1990年就出现了。它由两个模块组成：代码模块和解密模块。代码模块平时是被加密压缩的，而病毒在被激活时，会先运行解密模块，把包含真正的感染和破坏指令的代码模块解密，然后再去执行代码模块。而当病毒感染其他文件时，会随机打乱解密模块的部分内容，形成新的解密模块，然后用它来将代码模块重新加密。这种复杂的构造，就能保证每次感染时出现的病毒体都与以往完全不同，大大增加了查杀的难度。这种相对简单的自修改病毒，又叫多态病毒（polymorphic virus）。

然而这种小技巧并没有难倒安全研究人员。就像自然界中真正的病毒那样，多态病毒即使变异很快，仍然有一些至关重要的部分保持相对稳定，那就是解密模块。研究人员很快就学会了利用解密模块的特征来识别多态病毒。迫使多态病毒采用更多措施来打乱自身代码，比如说自动加插花指令和进行等价指令的替换，又或者是自动重新排列自身的代码。但安全研究人员很快就想出了反制的办法，毕竟这些改动都不算大，检测也不算困难。
最后病毒制作者只剩下一个希望：写出一个病毒，在每次感染时，病毒的几乎每一段代码都会产生重大改变。这样的话，就不可能在代码的层面上探测出这个病毒了。
说得轻巧，但具体怎么做呢？
黑客们想出了一条可谓破釜沉舟的计策：每次要感染新文件时，先把病毒本身转换为某种“中间代码”，然后将中间代码用另一种完全随机的方式编译，得到的就是全新的病毒代码。这种中间代码可以有无数种编译方式，但得到的代码执行时的行为都完全一样。以这种方式编写出来的病毒，又叫变形病毒（metamorphic virus）。通过先转换为中间代码再编译的方式，它们“变形”得到的具体代码千变万化，但具体的行为却完全一致。
最有名的变形病毒叫Simile，在2002年第一次出现，当时给安全研究人员带来了很大的麻烦。正因为它可以“变形”为与之前完全不同的代码，这使得特征码提取的方法基本失效。幸而变形病毒的研发非常复杂，尤其是“变形”所需的代码非常复杂（Simile中有90%的代码专门负责变形），所以变形病毒数量相当少。但即使变形病毒的门槛很高，随着技术的进步，也终会有普及的一天。即使是为了未雨绸缪，也应该想办法开发新技术去对付这种新型病毒。

48楼2017-12-11 00:10

听其言，观其行
不久之后，安全研究人员想到了两个办法，它们的核心思想都很简单。变形病毒改变的是它们“外在”的代码，但“内在”的行为，也就是病毒具体会做什么，却是不会改变的。如果有办法拨去具体代码的面纱，探测它们的“实际行为”，也就是语义，岂不是就可以成功查杀这些病毒了么？
第一个方法，就是尝试将变形病毒的“变形”过程还原，尝试将它们固定到同一个形式中。研究人员首先将变形病毒的代码拆解出来，然后用程序分析它的逻辑结构。因为变形病毒无论怎么变形，它的功能是不变的，所以具体的逻辑结构也不会有太大的变化。只要能识别它逻辑结构中不变的部分，就能识别同一类的病毒，无论它们怎么变形，代码有多不同。当然，分析一段代码的逻辑结构并不容易，研究人员借鉴了当时编译器的某些优化编译功能，可以将没有用处的指令剔除，也可以分辨出那些本质上等价的代码。最终结果相当成功，通过分析逻辑结构本身，就能有效查杀那些变形病毒。
研究人员想到的第二个办法更加直接。既然我们想要探测病毒的“实际行为”，那么何不让它实际“运行”一下，看它会做出什么举动？当然，我们不能在用户的计算机上实际运行可疑文件，否则如果可疑文件的确是病毒，那么麻烦就大了。研究人员做的，就是模拟一个病毒可以运行的环境，又叫“沙盒”，然后在这个环境中模拟病毒的运行，观察它的行为并记录下来。病毒通常会有一些特征行为，比如多态病毒就会访问并改写自己的代码，而变形病毒则会执行“变形”步骤。对于杀毒软件来说，对于可疑的程序，它可以先在沙盒中模拟这个程序，如果观察到的行为符合某个病毒的特征行为，那么这个程序很有可能就包含病毒。这种技术又叫沙盒查杀技术。但因为在沙盒内运行程序需要消耗不少的计算资源，所以只能用在一些特别重要的位置或者特别可疑的文件上，比如系统文件和内存。

“沙盒”原本是供小朋友游玩的设备，无论弄得再乱七八糟，也只是沙盒内部的事
实际上，沙盒查杀技术的用途不止于此。因为它检测的不是具体的代码，而是程序的行为，所以从理论上来说，这种技术能够用于检测未知病毒，走在病毒编写者的前面。不同的病毒会有不同的特征行为。有的病毒会检查操作系统的语言和当前时间，然后决定是否进行感染；有的病毒会尝试将自身注册为操作系统的底层驱动，用以隐藏自身；有的病毒会尝试枚举所有程序，准备感染它们；有的病毒会枚举特定文件然后进行加密，这是勒索的必备步骤。不同的行为有不同的风险，面对可疑文件，杀毒软件可以先在沙盒中运行它们，记录它们的行为。如果这些行为大体类似某个已知病毒，那么这个文件就可能包含病毒。即使没有检测到相应的病毒，如果记录到的行为过于危险可疑，杀毒软件也可以对它进行标记和隔离，以供进一步研究。这就是所谓的“启发式查杀技术”。确切地说，使用沙盒的是动态启发式技术，但也有所谓的静态启发式技术，只需要观察文件的代码，而不需要具体执行。利用最近兴起的机器学习技术，安全研究人员还能进一步提高启发式技术的可靠性。
启发式技术虽好，但并非无懈可击，因为它不能完全确定检测结果是对是错，有可能会误杀正常程序，毕竟很多正常程序，尤其是系统底层的驱动程序，也会作出与病毒相似的某些行为，但它们并不是病毒，而且对于计算机的正常运行至关重要。误伤这些文件会导致很多问题，而偏偏病毒倾向于感染这种贴近底层的文件来逃避侦测。我们有时会听到这样的消息，某款杀毒软件在更新后突然干掉关键系统文件，而且是成片发生。比较极端的，甚至还有解放军在演习中武器系统被杀毒软件咔嚓了的事件。但随着技术的发展，目前这些意外已经越来越少，杀毒软件的功能也越来越强大，查杀技术也越来越精确。
在杀毒软件和病毒的斗争之中，沙盒技术和启发式查杀技术有着重大的意义，因为它第一次让安全研究人员能部分走在病毒制作者的前面。在它出现之前，杀毒软件只能跟在病毒后面亦步亦趋，但有了这项技术，病毒制作者也就不能随心所欲编写新病毒，而要对市面上的杀毒软件进行一番研究，才能保证自己的新病毒不会在沙盒中被启发式查杀干掉。事实上，现在相当一部分的病毒被查杀时，仅仅会被识别为“一般病毒”（generic virus），因为阻止它们的是启发式技术，不需要具体识别它们的类型。
现在摆在病毒制作者面前的就是这样一个问题：怎么样才能躲过沙盒技术呢？也就是说，有没有办法在执行的时候，让病毒“意识”到自己身处沙盒而不是一台真正的电脑之中呢？
办法不是没有。既然沙盒是一种需要大量资源的模拟，为了减少资源的使用，杀毒软件的沙盒必定会有某种破绽。比如说，如果沙盒对于模拟的系统时间没有特殊处理的话，因为沙盒的模拟比真正的执行要慢，所以病毒可以通过测量执行某段代码所需的时间来得知自己是否处于沙盒之中。一旦安全研究人员发现有利用这种缺陷的病毒，他们就可以修正缺陷，重新取得先机。在这个战场上，亦步亦趋的不再是安全研究人员，而是那些病毒制作者。
但沙盒毕竟是模拟环境，总会存在破绽，病毒也可以等待一段时间再发作，以此逃避杀毒软件的检测。有些安全研究人员就有了一个大胆的想法：何不让要检测的程序自由运行，等到出现了可疑的行为再查杀不迟？毕竟病毒要复制和传播，必然要进行某些特定的操作，比如说读取其他程序或者调用某些特殊的系统函数。只要在病毒作出这些操作的瞬间进行拦截，那就没有问题了。这就是行为检测技术，要做到这一点，杀毒软件需要利用特殊的技术（Rootkit）监测所有应用程序的一举一动，在它们请**作系统进行任何任务时，拦截并分析具体的请求。这种技术一开始是病毒用以隐藏自身痕迹而开发的，现在反而成了杀毒软件的武器。
永无休止的斗争
当然，杀毒软件的技术再好，也不能保证绝对的安全。越好的查杀技术，通常使用的资源也越多。如果对每个文件都采取最高级的查杀技术，那肯定会大大拖慢系统的运行速度，所以在具体编写软件时，安全研究人员需要进行适当的取舍。既然有取舍，那就会有漏洞可供利用。另外，病毒制造者也可以先下手为强，感染时想办法先把杀毒软件干掉，或者利用操作系统本身的漏洞取得整个系统的主导权，直接架空杀毒软件。互联网技术发达之后，杀毒软件厂商可以让杀毒软件自动上报可疑文件，尽早获得新病毒的资料；病毒制作者也可以让病毒自动更新，不停逃避杀毒软件的追杀。病毒和杀毒软件的攻防战线广阔异常，从磁盘到内存甚至显卡，都是它们的战场，而攻防策略之多，无论如何列举都只能是挂一漏万。
但尽管杀毒软件现在已经成为非常成熟的技术，病毒要感染计算机，也还有别的路可以走。操作计算机的毕竟是人，跟杀毒软件相比，人的“漏洞”更多，更容易被利用。有多少人嫌麻烦不去更新系统填补漏洞，给病毒以可乘之机？又有多少人看到“请查收文件”的邮件，就急匆匆点开附件，丝毫不检查文件的来源和性质？还有多少人用的密码就是123456，或者上网看到什么链接，无论多么可疑都点进去看看？一个系统的安全，取决于最薄弱的环节。如果没有信息安全的意识，杀毒软件再好，也挡不住人类作死的脚步。

49楼2017-12-11 00:10

收起回复

日	一	二	三	四	五	六

回复：【大型专题】计算的极限

登录百度账号

扫二维码下载贴吧客户端