【程序安全百分百】系列文章

第一章:笑傲代码江湖

TODO:

  • [ ] 前言

      - [ ] 语言的能力(什么是语言?《人类简史》,人类语言的诞生,意识的表达,语言的不正确性)
      - [ ] 计算机语言的发展(举例,C)
      - [ ] 犯错的人类(举例)
      - [ ] 逻辑的诞生(三段论,引出逻辑系列文章:谓词逻辑,一阶逻辑,费马大定理,高阶逻辑,霍尔逻辑,分离逻辑)
    
  • [ ] 确保程序安全的各种手段

      - [ ] 软件测试
      - [ ] 模型检测
      - [ ] 定理证明
    

语言都会有真假吗?

谎言和真理似乎是对立存在的,有假,真才会有意义。人类的语言

本文粗略探讨人类语言的局限性和模糊性,以及计算机程序语言的安全与否,程序分析是怎么一回事。

语言的本质

万物诞生后的很长一段时间里,一切都没有名字,每个元素和细胞都没有代号,树就那么长着,云就那么飘着,天就那么亮着,仿佛并不在乎自身的存在。而后,它们被给了代号,只要文字中还没有可用的,新的就会被加入。而那些被人类用还未成熟的文字给予的最初名字,往往最附诗意,最带温柔,仿佛女孩出现的第一眼,仿佛夏天的第一夜。

海德格尔说语言是存在的家。语言(文字)的本质是符号系统,给所有存在不存在的能感知的不能感知的万物都贴上一个标签,所有标签的集合就是一种语言,中文贴“苹果”,法语贴“pomme”。地球上初始的生命还未有语言,还未有意识,生命的进化过程中语言和意识也在进化和升级,语言的存在是为了更好的生存,深层的奥秘还存在于生命密码中,书写爱情之诗的本意,其实是基因中为了提高繁衍的使命。

语言的模糊性,语言的真假

只要是使用到语言,很多围绕人本身的问题就出现了。语言是万能的吗?语言能够描述脑中意识所有的想法吗?如果语言的目的是交流,交流的目的是欲望,欲望的目的是生存,生存的本质是性,那老弗(弗洛伊德)又要笑醒了吧……人类的语言,诞生之后,语义是有局限性的,或者说,一句话是带有模糊性的,有一个著名的例子就是说谎者悖论。

圣经中的说谎者悖论

说谎者悖论 又叫谎言者悖论。公元前六世纪,克里特人的哲学家埃庇米尼得斯(Epimenides):“所有克里特人说的都是谎言。” 如果埃庇米尼得斯所言为真,那么克利特人就全都是说谎者,身为克利特人之一的埃庇米尼得斯自然也不例外,于是他所说的这句话应为谎言,但这跟先前假设此言为真,互相矛盾;假设此言为假,那么也就是说有部分克利特人是不说谎的,则表示埃庇米尼得斯说谎,仍符合假设(即埃庇米尼得斯属于克利特岛的人中说谎的部分),因此这句话一定为假。

逻辑学家塔斯基(Alfred Tarski)认为此悖论的出现是由于语言的“语义封闭性”。所谓“语义封闭性”是指一语言中的一语句被同一语言中另一语句(或者该语句自身)的真理述词指涉“为真”(或“为假”)。

但也有一些逻辑学家认为,说谎者悖论从严格的意义上来说,并不是真的是个悖论,悖论是指从为真的前提推导出矛盾的结论,而说谎者悖论中的那句话本身自始就隐含矛盾而为假,所以并不是悖论。不管是否是悖论,直觉上,这跟描述的对象集合有关系。

罗素悖论(Russell’s paradox)

类似的数学意义上的问题是英国哲学家罗素(Russell)1901 年提出的悖论,罗素悖论的提出,导致了第三次数学危机。

罗素悖论:给定一个性质 P,满足性质 P 的所有集合可以构成一个集合 S,

理发师悖论:南京路理发师 Tony 放出豪言:他只为,而且一定要为,上海滩所有不为自己刮胡子的人刮胡子。

但问题是:Tony 该为自己刮胡子吗?如果他为自己刮胡子,那么按照他的豪言“只为上海滩所有不为自己刮胡子的人刮胡子”他不应该为自己刮胡子;但如果他不为自己刮胡子,同样按照他的豪言“一定要为上海滩所有不为自己刮胡子的人刮胡子”他又应该为自己刮胡子。所以,结论是,这样的 Tony 不存在。

罗素悖论用数学的形式来描述就是:

R=x:xX;R = {x:x \notin X};

