Security

静态分析 静态分析（Static Analysis） 是指在实际运行程序 $P$ 之前，通过分析静态程序 $P$ 本身来推测程序的行为，并判断程序是否满足某些特定的 性质（Property） $Q$ 。 缺陷检测问题 给定某程序 $P$与某种类型的缺陷（如内存泄露），输出程序$P$是否存在给定类型的缺陷。 我们可能关注的程序性质（缺陷）可能有： 程序P是否会产生私有信息泄漏（Private Information Leak），或者说是否存在访问控制漏洞（Access Control Vulnerability）； 程序P是否有空指针的解引用(Null Pointer Dereference)操作，更一般的，是否会发生不可修复的运行时错误（Runtime Error）； 程序P中的类型转换（Type Cast）是否都是安全的； 程序P中是否存在可能无法满足的断言（Assertion Error）； 程序P中是否存在死代码（Dead Code, 即控制流在任何情况下都无法到达的代码） 是否存在算法能给出该判定问题的答案？ 软件测试？ “Testing shows the presence, not the absence of bugs.” ——Edsger W. Dijkstra 希尔伯特计划 “Wir müssen wissen, wir werden wissen.” ——David Hilbert (我们必须知道，我们必将知道) 1900 年，38岁的希尔伯特在巴黎举行的第二届国际数学会议上以“数学问题”为题的演讲中提出了23个重要的数学难题，即众所周知的“希尔伯特问题”，激励和推动了后来一个多世纪许多数学分支的蓬勃发展。简而言之，希尔伯特的第1-6问题关于数学基础理论，第 7-12 问题关于数论，第13-18问题属于代数和几何，而最后的第19-23问题属于数学分析范畴。经过许多数学家长期的努力，目前大多数问题都得到了完全或部分解答。 希尔伯特的第二问题是有名的“判定问题”。它至关重要，涉及整个数学基础，关心数学是否完备和一致？、是不是所有数学命题都可以通过有限次正确的数学步骤作出判定？希尔伯特雄心勃勃，要将整个数学体系严格公理化，然后用他的所谓“元数学”（证明数学的数学）来证明整个数学体系是坚不可摧的。 为了这个目标，他制定了一个后人称之为“希尔伯特计划”的部署 ：首先，将所有数学形式化，把每一个数学陈述都用符号来表达。然后，证明整个数学系统是完备的，即对任何一个数学陈述都存在一个数学证明（对所有命题，该命题本身或其否定命题一定能被证明）。同时，还要证明数学是一致的，也就是说绝不存在自相矛盾的陈述（任意命题和其否定命题不能同时被证明）。最后，还要具有可判断性，存在一个可以实现的算法，通过有限步程序最终判定数学陈述的对错。 这个计划的背景是罗素悖论引发的第三次数学危机，罗素悖论的公式表述为： $$ R = { x \mid x \notin x }, \qquad R \in R \iff R \notin R. $$ 简单来说，罗素悖论揭示了朴素数学直觉在形式化下的不一致性，数学中看似直观、自然的推理方式，在形式化后会导致自指性矛盾。希尔伯特计划试图通过形式化和元数学的一致性证明为数学奠定绝对可靠的基础。 ...