这个悖论最初是从康托尔的无穷集合论里面引申出来的。当初康托尔在思考无穷集合的时候发现可以称“一切集合的集合”,这样一个集合由于它本身也是一个集合,所以它就属于它自身。也就是说,我们现在可以称世界上存在一类属于自己的集合,除此之外当然就是不属于自己的集合了。而我们把所有不属于自己的集合收集起来做成一个集合R,这就是上面这个著名的罗素悖论了。

Ouroboros

  1. 绝对没有绝对的事情。
  2. 从前有家饭店,只卖包子和馒头,这时候假设存在一个聪明的侍者,这个侍者可以判断任何一个前来点餐的客人要点什么菜,这时候有个腹黑的家伙说:“如果你判断我要点包子,那我就点馒头;如果你判断我点馒头,那我就吃包子。”所以这样的侍者是不存在的。

同样的问题其实也在计算理论中出现,也就是停机问题。艾伦·图灵在 1936 年用对角论证法证明了不存在解决停机问题的通用算法,美妙性不言而喻。

数学家对命题和演算总是充满热情。莱布尼茨很早就想制定一张字母表,字母表中的元素都是概念,有这样一个符号系统,就可以发展出一种语言,我们仅凭符号演算,就可以确定用这种语言写成的句子是否为真,以及句子与句子之间存在着什么样的逻辑关系。

在计算机的世界里,程序语言可以看成是逻辑,逻辑系统是语言的子集,既然是逻辑,就是无懈可击的,没有二义性,简单直白,这些当然都是数学的特点(因此,通常数学家和物理学家都看不起计算机)。

逻辑系统的起源要归功于两千多年前的亚里士多德建立的形而上学的基础,其开创的传统逻辑在逻辑学中独领风骚数千年,后来逐渐演变成现在的谓词逻辑。

逻辑推理和三段论式的证明也成为王小波在《黄金时代》中书写幽默的方式。

程序的真假

Pascal 语言之父 Niklaus Wirth 在 70 年代提出:Program = Data Structure + Algorithm,随后逻辑学家和计算机科学家 R Kowalski 进一步提出:Algorithm = Logic + Control。我个人当然赞同后者了。程序由一堆指令组成,用以表达工程师的想法,当然表达一个想法可以有不同的指令组合,对于一个问题,能找到最优的指令组合,也就找到了最后的算法解。

程序的目的

1673 年,莱布尼茨在巴黎为某个贵族服务,期间去过英国访问。在第一次访问时,就展示了一台能够执行四中算术基本运算的计算机模型,凭借这一模型,莱布尼茨被推选为伦敦皇家学会会员。

在刚开始学编程时,我们一般通过测试来验证我们的程序,比如执行一次程序,得到执行结果,看跟自己心中期望的结果是否相同。这可以看成是简单的软件测试思路。通过测试来判断软件的正确性在工业界取得很高的效率,一般的软件公司都有两个大部门,一个是软件开发,一个是软件测试。软件测试是不严谨的手段,并不能确保软件百分百的正确,因为程序的状态空间有可能是无限的,因为有无限状态,测试就不可能穷尽所有的可能。1996年,欧航局的 Ariane 5 发射40秒后爆炸,爆炸的原因是软件中,变量从float类型转换到integer类型时溢出。这种错误,是测试很难发现的。

 欧航局研制的Ariane 5 爆炸

1
2
3
4
5
// Ariane 5 系统中含有漏洞的代码

P M DERIVE(T ALG.E BH) :=
UC 16S EN 16NS (TDB.T ENTIER 16S
((1.0/C M LSB BH) * G M INFO DERIVE(T ALG.E BH)));

现代的静态分析器对除零问题(division by zero)都已经有了很好的支持。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
// frama-c 
#include <stdlib.h>

int test() {
int x, y = 2, z = 3;

if (y >= 2) {
x = rand();
z = x / (x - 1);
} else {
x = 1;
z = x / (x - 1);
}
return z;
}
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
[value:initial-state] Values of globals at initialization
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_mblen_state ∈ {0}
__fc_mbtowc_state ∈ {0}
__fc_wctomb_state ∈ {0}
[value] using specification for function rand
1.c:8:[value] warning: division by zero. assert (int)(x - 1) ≢ 0;
[value] done for function test
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function test:
__fc_random_counter ∈ [--..--]
x ∈ [0..32767]
y ∈ {2}
z ∈ [-32767..32767]

保证程序安全的几种手段

软件测试

将程序转化为公式

抽象和数理建模